- An identifier: Some collection of symbols not including dot or lambda
- A function expression:
- A function application:
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 it can be evaluated to .
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.
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 ---
(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
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.
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?
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.
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.
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.
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)
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.
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
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, }