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

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