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