[Haskell-cafe] Type-Level Programming

[Jason Dagit]

On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit <dagit at codersbase.com> wrote:

>
>
> 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.
>

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100626/4ecf35a1/attachment.html