Brent Yorgey wrote:
As several people have pointed out, type-level programming in Haskell resembles logic programming a la Prolog -- however, this actually only applies to type-level programming using multi-parameter type classes with functional dependencies [1] (which was until recently the only way to do it).
Type-level programming using the newer type families [2] (which are equivalent in power [3]) actually lets you program in a functional style, much more akin to defining value-level functions in Haskell.
I did wonder what the heck a "type function" is or why you'd want one. And then a while later I wrote some code along the lines of class Collection c where type Element c :: * empty :: c -> Bool first :: c -> Element c So now it's like Element is a function that takes a collection type and returns the type of its elements - a *type function*. Suddenly the usual approach of doing something like class Collection c where empty :: c x -> Bool first :: c x -> x seems like a clumsy kludge, and the first snippet seems much nicer. (I gather that GHC's implementation of all this is still "fragile" though? Certainly I regularly get some very, very strange type errors if I try to use this stuff...) The latter approach relies on "c" having a particular kind, and the element type being a type argument (rather than static), and in a specific argument position, and so on. So you can construct a class that works for *one* type of element, or for *every* type of element, but not for only *some*. The former approach (is that type families or associated types or...? I get confused with all the terms for nearly the same thing...) seems much cleaner to me. I never liked FDs in the first place. Not only is Element now a function, but you define it as a sort of case-by-case pattern match: instance Collection Bytestring where type Element ByteString = Word8 instance Collection [x] where type Element [x] = x instance Ord x => Collection (Set x) where type Element (Set x) = x ... So far, I haven't seen any other obvious places where this technology might be useful (other than monads - which won't work). Then again, I haven't looked particularly hard either. ;-)
However, all of this type-level programming is fairly *untyped*
Yeah, there is that.
-- the only kinds available are * and (k1 -> k2)
Does # not count?
so type-level programming essentially takes place in the simply typed lambda calculus with only a single base type, except you can't write explicit lambdas.
Uh... if you say so? o_O
I'm currently working on a project with Simon Peyton-Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic on enabling *typed* functional programming at the type level in GHC
Certainly sounds interesting...