type-unary 0.2.19 → 0.2.21
raw patch · 2 files changed
+7/−4 lines, 2 filesdep ~basePVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: base
API changes (from Hackage documentation)
- TypeUnary.Nat: SLess :: m :<: n -> S m :<: S n
- TypeUnary.Nat: Succ :: Nat n -> Nat (S n)
- TypeUnary.Nat: ZLess :: Z :<: S n
- TypeUnary.Nat: Zero :: Nat Z
- TypeUnary.Nat: instance (n :+: Z) ~ n => PlusZero n
- TypeUnary.Nat: instance Eq (Index lim)
- TypeUnary.Nat: instance IsNat Z
- TypeUnary.Nat: instance IsNat n => IsNat (S n)
- TypeUnary.Nat: instance IsNat n => Num (Index n)
- TypeUnary.Nat: instance Show (Index n)
- TypeUnary.Nat: instance Show (Nat n)
- TypeUnary.TyNat: instance Typeable S
- TypeUnary.TyNat: instance Typeable Z
- TypeUnary.Vec: (:<) :: a -> Vec n a -> Vec (S n) a
- TypeUnary.Vec: ZVec :: Vec Z a
- TypeUnary.Vec: instance (IsNat n, Enum applicative_arg) => Enum (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Floating applicative_arg) => Floating (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Fractional applicative_arg) => Fractional (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Integral applicative_arg) => Integral (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Monoid a) => Monoid (Vec n a)
- TypeUnary.Vec: instance (IsNat n, Num a) => AdditiveGroup (Vec n a)
- TypeUnary.Vec: instance (IsNat n, Num a) => InnerSpace (Vec n a)
- TypeUnary.Vec: instance (IsNat n, Num a) => VectorSpace (Vec n a)
- TypeUnary.Vec: instance (IsNat n, Num applicative_arg) => Num (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Num applicative_arg, Ord applicative_arg) => Real (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, RealFloat applicative_arg) => RealFloat (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, RealFrac applicative_arg) => RealFrac (Vec n applicative_arg)
- TypeUnary.Vec: instance (IsNat n, Storable a) => Storable (Vec n a)
- TypeUnary.Vec: instance Eq a => Eq (Vec n a)
- TypeUnary.Vec: instance Foldable (Vec n)
- TypeUnary.Vec: instance Functor (Vec n)
- TypeUnary.Vec: instance IsNat n => Applicative (Vec n)
- TypeUnary.Vec: instance IsNat n => Monad (Vec n)
- TypeUnary.Vec: instance IsNat n => ToVec [a] n a
- TypeUnary.Vec: instance Newtype (Vec (S n) a) (a, Vec n a)
- TypeUnary.Vec: instance Newtype (Vec Z a) ()
- TypeUnary.Vec: instance Ord a => Ord (Vec n a)
- TypeUnary.Vec: instance Show a => Show (Vec n a)
- TypeUnary.Vec: instance ToVec (Vec n a) n a
- TypeUnary.Vec: instance Traversable (Vec n)
- TypeUnary.Vec: instance Typeable Vec
+ TypeUnary.Nat: [SLess] :: m :<: n -> S m :<: S n
+ TypeUnary.Nat: [Succ] :: IsNat n => Nat n -> Nat (S n)
+ TypeUnary.Nat: [ZLess] :: Z :<: S n
+ TypeUnary.Nat: [Zero] :: Nat Z
+ TypeUnary.Nat: instance (n TypeUnary.TyNat.:+: TypeUnary.TyNat.Z) ~ n => TypeUnary.Nat.PlusZero n
+ TypeUnary.Nat: instance GHC.Classes.Eq (TypeUnary.Nat.Index lim)
+ TypeUnary.Nat: instance GHC.Show.Show (TypeUnary.Nat.Index n)
+ TypeUnary.Nat: instance GHC.Show.Show (TypeUnary.Nat.Nat n)
+ TypeUnary.Nat: instance TypeUnary.Nat.IsNat TypeUnary.TyNat.Z
+ TypeUnary.Nat: instance TypeUnary.Nat.IsNat n => GHC.Num.Num (TypeUnary.Nat.Index n)
+ TypeUnary.Nat: instance TypeUnary.Nat.IsNat n => TypeUnary.Nat.IsNat (TypeUnary.TyNat.S n)
+ TypeUnary.Vec: [:<] :: a -> Vec n a -> Vec (S n) a
+ TypeUnary.Vec: [ZVec] :: Vec Z a
+ TypeUnary.Vec: infixl 1 <+>
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, Foreign.Storable.Storable a) => Foreign.Storable.Storable (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Base.Monoid a) => GHC.Base.Monoid (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Enum.Enum applicative_arg) => GHC.Enum.Enum (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Float.Floating applicative_arg) => GHC.Float.Floating (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Float.RealFloat applicative_arg) => GHC.Float.RealFloat (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Num.Num a) => Data.AdditiveGroup.AdditiveGroup (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Num.Num a) => Data.VectorSpace.InnerSpace (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Num.Num a) => Data.VectorSpace.VectorSpace (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Num.Num applicative_arg) => GHC.Num.Num (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Num.Num applicative_arg, GHC.Classes.Ord applicative_arg) => GHC.Real.Real (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Real.Fractional applicative_arg) => GHC.Real.Fractional (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Real.Integral applicative_arg) => GHC.Real.Integral (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance (TypeUnary.Nat.IsNat n, GHC.Real.RealFrac applicative_arg) => GHC.Real.RealFrac (TypeUnary.Vec.Vec n applicative_arg)
+ TypeUnary.Vec: instance Control.Newtype.Newtype (TypeUnary.Vec.Vec (TypeUnary.TyNat.S n) a) (a, TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance Control.Newtype.Newtype (TypeUnary.Vec.Vec TypeUnary.TyNat.Z a) ()
+ TypeUnary.Vec: instance Data.Foldable.Foldable (TypeUnary.Vec.Vec n)
+ TypeUnary.Vec: instance Data.Traversable.Traversable (TypeUnary.Vec.Vec n)
+ TypeUnary.Vec: instance GHC.Base.Functor (TypeUnary.Vec.Vec n)
+ TypeUnary.Vec: instance GHC.Classes.Eq a => GHC.Classes.Eq (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance GHC.Classes.Ord a => GHC.Classes.Ord (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance GHC.Show.Show a => GHC.Show.Show (TypeUnary.Vec.Vec n a)
+ TypeUnary.Vec: instance TypeUnary.Nat.IsNat n => GHC.Base.Applicative (TypeUnary.Vec.Vec n)
+ TypeUnary.Vec: instance TypeUnary.Nat.IsNat n => GHC.Base.Monad (TypeUnary.Vec.Vec n)
+ TypeUnary.Vec: instance TypeUnary.Nat.IsNat n => TypeUnary.Vec.ToVec [a] n a
+ TypeUnary.Vec: instance TypeUnary.Vec.ToVec (TypeUnary.Vec.Vec n a) n a
- TypeUnary.Nat: induction :: p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> (forall n. IsNat n => Dict (p n))
+ TypeUnary.Nat: induction :: forall p. p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> (forall n. IsNat n => Dict (p n))
- TypeUnary.Nat: natMul :: Nat m -> Nat n -> Nat (m :*: n)
+ TypeUnary.Nat: natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
- TypeUnary.Nat: natToZ :: (Enum a, Num a) => Nat n -> a
+ TypeUnary.Nat: natToZ :: Num a => Nat n -> a
Files
- src/TypeUnary/Nat.hs +6/−3
- type-unary.cabal +1/−1
src/TypeUnary/Nat.hs view
@@ -1,8 +1,9 @@ {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-} --- Experiment+-- PlusZero Experiment {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP #-} {-# OPTIONS_GHC -Wall #-}@@ -88,9 +89,10 @@ -} -- | Interpret a 'Nat' as a plain number-natToZ :: (Enum a, Num a) => Nat n -> a+natToZ :: Num a => Nat n -> a natToZ Zero = 0-natToZ (Succ n) = (succ . natToZ) n+natToZ (Succ n) = ((1+) . natToZ) n+{-# INLINE natToZ #-} -- | Equality test natEq :: Nat m -> Nat n -> Maybe (m :=: n)@@ -137,6 +139,7 @@ go Zero = Dict go (Succ m) = s (go m) +-- Needs UndecidableInstances in GHC 7.6.3, though not in 7.8.2 class (n :+: Z) ~ n => PlusZero n instance (n :+: Z) ~ n => PlusZero n
type-unary.cabal view
@@ -1,5 +1,5 @@ Name: type-unary-Version: 0.2.19+Version: 0.2.21 Cabal-Version: >= 1.6 Synopsis: Type-level and typed unary natural numbers, inequality proofs, vectors