cannot perform arithmetic with GHC.TypeLits?

Baojun Wang

30 Apr 2016 30 Apr '16

2:43 a.m.

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

Attachments:

attachment.html (text/html — 2.4 KB)

Show replies by date

Carter Schonwald

30 Apr 30 Apr

8:34 a.m.

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

Mitchell Rosen

1 May 1 May

1:54 p.m.

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 javascript:> 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

Richard Eisenberg

2 May 2 May

10:05 a.m.

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

Baojun Wang

1:24 p.m.

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

Kosyrev Serge

1:47 p.m.

Baojun Wang writes:

...

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)

These runInteractiveProcess errors are *notoriously* unintelligible, reliably confusing every single person seeing them for the first time.. In this case the 'z3' executable is missing -- most likely due to the Z3 solver not installed on your machine. -- с уважениeм / respectfully, Косырев Сергей

Baojun Wang

2:36 p.m.

Yeah the error message was really confusing. Install z3 solver fixed the issue. - baojun On Mon, May 2, 2016 at 10:47 AM Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:

...

Baojun Wang writes:

...
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)

These runInteractiveProcess errors are *notoriously* unintelligible, reliably confusing every single person seeing them for the first time..

In this case the 'z3' executable is missing -- most likely due to the Z3 solver not installed on your machine.

-- с уважениeм / respectfully, Косырев Сергей

3306

Age (days ago)

3308

Last active (days ago)

List overview

Download

6 comments

5 participants

participants (5)

Baojun Wang
Carter Schonwald
Kosyrev Serge
Mitchell Rosen
Richard Eisenberg