<div dir="ltr">Greetings,<div><br></div><div>The latest type-nat solver is available as a GHC plugin. The repo is here:</div><div><br></div><div><a href="https://github.com/yav/type-nat-solver">https://github.com/yav/type-nat-solver</a><br></div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>We can push this is many interesting directions. Here are some ideas:</div><div> - Work on writing a Haskell based decision procedure; this would remove the need for calling an external tool</div><div> - Explore and improve the current support for type naturals (e.g., add rules to go beyond linear arithmetic).</div><div> - 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).</div><div><br></div><div>Lots of interesting work to do, and not enough hacking time!</div><div><br></div><div>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.</div><div><br></div><div>Cheers,</div><div>-Iavor</div><div><br></div><div><br></div><div>Examples that work at the moment:</div><div><br></div><div><br></div><div><div><font face="monospace, monospace">f :: ((a + 6) ~ x) => Proxy x -> ()</font></div><div><font face="monospace, monospace">f = g</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">g :: ((6 <=? x) ~ True) => Proxy x -> ()</font></div><div><font face="monospace, monospace">g _ = ()</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">data Vec :: Nat -> * -> * where</font></div><div><font face="monospace, monospace"> Nil :: Vec 0 a</font></div><div><font face="monospace, monospace"> Cons :: a -> Vec n a -> Vec (n + 1) a</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">append :: Vec m a -> Vec n a -> Vec (n + m) a</font></div><div><font face="monospace, monospace">append Nil ys = ys</font></div><div><font face="monospace, monospace">append (Cons x xs) ys = Cons x (append xs ys)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">reverse = go Nil</font></div><div><font face="monospace, monospace"> where</font></div><div><font face="monospace, monospace"> go :: Vec m a -> Vec n a -> Vec (m + n) a</font></div><div><font face="monospace, monospace"> go xs Nil = xs</font></div><div><font face="monospace, monospace"> go xs (Cons y ys) = go (Cons y xs) ys</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">f1 :: Proxy (2 + a) -> ()</font></div><div><font face="monospace, monospace">f1 = g1</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">g1 :: Proxy (1 + a) -> ()</font></div><div><font face="monospace, monospace">g1 _ = ()</font></div></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 23, 2015 at 2:53 PM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Marc<br>
<br>
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!<br>
<br>
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.<br>
<br>
Simon<br>
<br>
| -----Original Message-----<br>
| From: dongen [mailto:<a href="mailto:dongen@cs.ucc.ie">dongen@cs.ucc.ie</a>]<br>
| Sent: 23 February 2015 10:54<br>
| To: Simon Peyton Jones<br>
| Cc: <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
| Subject: GHC Type Inference<br>
|<br>
| Dear Simon,<br>
|<br>
|<br>
| I am cc-ing _ghc-devs@haskell.org_ as requested on _ghc.haskell.org_.<br>
|<br>
| I hope you're fine.<br>
|<br>
| On _ghc.haskell.org_ I noticed you are the ``owner'' of _type<br>
| inference and interface files._<br>
|<br>
| A year ago I started a project that requires integer type-level<br>
| literals but I soon had to drop it because GHC wasn't able to<br>
| simplify simple type equalities. As a consequence, I had to<br>
| add lots and lots of constraints to make my code work, which<br>
| effectively meant the code became unmaintainable because a small<br>
| change requlted in lots of errors.<br>
|<br>
| I know have a bit more time to work on the project and I'd like<br>
| to see if it's possible to ``talk'' to somebody in the GHC team<br>
| to see if we can improve type-level literal inference for natural<br>
| numbers.<br>
|<br>
| Is there somebody who's ``responsible'' for this area in the GHC<br>
| team? If yes, would you mind giving me their contact details?<br>
|<br>
| Regards,<br>
|<br>
|<br>
| Marc van Dongen<br>
</blockquote></div><br></div>