This page looks at data types as mathematical expressions which we can manipulate in equations.
- See page here for more of an introduction to the subject.
- See this page for a more mathematical approach to the subject.
Algebraic Data Types
| Name | Algebra | Catagory | Haskell |
|---|---|---|---|
| Unit - has one value | 1 | Final | () |
| Void | 0 | Initial | not in haskell |
| Boolean | 2 | ||
| Sum - disjoint union - either | + | Sum | |
| Product - both | • | Product | |
| Exponent - function space | ^ | Exponent | function type |
| For example: product creates a tuple. |  |
Inductivly Defined Types
| Name | Equation | Catagory | Haskell | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| List | L(x)=1+x•L(x) = 1+x+x²+x³... |
List x = Nil | Cons x (List x) | |||||||||
| Binary Tree | T(x)=1+x•T²(x) =(1 - √(1-4x))/2x = 1+x+2x²+5x³+14x4... |
|
| So a list allows us to create a tuple of variable length by using recursion. |  |
Fixpoint
The fixpoint are the values of x where T(x)=x
see
- least fixpoint
- greatest fixpoint
- fixpoint theorm
- http://plato.stanford.edu/entries/recursive-functions/
- Recursive types for free! - Philip Wadler
Zipper
value + one-hole-context
One-hole-context
The derirative of a regular type is its type of one-hole contexts (Conor McBride)
| 1 => 0 | |||
| x => 1 | |||
| x² => 2x | |||
| x³ => 3x² |
Using calculus notation
| ∂1 = 0 | |||
| ∂x = 1 | |||
| ∂x² = 2x | |||
| ∂x³ = 3x² | |||
| ∂(f+g) = ∂f + ∂g | |||
| ∂(f•g) = ∂f•g + f•∂g | |||
| ∂(f(g)) = ∂f(g) •∂g |
Non-Regular Types
| Name | Equation | Haskell |
|---|---|---|
| Bags (No order) | ||
| ULists (No duplicates) | ||
| Sets (No order,No duplicates) | setn(x)= set of size n containing type x in general: setn(x)= x(x-1)...x-(n+1)/n! all possible holes = Δ f(x)=f(x+1)-f(x) Δ set(x)=set(x) set(x) = 2x=all maps from x to bool |
|
| Cyclic Lists | ||
| Deques |
