Tutorial by Examples

We can draw a connection between the Haskell types and the natural numbers. This connection can be made assigning to every type the number of inhabitants it has. Finite union types For finite types, it suffices to see that we can assign a natural type to every number, based in the number of constr...

The addition and multiplication have equivalents in this type algebra. They correspond to the tagged unions and product types. data Sum a b = A a | B b data Prod a b = Prod a b We can see how the number of inhabitants of every type corresponds to the operations of the algebra. Equivalently, we...

Lists Lists can be defined as: data List a = Nil | Cons a (List a) If we translate this into our type algebra, we get List(a) = 1 + a * List(a) But we can now substitute List(a) again in this expression multiple times, in order to get: List(a) = 1 + a + a*a + a*a*a + a*a*a*a + ... ...

The derivative of a type is the type of its type of one-hole contexts. This is the type that we would get if we make a type variable disappear in every possible point and sum the results. As an example, we can take the triple type (a,a,a), and derive it, obtaining data OneHoleContextsOfTriple = (a...

Functions can be seen as exponentials in our algebra. As we can see, if we take a type a with n instances and a type b with m instances, the type a -> b will have m to the power of n instances. As an example, Bool -> Bool is isomorphic to (Bool,Bool), as 2*2 = 2². iso1 :: (Bool -> Bool) -...