<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">There's also <a href="https://github.com/yav/type-nat-solver">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>On May 1, 2016, at 1:54 PM, Mitchell Rosen <<a href="mailto:mitchellwrosen@gmail.com">mitchellwrosen@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">I think Carter is referring to this: <a href="http://hackage.haskell.org/package/ghc-typelits-natnormalise">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 href="javascript:" target="_blank" gdf-obfuscated-mailto="o_yzxDUEBwAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">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>_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe<br></blockquote></div><br></div></body></html>