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

[Mitchell Rosen]

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 <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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160501/8be237fd/attachment.html>