[prev in list] [next in list] [prev in thread] [next in thread]
List: haskell-cafe
Subject: Re: [Haskell-cafe] cannot perform arithmetic with GHC.TypeLits?
From: Carter Schonwald <carter.schonwald () gmail ! com>
Date: 2016-04-30 12:34:56
Message-ID: CAHYVw0wugqrHDqJSb7=da9G=CTF7ww3eA5qBepYBfqykNDm1pQ () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
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 <wangbj@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
>
[Attachment #5 (text/html)]
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. <div><br></div><div>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. <span></span><br><br>On Saturday, April 30, \
2016, Baojun Wang <<a href="mailto:wangbj@gmail.com">wangbj@gmail.com</a>> \
wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px \
#ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hi \
List,</div><div><br></div><div>When I try to build below program, the compiler \
complains </div><div><br></div><div> Couldn't match type ‘n' with ‘1 + (n \
- 1)' …<br></div><div><br></div><div>Why GHC (7.10.3) cannot do type level natural \
number arithmetic? `` n /= 1 + (n-1)`` at type level?</div><div><br></div><div>-- | \
main.hs</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE \
FlexibleInstances #-}</div><div>{-# LANGUAGE GADTs #-}</div><div>{-# LANGUAGE \
PolyKinds #-}</div><div>{-# LANGUAGE KindSignatures #-}</div><div>{-# LANGUAGE \
TypeOperators #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE \
OverloadedStrings #-}</div><div>{-# LANGUAGE DeriveGeneric \
#-}</div><div><br></div><div>module Main where</div><div><br></div><div>import \
qualified Data.ByteString as B</div><div>import \
Data.ByteString(ByteString)</div><div>import Data.Serialize -- require \
cereal</div><div><br></div><div>import GHC.TypeLits</div><div><br></div><div>data \
Scalar :: Nat -> * -> * where</div><div> Nil :: Scalar 0 a</div><div> Cons \
:: a -> Scalar m a -> Scalar (1+m) a</div><div><br></div><div>instance \
(Serialize a) => Serialize (Scalar 0 a) where</div><div> get = return \
Nil</div><div> put _ = return $ mempty</div><div><br></div><div>instance (Serialize \
a) => Serialize (Scalar n a) where</div><div> get = do</div><div> x <- \
get :: Get a</div><div> xs <- get :: Get (Scalar (n-1) a)</div><div> \
return $! Cons x xs</div><div> put (Cons x xs) = do</div><div> put (x :: \
a)</div><div> put \
xs</div><div><br></div></div><div>--</div><div><br></div><div>/tmp/vect1/app/Main.hs:31:15: \
Couldn't match type ‘n' with ‘1 + (n - 1)' …</div><div> ‘n' is a \
rigid type variable bound by</div><div> the instance declaration at \
/tmp/vect1/app/Main.hs:27:10</div><div> Expected type: Scalar n a</div><div> \
Actual type: Scalar (1 + (n - 1)) a</div><div> Relevant bindings \
include</div><div> xs :: Scalar (n - 1) a (bound at \
/tmp/vect1/app/Main.hs:30:5)</div><div> get :: Get (Scalar n a) (bound at \
/tmp/vect1/app/Main.hs:28:3)</div><div> In the second argument of ‘($!)', \
namely ‘Cons x xs'</div><div> In a stmt of a 'do' block: return $! \
Cons x xs</div><div>Compilation failed.</div><div><br></div><div>- baojun</div></div> \
</blockquote></div>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic