respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).
For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type lits". Heres what I'd like to happen for 7.10, and i'm happy to help / pester this along 1) Typelits as it currently exists in GHC actually conflates "syntactic support" for Nats with having primacy as the "nat" type for ghc. I think we should seriously consider moving in a direction akin to how Agda provides syntactic/ computational support for efficient / 2) the current typelits supplied Nat is kinda crippled because we can't do userland reasoning / compute on it, I consider this a bug! I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver! i think (1) and some part of (2) should happen for 7.10. What design work / subtleties might block it? On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij < christiaan.ba...@gmail.com> wrote: > 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 > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
