[Haskell-cafe] Type-Level Programming
liamoc at cse.unsw.edu.au
Sat Jun 26 09:00:55 EDT 2010
We most certainly do have type-level functions. See type families.
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:
>> Also 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe