Facilities for generating Haskell types in Haskell (“second order Haskell”)?

Question

Apologies in advance if this question is a bit vague. It's the result of some weekend daydreaming.

With Haskell's wonderful type system, it's delightfully pleasing to express mathematical (especially algebraic) structure as typeclasses. I mean, just have a look at numeric-prelude! But taking advantage of such wonderful type structure in practice has always seemed difficult to me.

You have a nice, type-system way of expressing that v1 and v2 are elements of a vector space V and that w is a an element of a vector space W. The type system lets you write a program adding v1 and v2, but not v1 and w. Great! But in practice you might want to play with potentially hundreds of vector spaces, and you certainly don't want to create types V1, V2, ..., V100 and declare them instances of the vector space typeclass! Or maybe you read some data from the real world resulting in symbols a, b and c - you may want to express that the free vector space over these symbols really is a vector space!

So you're stuck, right? In order to do many of the things you'd like to do with vector spaces in a scientific computing setting, you have to give up your typesystem by foregoing a vector space typeclass and having functions do run-time compatibility checks instead. Should you have to? Shouldn't it be possible to use the fact that Haskell is purely functional to write a program that generates all the types you need and inserts them into the real program? Does such a technique exist? By all means do point out if I'm simply overlooking something basic here (I probably am) :-)

Edit: Just now did I discover fundeps. I'll have to think a bit about how they relate to my question (enlightening comments with regards to this are appreciated).

Answer 1

Template Haskell allows this. The wiki page has some useful links; particularly Bulat's tutorials.

The top-level declaration syntax is the one you want. By typing:

mkFoo = [d| data Foo = Foo Int |]

you generate a Template Haskell splice (like a compile-time function) that will create a declaration for data Foo = Foo Int just by inserting the line $(mkFoo).

While this small example isn't too useful, you could provide an argument to mkFoo to control how many different declarations you want. Now a $(mkFoo 100) will produce 100 new data declarations for you. You can also use TH to generate type class instances. My adaptive-tuple package is a very small project that uses Template Haskell to do something similar.

An alternative approach would be to use Derive, which will automatically derive type class instances. This might be simpler if you only need the instances.

Answer 2

Also there are some simple type-level programming techniques in Haskell. A canonical example follows:

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

Take a moment to take that in. I think it is pretty magical that it works.

However, type-level programming in Haskell is in the feature-uncanny-valley -- just enough to draw attention to how much you can't do. Dependently-typed languages like Agda, Coq, and Epigram take this style to its limit and full power.

Template Haskell is much more like the usual LISP-macro style of code generation. You write some code to write some code, then you say "ok insert that generated code here". Unlike the above technique, you can write any computably-specified code that way, but you don't get the very general typechecking as is seen in concatV above.

So you have a few options to do what you want. I think metaprogramming is a really interesting space, and in some ways still quite young. Have fun exploring. :-)