Datatype promotion for dependently challenged

Question

After reading through the ghc 7.4. pre-release notes and the Giving Haskell a Promotion paper, I'm still confused on what you actually do with promoted types. For example, the GHC manual gives the following examples on promoted datatypes:

data Nat = Ze | Su Nat  data List a = Nil | Cons a (List a)  data Pair a b = Pair a b  data Sum a b = L a | R b 

What kind of uses do these have as kinds? Can you give (code) examples?

Answer 1

There are at least two examples in the paper itself:

"1. Introduction" says: "for example, we might be able to ensure [at compile time] that an alleged red-black tree really has the red-black property".

"2.1 Promoting datatypes" discusses length-indexed vectors (that is, vectors with compile-time "index out of bounds" errors).

You can also take a look at earlier work in this direction, e.g. HList library for type-safe heterogenous lists and extensible collections. Oleg Kiselyov has many related works. You can also read works on programming with dependent types. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf has introductory examples for type-level computations in Agda, but those can be applied to Haskell as well.

Roughly, the idea is that head for lists is given a more precise type. Instead of

head :: List a -> a 

it is

head :: NotEmptyList a -> a 

The latter head function is more typesafe than the fomer: it can never be applied to empty lists because it would cause compiler errors.

You need type-level computations to express types such as NotEmptyList. Type classes with functional dependencies, GAGTs and (indexed) type families already provide weak forms of type-level computations for haskell. The work you mentioned just elaborates further in this direction.

See http://www.haskell.org/haskellwiki/Non-empty_list for an implementation using only Haskell98 type classes.

Answer 2

Nat can be e.g. used to construct numerical vectors that can be only added if they have the same length, checked at compile time.