[Haskell-cafe] Type-Level Programming

[Liam O'Connor]

We most certainly do have type-level functions. See type families.

Cheers.
~Liam



On 26 June 2010 17:33, Jason Dagit <dagit at codersbase.com> wrote:
>
>
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>