Prelude for type-level programming

[Etienne Laurin]

Hello,

To experiment with some of GHC's new features in HEAD, I have started
ported part of the Prelude from values and functions to types and
constraints.

For example: comparing lists.

instance Compare '[] '[] EQ
instance Compare '[] (x ': xs) LT
instance Compare (x ': xs) '[] GT
instance
    (Compare x y o,
     Case o [
      EQ --> Compare xs ys r,
      o --> o ~ r
     ])
    => Compare (x ': xs) (y ': ys) r

Prelude.Type> T :: (Compare '[I 1, I 2] '[I 1, I 3] a) => T a
LT

Sometimes I get nice error messages.

Prelude.Type> T :: If (I 1 == I 2) (a ~ "hello") (a ~ 3) => T a
    Kind mis-match
    The left argument of the equality predicate had kind `Symbol',
    but `3' has kind `Nat'

But often GHC refuses to type large constraints when there are too
many constraint kinds and free variables. It also gets confused if I
pretend to use higher-order kinds.

instance ((a >>= Const b) c) => (a >> b) c

    Kind mis-match
    The first argument of `>>' should have kind `k0 k1',
    but `a' has kind `k0 k1'
    In the instance declaration for `(a >> b) c'

I'm not sure yet how this is useful this, but I hope it can at least
entertain a few people and stress-test the typechecker.

http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type.hs

darcs get http://code.atnnn.com/darcs/type-prelude/

Etienne Laurin