type-unary 0.2.16 → 0.2.19

raw patch · 3 files changed

+101/−33 lines, 3 filesdep +constraintsdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: constraints

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• src/TypeUnary/Nat.hs +30/−9
• src/TypeUnary/Vec.hs +69/−23
• type-unary.cabal +2/−1

@@ -1,6 +1,10 @@ {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-}++-- Experiment+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP #-}+ {-# OPTIONS_GHC -Wall #-} ---------------------------------------------------------------------- -- |@@ -18,11 +22,12 @@   (     module TypeUnary.TyNat   -- * Value-typed natural numbers-  , Nat(..), zero, one, two, three, four+  , Nat(..), predN, zero, one, two, three, four   , withIsNat, natSucc, natIsNat   , natToZ, natEq, natAdd, natMul   , IsNat(..)   , induction+  , PlusZero, plusZero   -- * Inequality proofs and indices   , (:<:)(..), succLim   , Index(..), unIndex, succI, index0, index1, index2, index3@@ -37,6 +42,8 @@ import Data.Maybe (isJust) import Data.Typeable (Typeable) +import Data.Constraint (Dict(..))+ import Data.Proof.EQ  import TypeUnary.TyNat@@ -61,6 +68,9 @@ natIsNat Zero     = Zero natIsNat (Succ n) = Succ n +predN :: Nat (S n) -> Nat n+predN (Succ n) = n+ {-  -- Another approach (also works):@@ -118,17 +128,28 @@ -- from IsNat.  -- | Peano's induction principle-induction :: forall p. -             p Z -> (forall n. IsNat n => p n -> p (S n))-          -> (forall n. IsNat n => p n)-induction z s = go nat+induction :: forall p . +             p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n)))+          -> (forall n. IsNat n => Dict (p n))+induction s = go nat  where-   -- morphism over z & s.-   go :: forall n. Nat n -> p n-   go Zero     = z+   go :: forall n. Nat n -> Dict (p n)+   go Zero     = Dict    go (Succ m) = s (go m) --- TODO: Use induction for n + Z == n. Then associativity and commutativity.+class    (n :+: Z) ~ n => PlusZero n+instance (n :+: Z) ~ n => PlusZero n++plusZero :: IsNat n => Dict (PlusZero n)+plusZero = induction (\ Dict -> Dict)++#if 0+class    ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r+instance ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r++plusAssocR :: (IsNat p, IsNat q, IsNat r) => Dict (PlusAssocR p q r)+plusAssocR ...+#endif  {--------------------------------------------------------------------     Inequality proofs

@@ -45,7 +45,7 @@  import Prelude hiding (foldr,sum,and) -import Data.Monoid (Monoid(..))+import Data.Monoid (Monoid(..),(<>)) import Control.Applicative (Applicative(..),liftA2,(<$>)) import Data.Foldable (Foldable(..),toList,sum) -- ,and import Data.Traversable (Traversable(..))@@ -56,6 +56,8 @@  import Control.Newtype (Newtype(..)) +-- import Data.Constraint+ import Data.VectorSpace  import TypeUnary.Nat@@ -176,25 +178,41 @@   {-# INLINE fmap #-}  instance IsNat n => Applicative (Vec n) where-  pure  = pureV-  (<*>) = applyV+  pure  = pureV nat+  (<*>) = applyV nat+  {-# INLINE pure  #-}+  {-# INLINE (<*>) #-} -pureV :: IsNat n => a -> Vec n a-pureV = pureV' nat+pureV :: Nat n -> a -> Vec n a+pureV Zero     _ = ZVec+pureV (Succ n) a = a :< pureV n a+{-# INLINE pureV #-} -pureV' :: Nat n -> a -> Vec n a-pureV' Zero     _ = ZVec-pureV' (Succ n) a = a :< pureV' n a+-- Experiment -applyV :: Vec n (a -> b) -> Vec n a -> Vec n b-ZVec      `applyV` ZVec      = ZVec-(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)-_ `applyV` _ = cant "applyV"+inVecS :: ((a, Vec n a) -> (b, Vec n b)) -> (Vec (S n) a -> Vec (S n) b)+inVecS f = uncurry (:<) . f . unConsV --- Without -fno-warn-incomplete-patterns above,--- the previous two instances lead to warnings about non-exhaustive--- pattern matches, although the other possibilities--- are type-incorrect.  According to SLPJ:+inVecS2 :: ((a, Vec n a) -> (b, Vec n b) -> (c, Vec n c))+        -> (Vec (S n) a  -> Vec (S n) b  -> Vec (S n) c )+inVecS2 f = inVecS . f . unConsV++-- TODO: reconcile unConsV vs unVecS++applyV :: Nat n -> Vec n (a -> b) -> Vec n a -> Vec n b+applyV Zero     = \ _      _      -> ZVec+applyV (Succ n) = inVecS2 (\ (f,fs) (x,xs) -> (f x , applyV n fs xs))+{-# INLINE applyV #-}++-- applyV :: Nat n -> Vec n (a -> b) -> Vec n a -> Vec n b+-- applyV Zero     = \ ZVec      ZVec      -> ZVec+-- applyV (Succ n) = \ (f :< fs) (x :< xs) -> f x :< applyV n fs xs+-- {-# INLINE applyV #-}++-- The "= \ ..." form here side-steps the incomplete patterns warning without+-- -fno-warn-incomplete-patterns above. Otherwise we get warnings about+-- non-exhaustive pattern matches, although the other possibilities are+-- type-incorrect. Once upon a time SLPJ said --  --   The overlap warning checker simply doesn't take account of GADTs. --   There's a long-standing project suggestion to fix this:@@ -212,9 +230,9 @@ joinV _ = cant "joinV"  instance Foldable (Vec n) where-  foldr _  b ZVec     = b-  foldr h b (a :< as) = a `h` foldr h b as-  {-# INLINE foldr #-}+  foldMap _ ZVec      = mempty+  foldMap h (a :< as) = h a <> foldMap h as+  {-# INLINE foldMap #-}  instance Traversable (Vec n) where   traverse _ ZVec      = pure ZVec@@ -539,16 +557,42 @@ --  -- Won't type-check without commutativity of addition. :( -{-+#if 0 +addZ :: IsNat n => Dict (n ~ (n :+: Z))+addZ = addZ' nat++addZ' :: Nat n -> Dict (n ~ (n :+: Z))+addZ' Zero                       = Dict+addZ' (Succ m) | Dict <- addZ' m = Dict++add1 :: IsNat m => Dict ((m :+: S Z) ~ S m)+add1 = add1' nat++add1' :: Nat m -> Dict ((m :+: S Z) ~ S m)+add1' Zero                       = Dict+add1' (Succ m) | Dict <- add1' m = Dict++-- addS :: (IsNat m, IsNat n) => Dict ((m :+: S n) ~ S (m :+: n))+-- addS = addS' nat++addS' :: IsNat m => Nat n -> Dict ((m :+: S n) ~ S (m :+: n))+addS' Zero | Dict <- add1 = Dict+...++-- Oops: non-injectivity+ -- Reversal. Thinking about this one. Currently thwarted by missing -- knowledge about numbers in the type-checker. Would be easy with -- built-in type-level naturals.  -- | Reverse a vector-reverseV :: Vec n a -> Vec n a-reverseV = reverse' nat ZVec+reverseV :: forall n a. IsNat n => Vec n a -> Vec n a+reverseV | Dict <- (addZ :: Dict (n ~ (n :+: Z))) = reverse' nat ZVec +-- reverseV :: Vec n a -> Vec n a+-- reverseV = reverse' nat ZVec+ --  Couldn't match type `n' with `n :+: Z'  -- Reverse na and append to ma@@ -557,7 +601,7 @@ reverse' (Succ n) ma (a :< as) = reverse' n (a :< ma) as  -- Could not deduce ((n1 :+: S m) ~ S (n1 :+: m))--}+#endif  -- | Delete exactly one occurrence of an element from a vector, raising an -- error if the element isn't present.@@ -646,11 +690,13 @@  instance IsNat n => ToVec [a] n a where   toVec = toVecL nat+  {-# INLINE toVec #-}  toVecL :: Nat n -> [a] -> Vec n a toVecL Zero [] = ZVec toVecL (Succ m) (a:as) = a :< toVecL m as toVecL _ _ = error "toVecL: length mismatch"+{-# INLINE toVecL #-}  {--------------------------------------------------------------------     Misc

@@ -1,5 +1,5 @@ Name:                type-unary-Version:             0.2.16+Version:             0.2.19 Cabal-Version:       >= 1.6 Synopsis:               Type-level and typed unary natural numbers, inequality proofs, vectors@@ -26,6 +26,7 @@   hs-Source-Dirs:      src   Extensions:   Build-Depends:       base >=4 && < 5+                     , constraints                      , newtype >= 0.2                      , ty >= 0.1.5                      , vector-space