[Haskell-cafe] Type-Level Programming

[Andrew Coppin]

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...