For these discussions we will be using racket so that we can put these ideas into practice

In practice this means that if we see \( \left( \lambda x . x \right) 5 \) it can be evaluated to \( 5 \) .

Note that in most imperative programming languages, you can rebind variables, which means that if we were to replace that variable with it's initial value everywhere in the code, then for every line in the code that uses the variable after it's rebound, then the meaning of the program would change.

If a programming languages is referentially transparent this is beneficial if we want to reason about our code, because whenever we see a symbol, we know what it's value is immediately.

Function Abstraction

If we have (lambda (x) b): R, and if we know that x: A, and that the body evalutes to something of type b, then the entire function has type A -> B

        x: A
        b: B
        ---

    

Function Application

(f t) : R, if we know that f has type T1 -> T2, then we know that (f t) has type T2,

        f: T1 -> T2
        t: T1
        ---
        (f t) : T2
    

Cardinality of a Type

We have the natural numbers

        Zero: Nat
    

        t: Nat
        ---
        Succ t : Nat
    

And if we ask the question, how many numbers are there in the unverse then we can say that there are countably infinite because we can always construct a new element where we know that that element is different from all other elements.

In reality we're on a computer and so there can never exist infinitely many types.

We also know that there is exactly one zero in the universe. We can think about the zero as a value constructor of no arguments (aka a nullary function/thunk) or it is a singleton value.

Single Value Type

What is the simplest type you can constructe, the one that has the smallest nonzero cardinality

Unit is a type with one constant value unit.

        unit: Unit
    

        e : Unit
        ---
        unit
    

It is similar to void, and is an appropriate return type for functions that has side effects, without side effects it wouldn't really be necessary. So here is a type with one possible value, but would we ever have a type with zero possible values? This is a type which is not constructible, because what would it ever evaluate to?

Enumerated Types

        data Date = Monday
                  | Tuesday
                  | Wednesday
                  | Thursday
                  | Friday
                  | Saturday
                  | SUnday deriving (Show)
    

Continas one or more disjoint value constructors of zero arguments

The cardinality of this type is 7, because we have 7 different nullary constructors. So at least for enumerated types the cardinality of an enumerated type is given by the number of different nullary constructors.

Sum Types

We call enumerated types as sum types, this is because we say that a given instance is "this type OR that type", which we can think of union or the sum of it's parts.

Product Type

Note that if we have two types T1, T2, then the cardiinality of T1 or T2 is the sum of their cardinalities

What if we want a type whose cardinality is the product of the cardinalities of the tywo types, then one way to do this is to have pairs, where we have every possible value, value pair.

        t1: T1
        t2: T2
        ---
        Pair t1 t2 : T1xT2
    

We can think of T1xT2 as a function which maps a type from T1 and T2, to (T1, T2) ? We also have projectections:

        p: T1xT2
        ---
        fst p: T1
    

        p: T1xT2
        ---
        snd p: T2
    

We can generalize the pair to a triple, or to any cartesian product. If we want this to work for a structure type, then all we need to do is change the name of the projections.

Combination of Sum and Product

        data Nat = Zero | Succ Nat
    

We have two ways of constructing a natural number through the Zero constructor or the Succ constructor.

        data ListNat = Empty | Cons Nat ListNat
    

The above is a list of natural numbers, so here Cons Nat ListNat represents a . So we can do Cons | (Cons 2 Empty) when types are written next to each other we get a product type and when we use | we get a sum type.

        data BinTree = Leafe Nat | Node BinTree Nat BinTree
    

So we have on the left Leaf 1, and then on the right right we can have Node (Leaf 1) 5 (Leaf 3)

Algebraic Data Types

Sum types, product types, a combination of sum types and proudct types.

We can use pattern matching to decompose and extract values

        
            data Pair = Pair String Int
            data BTree = Leaf | Node BTree Pair BTree
            getV2 (Node _ (Pair _ v2) _) = v2
        
    

So getV2 is pattern matching where we use wildcards to throw away values that we still need to match, so it only gets the right most Int from the pair.

Polymorphism

A type system that allows a single piece of code to be used with different types are said to be polymorphic.

There are multiple approaches to make this happen

• Parametric Polymorphism
• Ad-Hoc Polymorphism
• Sub-Types

        data ListNat = EmptyListNat | ConsNat Nat ListNat
        data ListInt = EmptyListInt | ConsInt Int ListInt
        data ListFloat = EmptyListFloat | ConsFloat Float ListFloat
    

This is bad, because it's verbose and tons of code re-use, because later we might need even more types of lists, and we would also need to redefine functions that run on every type of list, even ones that we would need everywhere like the length of a list.

With Parametric polymorphism, we allow a single piece of code to be typed generically using a type variable in place of actual types. This is like templating in c++, when we do std::vectorT.

In Haskell, all we have to do is something like this

        
            data MyList a = MyEmpty
                          | Cons a (MyList a)
        
    

In this case a can stand for different types, and we say that MyList is polymorphic over a, so if we write Cons | (EMpty 1) would be MyList Int

        
            myLength::MyList a -> Int
            myLength MyEmpty = 0
            myLength (Cons _ ls) = 1 + myLength ls
        
    

So here we abstracted over the type of the elements of MyList, which allows us to have this function working for many different types.

        data Lake = Ontario | Erie
            deriving (Show) // come up with a way to print the data type
        data Bay = Hudson | Baffin
            deriving (Show)
        data FunSites = MyLake Lake | MyBay Bay
            deriving (Show)

        ---

        data Class = Class Int  (type level definition)

        ---

        data FunSitesNew = Lake Lake | Bay Bay


        ---

        data Nat = Zero | Succ Nat (two ways to construct a natural number),
    

If you want to construct a FUnSite, then you can use the constructor Lake, provided a Lake, the Lake refers to the previously defined Lake, because we ar etalking about types, the type is on the right, we're defining a constructor that has the name Lake, and it has type Lake -> FunSite, this example shows that we can use the same name for the data construct as the type, and haskell will not get confused.

        Data Person = Person String Int String FLoat Int deriving (Show)
        getName (Person n _ _ _ _ ) = n
        getAge (Person _ a _ _ _ ) = a
        getClass (Person _ _ c _ _ ) = c
    

but the above is annoying so we can do something like this

        data Person = -- new type
        Person { -- a data constructor
            name :: String,
            age :: Int,
        }