positive type-level naturals

[Christiaan Baaij]

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 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?
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140316/4c4367d3/attachment-0001.html>