Greetings,
The latest type-nat solver is available as a GHC plugin. The repo is here:
https://github.com/yav/type-nat-solver
I just pushed a small fix-up and now it works with the GHC 7.10 release
candidate. The plugin makes use of an external solver (the plugin is
currently hard-coded to use `cvc4` but we should really parametrize on
this). I've not tested it a lot, but basic vector manipulation with GADTs
works fairly well, so you can do things like the examples at the end of the
e-mail.
If Marc---or anyone else---is interested in hacking on this, I'd be most
happy to collaborate, as I haven't had much time to work on this for the
last couple of a months.
We can push this is many interesting directions. Here are some ideas:
- Work on writing a Haskell based decision procedure; this would remove
the need for calling an external tool
- Explore and improve the current support for type naturals (e.g., add
rules to go beyond linear arithmetic).
- Explore other theories: the code in the current plugin happens to use
the theory of linear arithmetic, but most of the implementation is agnostic
to the actual theory used (apart from recognizing the symbols that belong
to the theory). So we have an opportunity to explore potential uses of
other theories (e.g., bit-vectors at the type level could be used to
implement finite sets, or type-level modulo arithmetic; some solvers have
experimental support for the theory of sets, so we could have interesting
reasoning about sets of various things: unions, intersections, etc).
Lots of interesting work to do, and not enough hacking time!
If there are questions, please drop me an e-mail directly, or we can chat
on the ghc-devs list, in case there are other interested developers.
Cheers,
-Iavor
Examples that work at the moment:
f :: ((a + 6) ~ x) => Proxy x -> ()
f = g
g :: ((6 <=? x) ~ True) => Proxy x -> ()
g _ = ()
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
Cons :: a -> Vec n a -> Vec (n + 1) a
append :: Vec m a -> Vec n a -> Vec (n + m) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
reverse = go Nil
where
go :: Vec m a -> Vec n a -> Vec (m + n) a
go xs Nil = xs
go xs (Cons y ys) = go (Cons y xs) ys
f1 :: Proxy (2 + a) -> ()
f1 = g1
g1 :: Proxy (1 + a) -> ()
g1 _ = ()
On Mon, Feb 23, 2015 at 2:53 PM, Simon Peyton Jones
Marc
For type-level literals, the man to talk to is Iavor Diatchki. He implemented the current system, and has been working on enhancements. I'm sure he'd welcome help!
There's also quite an active sub-group (on ghc-devs) working on "plug-ins" for the type inference algorithm, aimed at allowing things like better arithmetic reasoning to be done without having to change GHC itself.
Simon
| -----Original Message----- | From: dongen [mailto:dongen@cs.ucc.ie] | Sent: 23 February 2015 10:54 | To: Simon Peyton Jones | Cc: ghc-devs@haskell.org | Subject: GHC Type Inference | | Dear Simon, | | | I am cc-ing _ghc-devs@haskell.org_ as requested on _ghc.haskell.org_. | | I hope you're fine. | | On _ghc.haskell.org_ I noticed you are the ``owner'' of _type | inference and interface files._ | | A year ago I started a project that requires integer type-level | literals but I soon had to drop it because GHC wasn't able to | simplify simple type equalities. As a consequence, I had to | add lots and lots of constraints to make my code work, which | effectively meant the code became unmaintainable because a small | change requlted in lots of errors. | | I know have a bit more time to work on the project and I'd like | to see if it's possible to ``talk'' to somebody in the GHC team | to see if we can improve type-level literal inference for natural | numbers. | | Is there somebody who's ``responsible'' for this area in the GHC | team? If yes, would you mind giving me their contact details? | | Regards, | | | Marc van Dongen