Prelude for type-level programming

[Etienne Laurin]

Hello,

Now that GHC ticket #6015 and many others are fixed (thanks Simon),
all of Prelude.Type now kind checks, particularly Map and company:

>>> T::T (Map ((+) (I 1)) '[I 2, I 3])
[3,4]
>>> type Or  = FoldR (||) False
>>> type Any = (Compose1 Or) `Compose2` Partial1 Map
>>> T::T (Any ((==) 1) '[3,2,1])
True

I have also completed the implementation of two's complement integers
and added a second version of the code using type families instead of
type classes (except for higher-order functions).

I just discovered the singletons package and the associated paper. It
seems that I can now generate all my type families using TH.
Wonderful!

Etienne Laurin

2012/4/25 Simon Peyton-Jones <simonpj at microsoft.com>:
> 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
>
>