Prelude for type-level programming
simonpj at microsoft.com
Wed Apr 25 13:18:51 CEST 2012
When I tried to compile your Type.hs file, the first thing that broke was this:
class ((ma :: m a) >>= (f :: a -> m b -> Constraint)) (mb :: m b) | ma f -> mb
You want the sort of 'm' to be BOX -> BOX, but you can't do this at the moment. As our paper say, the sort system is pretty rudimentary, being just a single sort BOX.
The error message is bogus (GHC crashes) which I will fix. But if you think higher-sorts are useful, make the case!
| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Etienne Laurin
| Sent: 21 April 2012 00:44
| To: GHC users
| Subject: Prelude for type-level programming
| 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
| (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.
| darcs get http://code.atnnn.com/darcs/type-prelude/
| Etienne Laurin
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
More information about the Glasgow-haskell-users