Re: [Haskell-cafe] Type-Level Programming

We most certainly do have type-level functions. See type families. Cheers. ~Liam On 26 June 2010 17:33, Jason Dagit wrote:

On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit wrote:

...

On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin wrote:

...

wren ng thornton wrote:

...

And, as Jason said, if you're just interested in having the same programming style at both term and type levels, then you should look into dependently typed languages.

Out of curiosity, what the hell does "dependently typed" mean anyway?

The types can depend on values.  For example, have you ever notice we have families of functions in Haskell like zip, zip3, zip4, ..., and liftM, liftM2, ...? Each of them has a type that fits into a pattern, mainly the arity increases.  Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name.  That of course, is only the tip of the iceberg.  Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work.  Even the example I just gave can be emulated.  See this paper: http://www.brics.dk/RS/01/10/ Also SHE: http://personal.cis.strath.ac.uk/~conor/pub/she/ Then there are languages like Coq and Agda that support dependent types directly.  There you can return a type from a function instead of a value.

I just realized, I may not have made this point sufficiently clear.  Much of the reason we need to do extra work in Haskell to emulate dependent types is because types are not first class in Haskell.  We can't write terms that manipulate types (type level functions).  Instead we use type classes as sets of types and newtypes/data in place of type level functions.  But, in dependently typed languages types are first class.  Along this line, HList would also serve as a good example of what you would/could do in a dependently type language by showing you how to emulate it in Haskell. Jason _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe