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

2 May 2016

      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  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 
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  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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe