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 < lemm...@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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
