[Solved]: Types as first class Citizen

First class types enable something called dependent typing. These allow the programmer to use values of types at type level. For example, the type of all pairs of integers is a regular type, while the pair of all integers with the left number smaller than the right number is a dependent type. The standard introductory example of this is length encoded lists (typically called Vector in Haskell/Idris). The following pseudo-code is a mixture of Idris and Haskell.

-- a natural number data Nat = Zero | Successor Nat  data Vector length typ where   Empty : Vector Zero typ   (::)   : typ -> Vector length typ -> Vector (Successor length) typ 

This piece of code tells us two things:

• The empty list has length zero.
• consing an element onto a list creates a list of length n + 1

This looks very similar to another concept with 0 and n + 1, doesn’t it? I’ll come back to that. What do we gain from this? We can now determine additional properties of the functions we use. For example: An important property of append is that the length of the resulting list is the sum of the lengths of the two argument lists:

plus : Nat -> Nat -> Nat plus          Zero n = n plus (Successor m) n = Successor (plus m n)  append : Vector n a -> Vector m a -> Vector (plus n m) a append Empty  ys = ys append (x::xs) ys = x :: append xs ys 

But all in all this technique does not seem all to useful in everyday programming. How does this relate to sockets, POST/GET requests and so on? Well it doesn’t (at least not without considerable effort). But it can help us in other ways: Dependent types allow us to formulate invariants in code – rules as how a function must behave. Using these we get additional safety about the code’s behaviour, similar to Eiffel’s pre- and postconditions. This is extremely useful for automated theorem proving, which is one of the possible uses for Idris. Coming back to the example above, the definition of length-encoded lists resembles the mathematical concept of induction. In Idris, you can actually formulate the concept of induction on such a list as follows:

              -- If you can supply the following: list_induction : (Property : Vector len typ -> Type) -> -- a property to show                   (Property Empty) -> -- the base case                   ((w : a) -> (v : Vector n a) ->                       Property v -> Property (w :: v)) -> -- the inductive step                   (u : Vector m b) -> -- an arbitrary vector                   Property u -- the property holds for all vectors 

This technique is limited to constructive proofs, but is nonetheless very powerful. You can try to write append inductively as an exercise. Of course, dependent types are just one use of first class types, but it’s arguably one of the most common ones. Additional uses include, for example, returning a specific type from a function based on its arguments.

type_func : Vector n a -> Type type_func Empty = Nat type_func v     = Vector (Successor Zero) Nat  f : (v : Vector n a) -> type_func v f Empty = 0 f vs    = length vs :: Empty 

This is a nonsensical example, but it demonstrates something you cannot emulate without first class types.