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

[Richard Eisenberg]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160502/fd225615/attachment.html>