# Maths - Computation - Data Types

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...

 Tree x = Tip | Node (Tree x) x (Tree x) left branch value right branch
 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

### 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

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!
=Σx_n_/n!
=1+x+x3/!2+x5/!3

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

papers by Conor McBride:

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.      Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to this site, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

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