Re: positive type-level naturals

16 Mar 2014


      Iavor is working on a branch that allows the constraint solver to call an
external solver: https://github.com/ghc/ghc/tree/decision-procedure
Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly
out of of line with HEAD.
I think the above branch will be able to solve things like: 1 <= n + 1 ~
True

I myself worked on a patch that can only work with equalities:
https://gist.github.com/christiaanb/8396614
It allows you to solve both more and less constraints than Iavor's CVC4
approach:
More: It can deal with non-constant multiplications, and also with
exponentials
Less: It cannot deal with inequalities


On Sun, Mar 16, 2014 at 1:44 PM, Henning Thielemann <
lemming@henning-thielemann.de> wrote:
...
Am 16.03.2014 09:40, schrieb Christiaan Baaij:
To answer the second question (under the assumption that you want
...
phantom-type style Vectors and not GADT-style):
Now I like to define non-empty vectors. The phantom parameter for the
length shall refer to the actual vector length, not to length-1, for
consistency between possibly empty and non-empty vectors.
I have modified your code as follows:
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module PositiveNat where
import Data.Proxy (Proxy(Proxy))
import GHC.TypeLits
          (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal,
           type (<=), type (+))
data Vector (n :: Nat) a = Vector a [a]
withVector ::
   forall a b.
   a -> [a] ->
   (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b
withVector x xs f =
   case someNatVal $ toInteger $ length xs of
      Nothing -> error "static/dynamic mismatch"
      Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)
vecLen :: forall n . KnownNat n => Vector n Integer -> Integer
vecLen _ = natVal (Proxy :: Proxy n)
-- > withVector vecLen [1,2,3,4]
-- 4
GHC-7.8 complains with:
PositiveNat.hs:23:40:
    Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True)
    from the context (KnownNat n)
      bound by a pattern with constructor
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n ->
SomeNat,
               in a case alternative
      at PositiveNat.hs:23:13-34
    In the expression: f (Vector x xs :: Vector (m + 1) a)
    In a case alternative:
        Just (SomeNat (_ :: Proxy m))
          -> f (Vector x xs :: Vector (m + 1) a)
    In the expression:
      case someNatVal $ toInteger $ length xs of {
        Nothing -> error "static/dynamic mismatch"
        Just (SomeNat (_ :: Proxy m))
          -> f (Vector x xs :: Vector (m + 1) a) }
How can I convince GHC that n+1 is always at least 1?
When I remove the (1<=n) constraint, I still get:
PositiveNat.hs:23:40:
    Could not deduce (KnownNat (n + 1)) arising from a use of 'f'
    from the context (KnownNat n)
      bound by a pattern with constructor
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n ->
SomeNat,
               in a case alternative
      at PositiveNat.hs:23:13-34
    In the expression: f (Vector x xs :: Vector (m + 1) a)
    In a case alternative:
        Just (SomeNat (_ :: Proxy m))
          -> f (Vector x xs :: Vector (m + 1) a)
    In the expression:
      case someNatVal (toInteger (length xs)) of {
        Nothing -> error "static/dynamic mismatch"
        Just (SomeNat (_ :: Proxy m))
          -> f (Vector x xs :: Vector (m + 1) a) }
That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is
also KnownNat. How to do that?