Maths - Computation - Data Types

This page looks at data types as mathematical expressions which we can manipulate in equations.

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. array size 3

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...
Tree x = Tip | Node (Tree x) x (Tree x)
value right
So a list allows us to create a tuple of variable length by using recursion. list a


The fixpoint are the values of x where T(x)=x



value + 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
set0(x)= 1
set1(x)= x
set2(x)= x(x-1)/2

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    



metadata block
see also:

papers by Conor McBride:

Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.