Thanks Etienne 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. http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/promotion... The error message is bogus (GHC crashes) which I will fix. But if you think higher-sorts are useful, make the case! Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Etienne Laurin | Sent: 21 April 2012 00:44 | To: GHC users | Subject: Prelude for type-level programming | | 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 | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users