<div dir="ltr">ghc-typelits-natnormalise worked for the example. Tried type-nat-solver too, however, got bellow error (maybe just because my cabal setup):<div><br></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)">z3: runInteractiveProcess: runInteractiveProcess: exec: does not exist (No such file or directory)</span><br></span></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)"><br></span></span></div><div>Thanks to all for your solutions, first time tried GHC plugins :)<br></div><div>Also I'm wondering if GHC 8.0 could make this easier? couldn't wait to try GHC 8.0</div><div><br></div><div>-- baojun</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, May 2, 2016 at 7:05 AM Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">There's also <a href="https://github.com/yav/type-nat-solver" target="_blank">https://github.com/yav/type-nat-solver</a>, which uses a Z3 backend to do the solving. I wonder how the two solvers compare.<div><br></div><div>In your specific case, though: 1 + (n - 1) does *not* always equal n! If n is 0, then 1 + (n - 1) is 1, due to the partiality of (-). Always, always add before subtracting.</div><div><br></div><div>Richard</div><div><br><div></div></div></div><div style="word-wrap:break-word"><div><div><div>On May 1, 2016, at 1:54 PM, Mitchell Rosen <<a href="mailto:mitchellwrosen@gmail.com" target="_blank">mitchellwrosen@gmail.com</a>> wrote:</div><br></div></div></div><div style="word-wrap:break-word"><div><div><blockquote type="cite"><div dir="ltr">I think Carter is referring to this: <a href="http://hackage.haskell.org/package/ghc-typelits-natnormalise" target="_blank">http://hackage.haskell.org/package/ghc-typelits-natnormalise</a><div><br>On Saturday, April 30, 2016 at 8:35:01 AM UTC-4, Carter Schonwald wrote:<blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex">Use the type lits Nat solver plugin by Christian B, or a userland peano encoding. Sadly ghc does have any builtin equational theory so you either need to construct proofs yourself or use a plugin. <div><br></div><div>I'm personally doing the plugin approach. If you would like to construct the proofs by hand I'll dig up some examples later today if you like. <span></span><br><br>On Saturday, April 30, 2016, Baojun Wang <<a rel="nofollow">wan...@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hi List,</div><div><br></div><div>When I try to build below program, the compiler complains </div><div><br></div><div> Couldn't match type ‘n’ with ‘1 + (n - 1)’ …<br></div><div><br></div><div>Why GHC (7.10.3) cannot do type level natural number arithmetic? `` n /= 1 + (n-1)`` at type level?</div><div><br></div><div>-- | main.hs</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE FlexibleInstances #-}</div><div>{-# LANGUAGE GADTs #-}</div><div>{-# LANGUAGE PolyKinds #-}</div><div>{-# LANGUAGE KindSignatures #-}</div><div>{-# LANGUAGE TypeOperators #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE OverloadedStrings #-}</div><div>{-# LANGUAGE DeriveGeneric #-}</div><div><br></div><div>module Main where</div><div><br></div><div>import qualified Data.ByteString as B</div><div>import Data.ByteString(ByteString)</div><div>import Data.Serialize -- require cereal</div><div><br></div><div>import GHC.TypeLits</div><div><br></div><div>data Scalar :: Nat -> * -> * where</div><div> Nil :: Scalar 0 a</div><div> Cons :: a -> Scalar m a -> Scalar (1+m) a</div><div><br></div><div>instance (Serialize a) => Serialize (Scalar 0 a) where</div><div> get = return Nil</div><div> put _ = return $ mempty</div><div><br></div><div>instance (Serialize a) => Serialize (Scalar n a) where</div><div> get = do</div><div> x <- get :: Get a</div><div> xs <- get :: Get (Scalar (n-1) a)</div><div> return $! Cons x xs</div><div> put (Cons x xs) = do</div><div> put (x :: a)</div><div> put xs</div><div><br></div></div><div>--</div><div><br></div><div>/tmp/vect1/app/Main.hs:31:15: Couldn't match type ‘n’ with ‘1 + (n - 1)’ …</div><div> ‘n’ is a rigid type variable bound by</div><div> the instance declaration at /tmp/vect1/app/Main.hs:27:10</div><div> Expected type: Scalar n a</div><div> Actual type: Scalar (1 + (n - 1)) a</div><div> Relevant bindings include</div><div> xs :: Scalar (n - 1) a (bound at /tmp/vect1/app/Main.hs:30:5)</div><div> get :: Get (Scalar n a) (bound at /tmp/vect1/app/Main.hs:28:3)</div><div> In the second argument of ‘($!)’, namely ‘Cons x xs’</div><div> In a stmt of a 'do' block: return $! Cons x xs</div><div>Compilation failed.</div><div><br></div><div>- baojun</div></div>
</blockquote></div>
</blockquote></div></div></blockquote></div></div></div><div style="word-wrap:break-word"><div><div><blockquote type="cite">_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>