Prelude for type-level programming
etienne at atnnn.com
Sat Apr 21 01:43:40 CEST 2012
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
For example: comparing lists.
instance Compare ' ' EQ
instance Compare ' (x ': xs) LT
instance Compare (x ': xs) ' GT
(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
Sometimes I get nice error messages.
Prelude.Type> T :: If (I 1 == I 2) (a ~ "hello") (a ~ 3) => T a
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
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.
darcs get http://code.atnnn.com/darcs/type-prelude/
More information about the Glasgow-haskell-users