<div dir="ltr">Hi Henning,<div><br></div><div>I see two separate issues that show in what you describe, so it might be useful to discuss them separately:</div><div><br></div><div>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.</div>
<div><br></div><div>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:</div>
<div><br></div><div>f1 :: KnownNat (a + b) => ...</div><div>f2 :: (KnownNat a, KnownNat b) => ...</div><div><br></div><div>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.</div>
<div><br></div><div>Then, there is the issue about situations like this:</div><div><br></div><div>f3 :: (a + b ~ c, x + y ~ c, KnownNat c) => ...</div><div> </div><div>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.</div>
<div><br></div><div>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...</div>
<div><br></div><div><br></div><div>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 :-)</div>
<div><br></div><div>I hope this helps,</div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div> </div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div>
<div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Mar 16, 2014 at 5:44 AM, Henning Thielemann <span dir="ltr"><<a href="mailto:lemming@henning-thielemann.de" target="_blank">lemming@henning-thielemann.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Am 16.03.2014 09:40, schrieb Christiaan Baaij:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
To answer the second question (under the assumption that you want<br>
phantom-type style Vectors and not GADT-style):<br>
</blockquote>
<br>
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.<br>
<br>
I have modified your code as follows:<br>
<br>
{-# LANGUAGE Rank2Types #-}<br>
{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE KindSignatures #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE TypeFamilies #-}<br>
module PositiveNat where<br>
<br>
import Data.Proxy (Proxy(Proxy))<br>
import GHC.TypeLits<br>
          (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal,<br>
           type (<=), type (+))<br>
<br>
data Vector (n :: Nat) a = Vector a [a]<br>
<br>
withVector ::<br>
   forall a b.<br>
   a -> [a] -><br>
   (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b<br>
withVector x xs f =<br>
   case someNatVal $ toInteger $ length xs of<br>
      Nothing -> error "static/dynamic mismatch"<br>
      Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)<br>
<br>
vecLen :: forall n . KnownNat n => Vector n Integer -> Integer<br>
vecLen _ = natVal (Proxy :: Proxy n)<br>
<br>
-- > withVector vecLen [1,2,3,4]<br>
-- 4<br>
<br>
<br>
GHC-7.8 complains with:<br>
<br>
PositiveNat.hs:23:40:<br>
    Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True)<br>
    from the context (KnownNat n)<br>
      bound by a pattern with constructor<br>
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,<br>
               in a case alternative<br>
      at PositiveNat.hs:23:13-34<br>
    In the expression: f (Vector x xs :: Vector (m + 1) a)<br>
    In a case alternative:<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a)<br>
    In the expression:<br>
      case someNatVal $ toInteger $ length xs of {<br>
        Nothing -> error "static/dynamic mismatch"<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a) }<br>
<br>
<br>
How can I convince GHC that n+1 is always at least 1?<br>
<br>
<br>
When I remove the (1<=n) constraint, I still get:<br>
<br>
PositiveNat.hs:23:40:<br>
    Could not deduce (KnownNat (n + 1)) arising from a use of ‘f’<br>
    from the context (KnownNat n)<br>
      bound by a pattern with constructor<br>
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,<br>
               in a case alternative<br>
      at PositiveNat.hs:23:13-34<br>
    In the expression: f (Vector x xs :: Vector (m + 1) a)<br>
    In a case alternative:<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a)<br>
    In the expression:<br>
      case someNatVal (toInteger (length xs)) of {<br>
        Nothing -> error "static/dynamic mismatch"<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a) }<br>
<br>
That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is also KnownNat. How to do that?<br>
<br>
______________________________<u></u>_________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.<u></u>org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/glasgow-<u></u>haskell-users</a><br>
</blockquote></div><br></div>