type-unary 0.1.12 → 0.1.13
raw patch · 3 files changed
+28/−4 lines, 3 filesdep ~basePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base
API changes (from Hackage documentation)
+ TypeUnary.Vec: instance (IsNat n, Monoid a) => Monoid (Vec n a)
Files
- src/TypeUnary/Nat.hs +4/−1
- src/TypeUnary/Vec.hs +23/−2
- type-unary.cabal +1/−1
src/TypeUnary/Nat.hs view
@@ -36,7 +36,7 @@ import TypeUnary.TyNat --- Natural numbers+-- Natural numbers in unary form, built from zero & successor data Nat :: * -> * where Zero :: Nat Z Succ :: IsNat n => Nat n -> Nat (S n)@@ -117,6 +117,9 @@ -- | A number under the given limit, with proof data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)++-- TODO: Consider removing the Nat n field, since it's computable from+-- IsNat n or n :<: lim. instance Eq (Index lim) where Index _ n == Index _ n' = isJust (n `natEq` n')
src/TypeUnary/Vec.hs view
@@ -38,6 +38,7 @@ -- #include "Typeable.h" +import Data.Monoid (Monoid(..)) import Control.Applicative (Applicative(..),liftA2,(<$>)) import Data.Foldable (Foldable(..),toList,sum) import Data.Traversable (Traversable(..))@@ -59,8 +60,8 @@ -- | Vectors with type-determined length, having empty vector ('ZVec') and -- vector cons ('(:<)'). data Vec :: * -> * -> * where- ZVec :: Vec Z a -- -- ^ zero vector- (:<) :: a -> Vec n a -> Vec (S n) a -- -- ^ vector cons+ ZVec :: Vec Z a + (:<) :: a -> Vec n a -> Vec (S n) a -- | Type-safe head for vectors headV :: Vec (S n) a -> a@@ -121,6 +122,11 @@ -- do: check whether this change broke Shady's code generation. Maybe not, -- if the code generation uses Pretty instead of Show. +-- The Monoid instance uses a standard recipe for applicative functors.+instance (IsNat n, Monoid a) => Monoid (Vec n a) where+ mempty = pure mempty+ mappend = liftA2 mappend+ instance Functor (Vec n) where fmap _ ZVec = ZVec fmap f (a :< u) = f a :< fmap f u@@ -167,6 +173,7 @@ traverse _ ZVec = pure ZVec traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as) + instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate } @@ -178,6 +185,10 @@ -- u <.> v = vec1 (sum (liftA2 (*) u v)) (<.>) = (result.result) (vec1 . sum) (liftA2 (*)) +-- TODO: Rethink the previous three instances. Maybe replace the Num+-- constraints with AdditiveGroup, VectorSpace, and InnerSpace.+-- And why Vec1 for Scalar?+ instance (IsNat n, Storable a) => Storable (Vec n a) where sizeOf = const (fromIntegral (natToZ (nat :: Nat n)) * sizeOf (undefined :: a))@@ -294,6 +305,16 @@ -- | Extract elements un4 :: Vec4 a -> (a,a,a,a) un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)++-- TODO: consider this notation:+--+-- infixr 5 :<+-- (<|) :: a -> a -> Vec2 a+-- (<|) = vec2+-- +-- So we can say things like+-- +-- a :< b <| c {-------------------------------------------------------------------- Extract and set elements
type-unary.cabal view
@@ -1,5 +1,5 @@ Name: type-unary-Version: 0.1.12+Version: 0.1.13 Cabal-Version: >= 1.2 Synopsis: Type-level and typed unary natural numbers, inequality proofs, vectors