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

[Baojun Wang]

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

[Carter Schonwald]

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. 

[Mitchell Rosen]

I think Carter is referring to this: http://hackage.haskell.org/package/ghc-typelits-natnormalise

[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

_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

[Baojun Wang]

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

[Kosyrev Serge]

Baojun Wang <wan...@gmail.com> 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]

Yeah the error message was really confusing. Install z3 solver fixed the issue.

- baojun