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

Expression
An expression is one of the following:
1. An identifier: Some collection of symbols not including dot or lambda
2. A function expression: $$\lambda x . expr$$
3. A function application: $$f expr$$

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

Function Side Effects
We say that a programming function has side effects when, it has any observable effect other than returning a value.
Syntactic Sugar
Syntactic sugar is the part of a programs syntax that doesn't introduce new functionality but provides a simpler way to utilize existing functionality.
Function Purity
We say that a programming function is pure when:
• The function's behavior is exactly determined by the value of it's inputs
• The function has no side effects
Referentially Transparent
We say that an identifier is referentially transparent if it can be substituted with it's value in the source code without changing the meaning of the program.

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
• 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,
}