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,
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.