[Haskell-cafe] Type-Level Programming

[Jason Dagit]

On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin <andrewcoppin at btinternet.com
> 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.

Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100626/0bd0f87d/attachment.html