[Haskell-cafe] cannot perform arithmetic with GHC.TypeLits?
Baojun Wang
wangbj at gmail.com
Mon May 2 17:24:34 UTC 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 <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>
More information about the Haskell-Cafe
mailing list