We most certainly do have type-level functions. See type families. Cheers. ~Liam
On 26 June 2010 17:33, Jason Dagit <da...@codersbase.com> wrote: > > > On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit <da...@codersbase.com> wrote: >> >> >> On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin >> <andrewcop...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
