[Haskell-cafe] Type-Level Programming

[Andrew Coppin]

Liam O'Connor wrote:
> It means that not only can values have types, types can have values.
>   

Uh, don't types have values *now*?

> An example of the uses of a dependent type would be to encode the
> length of a list in it's type.
>   

Oh, right. So you mean that as well as being able to say "Foo Bar", you 
can say "Foo 7", where 7 is (of course) a value rather than a type. (?)