[Haskell-cafe] Re: Amazing

[Wolfgang Jeltsch]

Am Sonntag, 15. Februar 2009 23:00 schrieb Peter Verswyvelen:
> But if I understand it correctly, dependent types are a bit like that,
> values and types can inter-operate somehow?

With dependent types, parameters of types can be values. So you can define a 
data type List which is parameterized by the length of the list (and the 
element type):

    data List :: Nat -> * -> * where  -- The kind of List contains a type.

        Nil :: List 0 el

        Cons :: el -> List len el -> List (succ len) el

And you have functions where the result type can depend on the actual 
argument:

    replicate :: {len :: Nat} -> el -> List len el
        -- We have to name the argument so that we can refer to it.

So the type of replicate 0 'X' will be List 0 Char and the type of
replicate 5 'X' will be List 5 Char.

Dependent typing is very good for things like finding index-out-of-bounds 
errors and breach of data structure invariants (e.g., search tree balancing) 
at compile time. But you can even encode complete behavioral specifications 
into the types. For example, there is the type of all sorting functions. 
Properly implemented Quicksort and Mergesort functions would be values of 
this type but the reverse function wouldn’t. Personally, I have also thought 
a bit about dependently typed FRP where types encode temporal specifications.

Dependent types are really interesting. But note that you can simulate them to 
a large degree in Haskell, although especially dependent functions like 
replicate above need nasty workarounds. You may want to have a look at 
Haskell packages like type-level.

Best wishes,
Wolfgang