positive type-level naturals
Christiaan Baaij
christiaan.baaij at gmail.com
Sun Mar 16 15:06:10 UTC 2014
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>
More information about the Glasgow-haskell-users
mailing list