Re: positive type-level naturals

16 Mar 2014

      You can't with type lits. The solver can only decide concrete values :"""(

You'll have to use a concrete peano Nats type instead.

I've been toying with the idea that the type lits syntax should be just
that, a type level analogue of from integer that you can give to user land
types, but I'm not going to suggest that till 7.8 is fully released.

On Sunday, March 16, 2014, Henning Thielemann 
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?
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: positive type-level naturals

Carter Schonwald