Prelude for type-level programming

[Simon Peyton-Jones]

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.pdf


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 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
| 
| 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users