packages feed

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 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