[Haskell-cafe] Type-Level Programming
andrewcoppin at btinternet.com
Mon Jun 28 15:41:44 EDT 2010
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  (which was until recently the only way to
> do it).
> Type-level programming using the newer type families  (which are
> equivalent in power ) 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...
More information about the Haskell-Cafe