positive type-level naturals

[Carter Schonwald]

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 <lemming at 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?
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140316/759b3f7e/attachment-0001.html>