[Haskell-cafe] cannot perform arithmetic with GHC.TypeLits?

[Baojun Wang]

ghc-typelits-natnormalise worked for the example. Tried type-nat-solver
too, however, got bellow error (maybe just because my cabal setup):

z3: runInteractiveProcess: runInteractiveProcess: exec: does not exist (No
such file or directory)

Thanks to all for your solutions, first time tried GHC plugins :)
Also I'm wondering if GHC 8.0 could make this easier? couldn't wait to try
GHC 8.0

-- baojun

On Mon, May 2, 2016 at 7:05 AM Richard Eisenberg <eir at cis.upenn.edu> wrote:

> There's also https://github.com/yav/type-nat-solver, which uses a Z3
> backend to do the solving. I wonder how the two solvers compare.
>
> 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.
>
> Richard
>
> On May 1, 2016, at 1:54 PM, Mitchell Rosen <mitchellwrosen at gmail.com>
> wrote:
>
> I think Carter is referring to this:
> http://hackage.haskell.org/package/ghc-typelits-natnormalise
>
> On Saturday, April 30, 2016 at 8:35:01 AM UTC-4, Carter Schonwald wrote:
>>
>> 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.
>>
>> 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.
>>
>> On Saturday, April 30, 2016, Baojun Wang <wan... at gmail.com> wrote:
>>
>>> Hi List,
>>>
>>> When I try to build below program, the compiler complains
>>>
>>>   Couldn't match type ‘n’ with ‘1 + (n - 1)’ …
>>>
>>> Why GHC (7.10.3) cannot do type level natural number arithmetic? `` n /=
>>> 1 + (n-1)`` at type level?
>>>
>>> -- | main.hs
>>> {-# LANGUAGE ScopedTypeVariables #-}
>>> {-# LANGUAGE FlexibleInstances #-}
>>> {-# LANGUAGE GADTs #-}
>>> {-# LANGUAGE PolyKinds #-}
>>> {-# LANGUAGE KindSignatures #-}
>>> {-# LANGUAGE TypeOperators #-}
>>> {-# LANGUAGE DataKinds #-}
>>> {-# LANGUAGE OverloadedStrings #-}
>>> {-# LANGUAGE DeriveGeneric #-}
>>>
>>> module Main where
>>>
>>> import qualified Data.ByteString as B
>>> import Data.ByteString(ByteString)
>>> import Data.Serialize   -- require cereal
>>>
>>> import GHC.TypeLits
>>>
>>> data Scalar :: Nat -> * -> * where
>>>   Nil :: Scalar 0 a
>>>   Cons :: a -> Scalar m a -> Scalar (1+m) a
>>>
>>> instance (Serialize a) => Serialize (Scalar 0 a)  where
>>>   get = return Nil
>>>   put _ = return $ mempty
>>>
>>> instance (Serialize a) => Serialize (Scalar n a) where
>>>   get = do
>>>     x  <- get :: Get a
>>>     xs <- get :: Get (Scalar (n-1) a)
>>>     return $! Cons x xs
>>>   put (Cons x xs) = do
>>>     put (x :: a)
>>>     put xs
>>>
>>> --
>>>
>>> /tmp/vect1/app/Main.hs:31:15: Couldn't match type ‘n’ with ‘1 + (n - 1)’
>>> …
>>>       ‘n’ is a rigid type variable bound by
>>>           the instance declaration at /tmp/vect1/app/Main.hs:27:10
>>>     Expected type: Scalar n a
>>>       Actual type: Scalar (1 + (n - 1)) a
>>>     Relevant bindings include
>>>       xs :: Scalar (n - 1) a (bound at /tmp/vect1/app/Main.hs:30:5)
>>>       get :: Get (Scalar n a) (bound at /tmp/vect1/app/Main.hs:28:3)
>>>     In the second argument of ‘($!)’, namely ‘Cons x xs’
>>>     In a stmt of a 'do' block: return $! Cons x xs
>>> Compilation failed.
>>>
>>> - baojun
>>>
>> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160502/cc21b954/attachment.html>