positive type-level naturals

[Iavor Diatchki]

Hi Henning,

I see two separate issues that show in what you describe, so it might be
useful to discuss them separately:

1. The first issue is figuring out that `n  + 1` is always at least 1.  As
others have mentioned, GHC currently only does proofs "by evaluation",
which is why it gets stuck here.  We are working on connecting more
sophisticated decision procedures with GHC's type checker, and they seem to
work fairly well for these kinds of problems.

2. The second one is about: `KnownNat (n  + 1)`, and should this be implied
by `KnownNat n`, which is more of a design choice.   The current thinking
is that `KnownNat n` asserts that `n` is a concrete number (i.e., a
literal).  So having a `KnownNat` constraint is like having an extra
integer parameter, which is always evaluated, and never a thunk.  Now, `(n
+ 1)` is not a literal, which is why `KnowNat (n + 1)` is not solved.    I
think that it would be entirely possible to add more rules for solving
`KnownNat` constraints but there are trade offs.  For example, consider the
following two types:

f1 :: KnownNat (a + b) => ...
f2 :: (KnownNat a, KnownNat b) => ...

The first function will take a single integer parameter, while the second
one will take two, and then add them, which seems like more work.  Of
course, one might hope that in some cases GHC will optimize this away, so
maybe this is not much of an issue.

Then, there is the issue about situations like this:

f3 :: (a + b ~ c, x + y ~ c, KnownNat c) => ...

If we apply the same thinking, we could replace `KnownNat c` with either
`(KnowNat a, KnownNat b)` or with `(KnownNat x, KnownNat y)` and it is not
clear what is the right choice.  Similarly, it is not clear if `KnowNat (a
* b)`, should be replaced by `(KnownNat a, KnownNat b)`:  what if `a` was
0, then we shouldn't need the `KnowNat b` constraint at all.

It is also possible to compromise:  maybe we should simplify things like
`KnownNat (x + 1)` and `KnownNat (x * 2)`, because these do not increase
the number of constraints, and there is never the possibility of ambiguity?
 This might be an interesting direction to explore...


A general comment:  the function `withVec` is fairly tricky because it
introduces vectors whose length is not known statically.  This tends to
require much more advanced tools because one has to do real mathematical
reasoning about abstract values.  Of course, sometimes there is no way
around this, but on occasion one can avoid it.   For example, in the
expression `withVec 1 [2,3,4]` we know exactly the length of the vectors
involved, so there is no reason to resort to using fancy reasoning.  The
problem is that Haskell's list notation does not tell us the length of the
list literal.  One could imagine writing a little quasi-quoter that will
allow us to write things like `[vec| 1, 2, 3, 4]`, which would generate the
correctly sized vector. Then you can append and manipulate these as usual
and GHC will be able to check the types because it only has to work with
concrete numbers.  This is not a great program verification technique, but
it certainly beats having to do it manually :-)

I hope this helps,
-Iavor




















On Sun, Mar 16, 2014 at 5:44 AM, 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/20140319/59cf8dd7/attachment.html>