type-combinators 0.2.1.0 → 0.2.2.0

raw patch · 11 files changed

+120/−37 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• src/Data/Type/Boolean.hs +6/−3
• src/Data/Type/Conjunction.hs +6/−3
• src/Data/Type/Disjunction.hs +12/−0
• src/Data/Type/Nat.hs +10/−0
• src/Data/Type/Nat/Inequality.hs +0/−14
• src/Data/Type/Quantifier.hs +40/−0
• src/Data/Type/Sym.hs +5/−0
• src/Type/Class/Witness.hs +16/−0
• src/Type/Family/Bool.hs +3/−16
• src/Type/Family/Nat.hs +21/−0
• type-combinators.cabal +1/−1

@@ -30,6 +30,7 @@  import Data.Type.Quantifier (Some(..)) import Type.Family.Bool+import Type.Family.Constraint import Type.Class.Known import Type.Class.Higher @@ -83,11 +84,13 @@ (<==>) = (.==) infixr 1 <==> -class BoolEq (f :: k -> *) where-  (.==) :: f a -> f b -> Boolean (a == b)+class BoolEquality (f :: k -> *) where+  type BoolEqC f (a :: k) (b :: k) :: Constraint+  type BoolEqC f a b = ØC+  (.==) :: BoolEqC f a b => f a -> f b -> Boolean (a == b) infix 4 .== -instance BoolEq Boolean where+instance BoolEquality Boolean where   (.==) = \case     False_ -> \case       False_ -> True_

@@ -36,6 +36,7 @@ import Type.Class.Known import Type.Class.Witness import Type.Family.Tuple+import Data.Type.Boolean  -- (:&:) {{{ @@ -79,9 +80,6 @@ curryFan :: ((f :&: g) a -> r) -> f a -> g a -> r curryFan f a b = f (a :&: b) -instance DecEquality f => DecEquality (f :&: g) where-  decideEquality (a :&: _) (c :&: _) = decideEquality a c- instance (Known f a, Known g a) => Known (f :&: g) a where   known = known :&: known @@ -158,6 +156,11 @@  _snd :: (a#b) :~: (c#d) -> b :~: d _snd Refl = Refl++{-+instance (BoolEquality f, BoolEquality g) => BoolEquality (f :*: g) where+  (a :*: b) .== (c :*: d) = a .== c .&& b .== d+-}  instance (DecEquality f, DecEquality g) => DecEquality (f :*: g) where   decideEquality (a :*: b) (c :*: d) = case decideEquality a c of

@@ -167,6 +167,18 @@     , (a,s2)    <- readsPrec1 11 s1     ] +{-+instance (DecEquality f, DecEquality g) => DecEquality (f :+: g) where+  decideEquality = \case+    L' a -> \case+      L' b -> decCase (decideEquality a b) (\Refl -> Proven Refl) (\contra -> Refuted $ contra . toEquality fromLeftCong)+      R' _ -> Refuted $+    R' a -> \case+      L' b -> Refuted undefined+      R' b -> undefined+-}++ (>+<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :+: g) e -> r f >+< g = \case   L' a -> f a

@@ -28,6 +28,7 @@  module Data.Type.Nat where +import Data.Type.Boolean import Data.Type.Equality import Data.Type.Quantifier import Type.Class.Higher@@ -84,6 +85,15 @@     S_ x -> \case       Z_   -> Nothing       S_ y -> testEquality x y //? qed++instance BoolEquality Nat where+  (.==) = \case+    Z_ -> \case+      Z_   -> True_+      S_ _ -> False_+    S_ x -> \case+      Z_   -> False_+      S_ y -> x .== y  pred' :: Nat (S x) -> Nat x pred' (S_ x) = x

@@ -21,20 +21,6 @@ import Type.Family.Constraint import Type.Family.Nat -type family (x :: N) < (y :: N) :: Bool where-  Z   < Z   = False-  Z   < S y = True-  S x < Z   = False-  S x < S y = x < y-infix 4 <--type family (x :: N) > (y :: N) :: Bool where-  Z   > Z   = False-  Z   > S y = False-  S x > Z   = True-  S x > S y = x > y-infix 4 >- data NatLT :: N -> N -> * where   LTZ :: NatLT Z (S y)   LTS :: !(NatLT x y)

@@ -69,6 +69,15 @@ onSome :: (forall a. f a -> g x) -> Some f -> Some g onSome f (Some a) = Some (f a) +msome :: Monad m => f a -> m (Some f)+msome = return . Some++(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r+m >>=- f = do+  s <- m+  s >>- f+infixl 1 >>=-+ -- }}}  -- Some2 {{{@@ -93,6 +102,15 @@ onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g onSome2 f (Some2 a) = Some2 (f a) +msome2 :: Monad m => f a b -> m (Some2 f)+msome2 = return . Some2++(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r+m >>=-- f = do+  s <- m+  s >>-- f+infixl 1 >>=--+ -- }}}  -- Some3 {{{@@ -117,6 +135,15 @@ onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g onSome3 f (Some3 a) = Some3 (f a) +msome3 :: Monad m => f a b c -> m (Some3 f)+msome3 = return . Some3++(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r+m >>=--- f = do+  s <- m+  s >>--- f+infixl 1 >>=---+ -- }}}  -- SomeC {{{@@ -131,6 +158,15 @@ (>>~) = someC infixl 1 >>~ +msomeC :: (Monad m, c a) => f a -> m (SomeC c f)+msomeC = return . SomeC++(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r+m >>=~ f = do+  s <- m+  s >>~ f+infixl 1 >>=~+ -- }}}  -- EveryN {{{@@ -143,6 +179,10 @@  data Every3 (f :: k -> l -> m -> *) :: * where   Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f++data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where+  EveryC :: { instEveryC :: forall a. c a => f a }+         -> EveryC c f  -- }}} 

@@ -29,6 +29,7 @@  module Data.Type.Sym where +import Data.Type.Boolean import Type.Class.Higher import Type.Class.Known import Type.Class.Witness@@ -53,6 +54,10 @@  instance TestEquality Sym where   testEquality Sym Sym = sameSymbol Proxy Proxy++instance BoolEquality Sym where+  type BoolEqC Sym a b = Known Boolean (a == b)+  Sym .== Sym = known  instance KnownSymbol x => Known Sym x where   type KnownC Sym x = KnownSymbol x

@@ -88,6 +88,9 @@   id              = Sub Wit   Sub bc . Sub ab = Sub $ bc \\ ab +transC :: (b :- c) -> (a :- b) -> a :- c+transC = (.)+ -- }}}  -- Witness {{{@@ -176,6 +179,9 @@  -- Initial/Terminal {{{ +toEquality :: (a ~ b) :- (c ~ d) -> a :~: b -> c :~: d+toEquality p = \Refl -> Refl \\ p+ commute :: (a ~ b) :- (b ~ a) commute = Sub Wit @@ -192,6 +198,8 @@ bottom :: Fail :- c bottom = falso ++ instance Witness ØC c (Wit c) where   r \\ Wit = r @@ -239,6 +247,14 @@  impossible :: a -> Void impossible = unsafeCoerce++exFalso :: Wit Fail -> a+exFalso p = castWith q ()+  where+  q :: () :~: a+  q = toEquality (contraC r) Refl+  r :: (b ~ b) :- Fail+  r = Sub p  (=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b) (=?=) = testEquality

@@ -27,29 +27,16 @@  module Type.Family.Bool   ( module Type.Family.Bool-  , type (==)+  , module Exports   ) where  import Type.Family.Constraint-import Type.Class.Witness (type (==))+import Type.Class.Witness as Exports (type (==))+import Data.Type.Bool as Exports (type Not, type (||), type (&&))  type family BoolC (b :: Bool) :: Constraint where   BoolC True  = ØC   BoolC False = Fail--type family (a :: Bool) || (b :: Bool) :: Bool where-  True  || b = True-  False || b = b-infixr 2 ||--type family (a :: Bool) && (b :: Bool) :: Bool where-  True  && b = b-  False && b = False-infixr 3 &&--type family Not (a :: Bool) :: Bool where-  Not True  = False-  Not False = True  type a ==> b = Not a || b infixr 1 ==>

@@ -30,6 +30,7 @@ module Type.Family.Nat where  import Data.Type.Equality+import Type.Family.Bool import Type.Family.Constraint import Type.Family.List import Type.Class.Witness@@ -112,6 +113,26 @@  ixCong :: (x ~ y,as ~ bs) :- (Ix x as ~ Ix y bs) ixCong = Sub Wit++type family (x :: N) < (y :: N) :: Bool where+  Z   < Z   = False+  Z   < S y = True+  S x < Z   = False+  S x < S y = x < y+infix 4 <++type x <= y = (x == y) || (x < y)+infix 4 <=++type family (x :: N) > (y :: N) :: Bool where+  Z   > Z   = False+  Z   > S y = False+  S x > Z   = True+  S x > S y = x > y+infix 4 >++type x >= y = (x == y) || (x > y)+infix 4 >=  -- | Convenient aliases for low-value Peano numbers. type N0  = Z

@@ -1,5 +1,5 @@ name: type-combinators-version: 0.2.1.0+version: 0.2.2.0 category: Data synopsis: A collection of data types for type-level programming cabal-version: >=1.10