type-combinators 0.1.2.1 → 0.2.0.0

raw patch · 30 files changed

+1794/−1010 lines, 30 filesdep −containersdep −mtldep −template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies removed: containers, mtl, template-haskell, transformers

API changes (from Hackage documentation)

Files

• src/Data/Type/Combinator.hs +154/−200
• src/Data/Type/Conjunction.hs +50/−25
• src/Data/Type/Disjunction.hs +130/−47
• src/Data/Type/Fin.hs +23/−23
• src/Data/Type/Index.hs +48/−2
• src/Data/Type/Index/Quote.hs +0/−62
• src/Data/Type/Length.hs +32/−8
• src/Data/Type/Nat.hs +26/−39
• src/Data/Type/Nat/Quote.hs +0/−89
• src/Data/Type/Option.hs +8/−8
• src/Data/Type/Product.hs +109/−21
• src/Data/Type/Product/Dual.hs +0/−184
• src/Data/Type/Product/Lifted.hs +178/−0
• src/Data/Type/Quantifier.hs +72/−16
• src/Data/Type/Sum.hs +73/−21
• src/Data/Type/Sum/Dual.hs +0/−125
• src/Data/Type/Sum/Lifted.hs +119/−0
• src/Data/Type/Sym.hs +66/−0
• src/Data/Type/Vector.hs +20/−11
• src/Type/Class/HFunctor.hs +0/−56
• src/Type/Class/Higher.hs +236/−0
• src/Type/Class/Known.hs +1/−2
• src/Type/Class/Witness.hs +131/−34
• src/Type/Family/Either.hs +105/−0
• src/Type/Family/List.hs +87/−7
• src/Type/Family/Maybe.hs +27/−6
• src/Type/Family/Nat.hs +47/−4
• src/Type/Family/Symbol.hs +7/−0
• src/Type/Family/Tuple.hs +36/−9
• type-combinators.cabal +9/−11

@@ -1,9 +1,14 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -24,14 +29,14 @@ -- -- A collection of simple type combinators, -- such as @Identity@ 'I', @Constant@ 'C', @Compose@ '(:.:)',--- left unnest 'LL', right unnest 'RR', the @S Combinator@ 'SS',--- etc.+-- Currying/Uncurrying, etc. -- -----------------------------------------------------------------------------  module Data.Type.Combinator where -import Type.Class.HFunctor+import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Tuple@@ -40,75 +45,43 @@  -- (:.:) {{{ -data ((f :: l -> *) :.: (g :: k -> l)) :: k -> * where-  Comp :: { getComp :: f (g a) } -> (f :.: g) a-infixr 6 :.:+newtype ((f :: l -> *) :.: (g :: k -> l)) (a :: k) = Comp+  { getComp :: f (g a)+  } deriving+  ( Eq , Ord , Show , Read+  ) -deriving instance Eq   (f (g a)) => Eq   ((f :.: g) a)-deriving instance Ord  (f (g a)) => Ord  ((f :.: g) a)-deriving instance Show (f (g a)) => Show ((f :.: g) a)+instance Eq1 f => Eq1 (f :.: g) where+  Comp a `eq1` Comp b = a `eq1` b +instance Ord1 f => Ord1 (f :.: g) where+  Comp a `compare1` Comp b = a `compare1` b++instance Show1 f => Show1 (f :.: g) where+  showsPrec1 d (Comp a) = showParen (d > 10)+    $ showString "Comp "+    . showsPrec1 11 a+ instance Witness p q (f (g a)) => Witness p q ((f :.: g) a) where   type WitnessC p q ((f :.: g) a) = Witness p q (f (g a))   r \\ Comp a = r \\ a -data ((f :: m -> *) :..: (g :: k -> l -> m)) :: k -> l -> * where-  Comp2 :: f (g a b) -> (f :..: g) a b-infixr 6 :..:--deriving instance Eq   (f (g a b)) => Eq   ((f :..: g) a b)-deriving instance Ord  (f (g a b)) => Ord  ((f :..: g) a b)-deriving instance Show (f (g a b)) => Show ((f :..: g) a b)--instance Witness p q (f (g a b)) => Witness p q ((f :..: g) a b) where-  type WitnessC p q ((f :..: g) a b) = Witness p q (f (g a b))-  r \\ Comp2 a = r \\ a---- }}}---- IT {{{--data IT :: (k -> *) -> k -> * where-  IT :: { getIT :: f a } -> IT f a--deriving instance Eq   (f a) => Eq   (IT f a)-deriving instance Ord  (f a) => Ord  (IT f a)-deriving instance Show (f a) => Show (IT f a)--instance HFunctor IT where-  map' f = IT . f . getIT--instance HFoldable IT where-  foldMap' f = f . getIT--instance HTraversable IT where-  traverse' f = fmap IT . f . getIT--instance Witness p q (f a) => Witness p q (IT f a) where-  type WitnessC p q (IT f a) = Witness p q (f a)-  r \\ IT a = r \\ a+instance TestEquality f => TestEquality (f :.: g) where+  testEquality (Comp a) (Comp b) = a =?= b //? qed -instance Num (f a) => Num (IT f a) where-  IT a * IT b   = IT $ a * b-  IT a + IT b   = IT $ a + b-  IT a - IT b   = IT $ a - b-  abs    (IT a) = IT $ abs a-  signum (IT a) = IT $ signum a-  fromInteger   = IT . fromInteger+instance TestEquality f => TestEquality1 ((:.:) f) where+  testEquality1 (Comp a) (Comp b) = a =?= b //? qed  -- }}}  -- I {{{ -data I :: * -> * where-  I :: { getI :: a } -> I a--deriving instance Eq   a => Eq   (I a)-deriving instance Ord  a => Ord  (I a)-deriving instance Show a => Show (I a)--instance Functor I where-  fmap f (I a) = I $ f a+newtype I a = I+  { getI :: a+  } deriving+  ( Eq , Ord , Show+  , Functor , Foldable , Traversable+  )  instance Applicative I where   pure = I@@ -117,12 +90,6 @@ instance Monad I where   I a >>= f = f a -instance Foldable I where-  foldMap f (I a) = f a--instance Traversable I where-  traverse f (I a) = I <$> f a- instance Witness p q a => Witness p q (I a) where   type WitnessC p q (I a) = Witness p q a   r \\ I a = r \\ a@@ -137,112 +104,26 @@  -- }}} --- LL {{{--newtype LL (a :: k) (f :: l -> *) (g :: k -> l) = LL-  { getLL :: f (g a)-  }--deriving instance Eq   (f (g a)) => Eq   (LL a f g)-deriving instance Ord  (f (g a)) => Ord  (LL a f g)-deriving instance Show (f (g a)) => Show (LL a f g)--instance HFunctor (LL a) where-  map' f = LL . f . getLL--instance HFoldable (LL a) where-  foldMap' f = f . getLL--instance HTraversable (LL a) where-  traverse' f = fmap LL . f . getLL--instance Witness p q (f (g a)) => Witness p q (LL a f g) where-  type WitnessC p q (LL a f g) = Witness p q (f (g a))-  r \\ LL a = r \\ a---- }}}---- RR {{{--newtype RR (g :: k -> l) (f :: l -> *) (a :: k) = RR-  { getRR :: f (g a)-  }--deriving instance Eq   (f (g a)) => Eq   (RR g f a)-deriving instance Ord  (f (g a)) => Ord  (RR g f a)-deriving instance Show (f (g a)) => Show (RR g f a)--instance HFunctor (RR g) where-  map' f = RR . f . getRR--instance HFoldable (RR g) where-  foldMap' f = f . getRR--instance HTraversable (RR g) where-  traverse' f = fmap RR . f . getRR--instance Witness p q (f (g a)) => Witness p q (RR g f a) where-  type WitnessC p q (RR g f a) = Witness p q (f (g a))-  r \\ RR a = r \\ a---- }}}---- SS {{{--newtype SS (f :: k -> l -> *) (g :: k -> l) :: k -> * where-  SS :: { getSS :: f a (g a) } -> SS f g a--deriving instance Eq   (f a (g a)) => Eq   (SS f g a)-deriving instance Ord  (f a (g a)) => Ord  (SS f g a)-deriving instance Show (f a (g a)) => Show (SS f g a)--instance Witness p q (f a (g a)) => Witness p q (SS f g a) where-  type WitnessC p q (SS f g a) = Witness p q (f a (g a))-  r \\ SS a = r \\ a---- }}}---- CT {{{--data CT :: * -> (k -> *) -> l -> * where-  CT :: { getCT :: r } -> CT r f a--deriving instance Eq   r => Eq   (CT r f a)-deriving instance Ord  r => Ord  (CT r f a)-deriving instance Show r => Show (CT r f a)--instance HFunctor (CT r) where-  map' _ (CT r) = CT r--instance HFoldable (CT r) where-  foldMap' _ _ = mempty--instance HTraversable (CT r) where-  traverse' _ (CT r) = pure $ CT r--instance Witness p q r => Witness p q (CT r f a) where-  type WitnessC p q (CT r f a) = Witness p q r-  r \\ CT a = r \\ a--instance Num r => Num (CT r f a) where-  CT a * CT b   = CT $ a * b-  CT a + CT b   = CT $ a + b-  CT a - CT b   = CT $ a - b-  abs    (CT a) = CT $ abs a-  signum (CT a) = CT $ signum a-  fromInteger   = CT . fromInteger---- }}}- -- C {{{ -data C :: * -> k -> * where-  C :: { getC :: r } -> C r a+newtype C r a = C+  { getC :: r+  } deriving+  ( Eq , Ord , Show , Read+  , Functor , Foldable , Traversable+  ) -deriving instance Eq   r => Eq   (C r a)-deriving instance Ord  r => Ord  (C r a)-deriving instance Show r => Show (C r a)+instance Eq   r => Eq1   (C r)+instance Ord  r => Ord1  (C r)+instance Show r => Show1 (C r) +instance Read r => Read1 (C r) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (Some $ C r,s2)+    | ("C",s1) <- lex s0+    , (r,s2)   <- readsPrec 11 s1+    ]+ instance Witness p q r => Witness p q (C r a) where   type WitnessC p q (C r a) = Witness p q r   r \\ C a = r \\ a@@ -255,26 +136,8 @@   signum (C a) = C $ signum a   fromInteger  = C . fromInteger --- }}}---- Join {{{--newtype Join f a = Join-  { getJoin :: f a a-  }--deriving instance Eq   (f a a) => Eq   (Join f a)-deriving instance Ord  (f a a) => Ord  (Join f a)-deriving instance Show (f a a) => Show (Join f a)--instance Known (f a) a => Known (Join f) a where-  type KnownC (Join f) a = Known (f a) a-  known = Join known--instance Witness p q (f a a) => Witness p q (Join f a) where-  type WitnessC p q (Join f a) = Witness p q (f a a)-  r \\ Join a = r \\ a-  +mapC :: (r -> s) -> C r a -> C s b+mapC f = C . f . getC  -- }}} @@ -282,26 +145,40 @@  newtype Flip p b a = Flip   { getFlip :: p a b-  } deriving (Eq,Ord,Show)+  } deriving+  ( Eq , Ord , Show , Read+  ) -instance Known (p a) b => Known (Flip p b) a where-  type KnownC (Flip p b) a = Known (p a) b-  known = Flip known+flipTestEquality1 :: TestEquality (p c) => Flip p a c -> Flip p b c -> Maybe (a :~: b)+flipTestEquality1 (Flip a) (Flip b) = a =?= b +instance TestEquality1 p => TestEquality (Flip p b) where+  testEquality (Flip a) (Flip b) = a =??= b+ instance Witness p q (f a b) => Witness p q (Flip f b a) where   type WitnessC p q (Flip f b a) = Witness p q (f a b)   r \\ Flip a = r \\ a -flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c-flipped f = Flip . f . getFlip+instance Known (p a) b => Known (Flip p b) a where+  type KnownC (Flip p b) a = Known (p a) b+  known = Flip known +mapFlip :: (f a b -> g c d) -> Flip f b a -> Flip g d c+mapFlip f = Flip . f . getFlip+ -- }}}  -- Cur {{{ -newtype Cur (p :: (k,l) -> *) :: k -> l -> * where-  Cur :: { getCur :: p (a#b) } -> Cur p a b+newtype Cur (p :: (k,l) -> *) (a :: k) (b :: l) = Cur+  { getCur :: p (a#b)+  } +deriving instance Eq   (p (a#b)) => Eq   (Cur p a b)+deriving instance Ord  (p (a#b)) => Ord  (Cur p a b)+deriving instance Show (p (a#b)) => Show (Cur p a b)+deriving instance Read (p (a#b)) => Read (Cur p a b)+ instance Known p (a#b) => Known (Cur p a) b where   type KnownC (Cur p a) b = Known p (a#b)   known = Cur known@@ -310,6 +187,9 @@   type WitnessC q r (Cur p a b) = Witness q r (p (a#b))   r \\ Cur p = r \\ p +mapCur :: (p '(a,b) -> q '(c,d)) -> Cur p a b -> Cur q c d+mapCur f = Cur . f . getCur+ -- }}}  -- Uncur {{{@@ -317,6 +197,18 @@ data Uncur (p :: k -> l -> *) :: (k,l) -> * where   Uncur :: { getUncur :: p a b } -> Uncur p (a#b) +deriving instance Eq   (p (Fst x) (Snd x)) => Eq   (Uncur p x)+deriving instance Ord  (p (Fst x) (Snd x)) => Ord  (Uncur p x)+deriving instance Show (p (Fst x) (Snd x)) => Show (Uncur p x)+deriving instance (x ~ (a#b), Read (p a b)) => Read (Uncur p x)++instance Read2 p => Read1 (Uncur p) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (p >>-- Some . Uncur,s2)+    | ("Uncur",s1) <- lex s0+    , (p,s2)       <- readsPrec2 11 s1+    ]+ instance (Known (p a) b,q ~ (a#b)) => Known (Uncur p) q where   type KnownC (Uncur p) q = Known (p (Fst q)) (Snd q)   known = Uncur known@@ -325,13 +217,22 @@   type WitnessC r s (Uncur p q) = Witness r s (p (Fst q) (Snd q))   r \\ Uncur p = r \\ p +mapUncur :: (p (Fst a) (Snd a) -> q b c) -> Uncur p a -> Uncur q '(b,c)+mapUncur f (Uncur a) = Uncur $ f a+ -- }}} --- Cur {{{+-- Cur3 {{{ -newtype Cur3 (p :: (k,l,m) -> *) :: k -> l -> m -> * where-  Cur3 :: { getCur3 :: p '(a,b,c) } -> Cur3 p a b c+newtype Cur3 (p :: (k,l,m) -> *) (a :: k) (b :: l) (c :: m) = Cur3+  { getCur3 :: p '(a,b,c)+  } +deriving instance Eq   (p '(a,b,c)) => Eq   (Cur3 p a b c)+deriving instance Ord  (p '(a,b,c)) => Ord  (Cur3 p a b c)+deriving instance Show (p '(a,b,c)) => Show (Cur3 p a b c)+deriving instance Read (p '(a,b,c)) => Read (Cur3 p a b c)+ instance Known p '(a,b,c) => Known (Cur3 p a b) c where   type KnownC (Cur3 p a b) c = Known p '(a,b,c)   known = Cur3 known@@ -340,6 +241,9 @@   type WitnessC q r (Cur3 p a b c) = Witness q r (p '(a,b,c))   r \\ Cur3 p = r \\ p +mapCur3 :: (p '(a,b,c) -> q '(d,e,f)) -> Cur3 p a b c -> Cur3 q d e f+mapCur3 f = Cur3 . f . getCur3+ -- }}}  -- Uncur3 {{{@@ -347,6 +251,18 @@ data Uncur3 (p :: k -> l -> m -> *) :: (k,l,m) -> * where   Uncur3 :: { getUncur3 :: p a b c } -> Uncur3 p '(a,b,c) +deriving instance Eq   (p (Fst3 x) (Snd3 x) (Thd3 x)) => Eq   (Uncur3 p x)+deriving instance Ord  (p (Fst3 x) (Snd3 x) (Thd3 x)) => Ord  (Uncur3 p x)+deriving instance Show (p (Fst3 x) (Snd3 x) (Thd3 x)) => Show (Uncur3 p x)+deriving instance (x ~ '(a,b,c), Read (p a b c)) => Read (Uncur3 p x)++instance Read3 p => Read1 (Uncur3 p) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (p >>--- Some . Uncur3,s2)+    | ("Uncur",s1) <- lex s0+    , (p,s2)       <- readsPrec3 11 s1+    ]+ instance (Known (p a b) c,q ~ '(a,b,c)) => Known (Uncur3 p) q where   type KnownC (Uncur3 p) q = Known (p (Fst3 q) (Snd3 q)) (Thd3 q)   known = Uncur3 known@@ -354,6 +270,44 @@ instance (Witness r s (p a b c),q ~ '(a,b,c)) => Witness r s (Uncur3 p q) where   type WitnessC r s (Uncur3 p q) = Witness r s (p (Fst3 q) (Snd3 q) (Thd3 q))   r \\ Uncur3 p = r \\ p++mapUncur3 :: (p (Fst3 x) (Snd3 x) (Thd3 x) -> q d e f) -> Uncur3 p x -> Uncur3 q '(d,e,f)+mapUncur3 f (Uncur3 a) = Uncur3 $ f a++-- }}}++-- Join {{{++newtype Join f a = Join+  { getJoin :: f a a+  }++deriving instance Eq   (f a a) => Eq   (Join f a)+deriving instance Ord  (f a a) => Ord  (Join f a)+deriving instance Show (f a a) => Show (Join f a)+deriving instance Read (f a a) => Read (Join f a)++instance Eq2 f => Eq1 (Join f) where+  Join a `eq1` Join b = a `eq2` b++instance Ord2 f => Ord1 (Join f) where+  Join a `compare1` Join b = a `compare2` b++instance Show2 f => Show1 (Join f) where+  showsPrec1 d (Join a) = showParen (d > 10)+    $ showString "Join "+    . showsPrec2 11 a++instance Known (f a) a => Known (Join f) a where+  type KnownC (Join f) a = Known (f a) a+  known = Join known++instance Witness p q (f a a) => Witness p q (Join f a) where+  type WitnessC p q (Join f a) = Witness p q (f a a)+  r \\ Join a = r \\ a++mapJoin :: (f a a -> g b b) -> Join f a -> Join g b+mapJoin f = Join . f . getJoin  -- }}} 

@@ -32,7 +32,7 @@  module Data.Type.Conjunction where -import Type.Class.HFunctor+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Tuple@@ -46,13 +46,33 @@ deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :&: g) a) deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :&: g) a) deriving instance (Show (f a), Show (g a)) => Show ((f :&: g) a)+deriving instance (Read (f a), Read (g a)) => Read ((f :&: g) a) +instance (Eq1 f, Eq1 g) => Eq1 (f :&: g) where+  eq1 (a :&: b) (c :&: d) = a =#= c && b =#= d++instance (Ord1 f, Ord1 g) => Ord1 (f :&: g) where+  compare1 (a :&: b) (c :&: d) = compare1 a c `mappend` compare1 b d++instance (Show1 f, Show1 g) => Show1 (f :&: g) where+  showsPrec1 d (a :&: b) = showParen (d > 5)+    $ showsPrec1 11 a+    . showString " :&: "+    . showsPrec1 11 b+ fanFst :: (f :&: g) a -> f a fanFst (a :&: _) = a  fanSnd :: (f :&: g) a -> g a fanSnd (_ :&: b) = b +(.&.) :: (f a -> h b) -> (g a -> i b) -> (f :&: g) a -> (h :&: i) b+(f .&. g) (a :&: b) = f a :&: g b+infixr 3 .&.++fanFirst :: (f a -> g a) -> (f :&: h) a -> (g :&: h) a+fanFirst f (a :&: b) = f a :&: b+ uncurryFan :: (f a -> g a -> r) -> (f :&: g) a -> r uncurryFan f (a :&: b) = f a b @@ -65,30 +85,22 @@ instance (Known f a, Known g a) => Known (f :&: g) a where   known = known :&: known -instance HFunctor ((:&:) f) where-  map' f (a :&: b) = a :&: f b+instance Functor1 ((:&:) f) where+  map1 f (a :&: b) = a :&: f b -instance HFoldable ((:&:) f) where-  foldMap' f (_ :&: b) = f b+instance Foldable1 ((:&:) f) where+  foldMap1 f (_ :&: b) = f b -instance HTraversable ((:&:) f) where-  traverse' f (a :&: b) = (:&:) a <$> f b+instance Traversable1 ((:&:) f) where+  traverse1 f (a :&: b) = (:&:) a <$> f b -instance HBifunctor (:&:) where-  bimap' f g (a :&: b) = f a :&: g b+instance Bifunctor1 (:&:) where+  bimap1 f g (a :&: b) = f a :&: g b  instance (Witness p q (f a), Witness s t (g a)) => Witness (p,s) (q,t) ((f :&: g) a) where   type WitnessC (p,s) (q,t) ((f :&: g) a) = (Witness p q (f a), Witness s t (g a))   r \\ a :&: b = r \\ a \\ b -{--instance Witness p q (f a) => Witness p q (WitFst (:&:) f g a) where-  r \\ WitFst (a :&: _) = r \\ a--instance Witness p q (g a) => Witness p q (WitSnd (:&:) f g a) where-  r \\ WitSnd (_ :&: b) = r \\ b--}- -- }}}  -- (:*:) {{{@@ -100,7 +112,20 @@ deriving instance (Eq   (f (Fst p)), Eq   (g (Snd p))) => Eq   ((f :*: g) p) deriving instance (Ord  (f (Fst p)), Ord  (g (Snd p))) => Ord  ((f :*: g) p) deriving instance (Show (f (Fst p)), Show (g (Snd p))) => Show ((f :*: g) p)+deriving instance (p ~ (a#b), Read (f a), Read (g b)) => Read ((f :*: g) p) +instance (Eq1 f, Eq1 g) => Eq1 (f :*: g) where+  eq1 (a :*: b) (c :*: d) = a =#= c && b =#= d++instance (Ord1 f, Ord1 g) => Ord1 (f :*: g) where+  compare1 (a :*: b) (c :*: d) = compare1 a c `mappend` compare1 b d++instance (Show1 f, Show1 g) => Show1 (f :*: g) where+  showsPrec1 d (a :*: b) = showParen (d > 5)+    $ showsPrec1 11 a+    . showString " :*: "+    . showsPrec1 11 b+ parFst :: (f :*: g) p -> f (Fst p) parFst (a :*: _) = a @@ -116,17 +141,17 @@ instance (p ~ (a#b), Known f a, Known g b) => Known (f :*: g) p where   known = known :*: known -instance HFunctor ((:*:) f) where-  map' f (a :*: b) = a :*: f b+instance Functor1 ((:*:) f) where+  map1 f (a :*: b) = a :*: f b -instance HFoldable ((:*:) f) where-  foldMap' f (_ :*: b) = f b+instance Foldable1 ((:*:) f) where+  foldMap1 f (_ :*: b) = f b -instance HTraversable ((:*:) f) where-  traverse' f (a :*: b) = (:*:) a <$> f b+instance Traversable1 ((:*:) f) where+  traverse1 f (a :*: b) = (:*:) a <$> f b -instance HBifunctor (:*:) where-  bimap' f g (a :*: b) = f a :*: g b+instance Bifunctor1 (:*:) where+  bimap1 f g (a :*: b) = f a :*: g b  _fst :: (a#b) :~: (c#d) -> a :~: c _fst Refl = Refl

@@ -1,9 +1,9 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -23,107 +23,190 @@ -- Portability :  RankNTypes -- -- Two type combinators for working with disjunctions:--- A /branch/ combinator '(:+:)', and a /choice/ combinator '(:|:)'.+-- A /branch/ combinator '(:|:)', and a /choice/ combinator '(:+:)'. ----- These are analogous to '(+++)' and '(|||)' from 'Control.Arrow',+-- These are analogous to '(|||)' and '(+++)' from 'Control.Arrow', -- respectively. -- -----------------------------------------------------------------------------  module Data.Type.Disjunction where -import Type.Class.HFunctor+import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness+import Type.Family.Either --- (:+:) {{{+-- (:|:) {{{ -data ((f :: k -> *) :+: (g :: k -> *)) :: k -> * where-  L :: !(f a) -> (f :+: g) a-  R :: !(g a) -> (f :+: g) a-infixr 4 :+:+data ((f :: k -> *) :|: (g :: k -> *)) :: k -> * where+  L :: !(f a) -> (f :|: g) a+  R :: !(g a) -> (f :|: g) a+infixr 4 :|: -(>+<) :: (f a -> r) -> (g a -> r) -> (f :+: g) a -> r-f >+< g = \case+deriving instance (Eq   (f a), Eq   (g a)) => Eq   ((f :|: g) a)+deriving instance (Ord  (f a), Ord  (g a)) => Ord  ((f :|: g) a)+deriving instance (Show (f a), Show (g a)) => Show ((f :|: g) a)+deriving instance (Read (f a), Read (g a)) => Read ((f :|: g) a)++instance (Eq1 f, Eq1 g) => Eq1 (f :|: g) where+  eq1 = \case+    L a -> \case+      L b -> a =#= b+      _   -> False+    R a -> \case+      R b -> a =#= b+      _   -> False++instance (Ord1 f, Ord1 g) => Ord1 (f :|: g) where+  compare1 = \case+    L a -> \case+      L b -> compare1 a b+      R _ -> LT+    R a -> \case+      L _ -> GT+      R b -> compare1 a b++instance (Show1 f, Show1 g) => Show1 (f :|: g) where+  showsPrec1 d = showParen (d > 10) . \case+    L a -> showString "L "+         . showsPrec1 11 a+    R b -> showString "R "+         . showsPrec1 11 b++instance (Read1 f, Read1 g) => Read1 (f :|: g) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (a >>- Some . L,s2)+    | ("L",s1) <- lex s0+    , (a,s2)   <- readsPrec1 11 s1+    ] +++    [ (a >>- Some . R,s2)+    | ("R",s1) <- lex s0+    , (a,s2)   <- readsPrec1 11 s1+    ]++(>|<) :: (f a -> r) -> (g a -> r) -> (f :|: g) a -> r+f >|< g = \case   L a -> f a   R b -> g b-infixr 2 >+<+infixr 2 >|< -instance HFunctor ((:+:) f) where-  map' f = \case+instance Functor1 ((:|:) f) where+  map1 f = \case     L a -> L a     R b -> R $ f b -instance HFoldable ((:+:) f) where-  foldMap' f = \case+instance Foldable1 ((:|:) f) where+  foldMap1 f = \case     L _ -> mempty     R b -> f b -instance HTraversable ((:+:) f) where-  traverse' f = \case+instance Traversable1 ((:|:) f) where+  traverse1 f = \case     L a -> pure $ L a     R b -> R <$> f b -instance HBifunctor (:+:) where-  bimap' f g = \case+instance Bifunctor1 (:|:) where+  bimap1 f g = \case     L a -> L $ f a     R b -> R $ g b -instance (Witness p q (f a), Witness p q (g a)) => Witness p q ((f :+: g) a) where-  type WitnessC p q ((f :+: g) a) = (Witness p q (f a), Witness p q (g a))+instance (Witness p q (f a), Witness p q (g a)) => Witness p q ((f :|: g) a) where+  type WitnessC p q ((f :|: g) a) = (Witness p q (f a), Witness p q (g a))   (\\) r = \case     L a -> r \\ a     R b -> r \\ b  -- }}} --- (:|:) {{{+-- (:+:) {{{ -data ((f :: k -> *) :|: (g :: l -> *)) :: Either k l -> * where-  L' :: !(f a) -> (f :|: g) (Left  a)-  R' :: !(g b) -> (f :|: g) (Right b)-infixr 4 :|:+data ((f :: k -> *) :+: (g :: l -> *)) :: Either k l -> * where+  L' :: !(f a) -> (f :+: g) (Left  a)+  R' :: !(g b) -> (f :+: g) (Right b)+infixr 4 :+: -(>|<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :|: g) e -> r-f >|< g = \case+deriving instance (Eq   (f (FromLeft e)), Eq   (g (FromRight e))) => Eq   ((f :+: g) e)+deriving instance (Ord  (f (FromLeft e)), Ord  (g (FromRight e))) => Ord  ((f :+: g) e)+deriving instance (Show (f (FromLeft e)), Show (g (FromRight e))) => Show ((f :+: g) e)++instance (Eq1 f, Eq1 g) => Eq1 (f :+: g) where+  eq1 = \case+    L' a -> \case+      L' b -> a =#= b+      _    -> False+    R' a -> \case+      R' b -> a =#= b+      _    -> False++instance (Ord1 f, Ord1 g) => Ord1 (f :+: g) where+  compare1 = \case+    L' a -> \case+      L' b -> compare1 a b+      _    -> LT+    R' a -> \case+      R' b -> compare1 a b+      _    -> GT++instance (Show1 f, Show1 g) => Show1 (f :+: g) where+  showsPrec1 d = showParen (d > 10) . \case+    L' a -> showString "L' "+          . showsPrec1 11 a+    R' b -> showString "R' "+          . showsPrec1 11 b++instance (Read1 f, Read1 g) => Read1 (f :+: g) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (a >>- Some . L',s2)+    | ("L'",s1) <- lex s0+    , (a,s2)    <- readsPrec1 11 s1+    ] +++    [ (a >>- Some . R',s2)+    | ("R'",s1) <- lex s0+    , (a,s2)    <- readsPrec1 11 s1+    ]++(>+<) :: (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   R' b -> g b-infixr 2 >|<+infixr 2 >+< -instance Known f a => Known (f :|: g) (Left a) where-  type KnownC (f :|: g) (Left a) = Known f a+instance Known f a => Known (f :+: g) (Left a) where+  type KnownC (f :+: g) (Left a) = Known f a   known = L' known -instance Known g b => Known (f :|: g) (Right b) where-  type KnownC (f :|: g) (Right b) = Known g b+instance Known g b => Known (f :+: g) (Right b) where+  type KnownC (f :+: g) (Right b) = Known g b   known = R' known -instance HFunctor ((:|:) f) where-  map' f = \case+instance Functor1 ((:+:) f) where+  map1 f = \case     L' a -> L' a     R' b -> R' $ f b -instance HFoldable ((:|:) f) where-  foldMap' f = \case+instance Foldable1 ((:+:) f) where+  foldMap1 f = \case     L' _ -> mempty     R' b -> f b -instance HTraversable ((:|:) f) where-  traverse' f = \case+instance Traversable1 ((:+:) f) where+  traverse1 f = \case     L' a -> pure $ L' a     R' b -> R' <$> f b -instance HBifunctor (:|:) where-  bimap' f g = \case+instance Bifunctor1 (:+:) where+  bimap1 f g = \case     L' a -> L' $ f a     R' b -> R' $ g b -instance Witness p q (f a) => Witness p q ((f :|: g) (Left a)) where-  type WitnessC p q ((f :|: g) (Left a)) = Witness p q (f a)+instance Witness p q (f a) => Witness p q ((f :+: g) (Left a)) where+  type WitnessC p q ((f :+: g) (Left a)) = Witness p q (f a)   r \\ L' a = r \\ a -instance Witness p q (g b) => Witness p q ((f :|: g) (Right b)) where-  type WitnessC p q ((f :|: g) (Right b)) = Witness p q (g b)+instance Witness p q (g b) => Witness p q ((f :+: g) (Right b)) where+  type WitnessC p q ((f :+: g) (Right b)) = Witness p q (g b)   r \\ R' b = r \\ b  -- }}}

@@ -1,3 +1,4 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternSynonyms #-}@@ -5,7 +6,6 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -30,9 +30,8 @@  module Data.Type.Fin where -import Data.Type.Combinator import Data.Type.Nat-import Type.Class.Known+import Type.Class.Higher import Type.Class.Witness import Type.Family.Constraint import Type.Family.Nat@@ -46,6 +45,27 @@ deriving instance Ord  (Fin n) deriving instance Show (Fin n) +instance Eq1   Fin+instance Ord1  Fin+instance Show1 Fin++instance Read1 Fin where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (Some FZ,s1)+    | ("FZ",s1) <- lex s0+    ] ++ +    [ (n >>- Some . FS,s2)+    | ("FS",s1) <- lex s0+    , (n,s2)    <- readsPrec1 11 s1+    ]++elimFin :: (forall x. p (S x))+        -> (forall x. Fin x -> p x -> p (S x))+        -> Fin n -> p n+elimFin z s = \case+  FZ   -> z+  FS n -> s n $ elimFin z s n+ -- | Gives the list of all members of the finite set of size @n@. fins :: Nat n -> [Fin n] fins = \case@@ -76,26 +96,6 @@   FS x -> \case     FZ   -> Just FZ \\ x     FS y -> FS <$> without x y \\ x--class (x :: N) <= (y :: N) where-  weakenN :: Fin x -> Fin y--instance {-# OVERLAPPING #-} x <= x where-  weakenN = id--instance {-# OVERLAPPABLE #-} (x <= y) => x <= S y where-  weakenN = weaken . weakenN--{--instance Known Nat n => Known ([] :.: Fin) n where-  type KnownC ([] :.: Fin) n = Known Nat n-  known = Comp $ go (known :: Nat n)-    where-    go :: Nat x -> [Fin x]-    go = \case-      Z_   -> []-      S_ x -> FZ : map FS (go x)--}  -- | Take a 'Fin' to an existentially quantified 'Nat'. finNat :: Fin x -> Some Nat

@@ -1,3 +1,4 @@+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}@@ -28,10 +29,11 @@  module Data.Type.Index where -import Type.Class.HFunctor+import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known+import Type.Class.Witness import Type.Family.List-import Type.Family.Nat  data Index :: [k] -> k -> * where   IZ :: Index (a :< as) a@@ -41,6 +43,47 @@ deriving instance Ord  (Index as a) deriving instance Show (Index as a) +instance Eq1   (Index as)+instance Ord1  (Index as)+instance Show1 (Index as)++instance Read2 Index where+  readsPrec2 d = readParen (d > 10) $ \s0 ->+    [ (Some2 IZ,s1)+    | ("IZ",s1) <- lex s0+    ] +++    [ (i >>-- Some2 . IS,s2)+    | ("IS",s1) <- lex s0+    , (i,s2)    <- readsPrec2 11 s1+    ]++instance TestEquality (Index as) where+  testEquality = \case+    IZ -> \case+      IZ -> qed+      _  -> Nothing+    IS x -> \case+      IS y -> x =?= y //? qed+      _    -> Nothing++elimIndex :: (forall   xs. p (a :< xs) a)+          -> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a)+          -> Index as a+          -> p as a+elimIndex z s = \case+  IZ   -> z+  IS x -> s x $ elimIndex z s x++ixNil :: Index Ø a -> Void+ixNil = impossible++onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a+onIxPred f = \case+  IZ   -> IZ+  IS x -> IS $ f x++-- Elem {{{+ type a ∈ as = Elem as a infix 6 ∈ @@ -53,9 +96,12 @@ instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where   elemIndex = IS elemIndex + instance {-# OVERLAPPING #-} Known (Index (a :< as)) a where   known = IZ  instance {-# OVERLAPPABLE #-} Known (Index as) a => Known (Index (b :< as)) a where   known = IS known++-- }}} 

@@ -1,62 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE LambdaCase #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Type.Index.Quote--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ A 'QuasiQuoter' for the 'Index' type.-----------------------------------------------------------------------------------module Data.Type.Index.Quote where--import Data.Type.Index-import Language.Haskell.TH-import Language.Haskell.TH.Lib-import Language.Haskell.TH.Quote-import Text.Read (readMaybe)-import Control.Monad--ix :: QuasiQuoter-ix = QuasiQuoter-  { quoteExp  = parseIxExp-  , quotePat  = parseIxPat-  , quoteType = error "ix: quoteType not defined"-  , quoteDec  = error "ix: quoteDec not defined"-  }--parseIxExp :: String -> Q Exp-parseIxExp s = maybe (fail $ "ix: couldn't parse Int: " ++ show s)-  (notNeg >=> go)-  $ readMaybe s-  where-  notNeg :: Int -> Q Int-  notNeg n-    | n < 0 = fail $ "ix: negative index: " ++ show n-    | True  = return n-  go :: Int -> Q Exp-  go = \case-    0 -> [| IZ |]-    n -> [| IS $(go $ n-1) |]--parseIxPat :: String -> Q Pat-parseIxPat s = maybe (fail $ "ix: couldn't parse Int: " ++ show s)-  (notNeg >=> go)-  $ readMaybe s-  where-  notNeg :: Int -> Q Int-  notNeg n-    | n < 0 = fail $ "ix: negative index: " ++ show n-    | True  = return n-  go :: Int -> Q Pat-  go = \case-    0 -> [p| IZ |]-    n -> [p| IS $(go $ n-1) |]-

@@ -29,6 +29,8 @@  module Data.Type.Length where +import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known import Type.Family.List @@ -36,22 +38,44 @@   LZ :: Length Ø   LS :: !(Length as) -> Length (a :< as) -lOdd, lEven :: Length as -> Bool-lOdd = \case-  LZ   -> False-  LS l -> lEven l-lEven = \case-  LZ   -> True-  LS l -> lOdd l- deriving instance Eq   (Length as) deriving instance Ord  (Length as) deriving instance Show (Length as) +instance Eq1   Length+instance Ord1  Length+instance Show1 Length++instance Read1 Length where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (Some LZ,s1)+    | ("LZ",s1) <- lex s0+    ] +++    [ (l >>- Some . LS,s2)+    | ("LS",s1) <- lex s0+    , (l,s2) <- readsPrec1 11 s1+    ]+ instance Known Length Ø where   known = LZ  instance Known Length as => Known Length (a :< as) where   type KnownC Length (a :< as) = Known Length as   known = LS known++elimLength :: p Ø+           -> (forall x xs. Length xs -> p xs -> p (x :< xs))+           -> Length as+           -> p as+elimLength z s = \case+  LZ   -> z+  LS l -> s l $ elimLength z s l++lOdd, lEven :: Length as -> Bool+lOdd = \case+  LZ   -> False+  LS l -> lEven l+lEven = \case+  LZ   -> True+  LS l -> lOdd l 

@@ -29,12 +29,13 @@ module Data.Type.Nat where  import Data.Type.Equality-import Data.Type.Product+import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Constraint-import Type.Family.List import Type.Family.Nat+-- import Type.Class.Categories  data Nat :: N -> * where   Z_ :: Nat Z@@ -44,6 +45,20 @@ deriving instance Ord  (Nat n) deriving instance Show (Nat n) +instance Eq1   Nat+instance Ord1  Nat+instance Show1 Nat++instance Read1 Nat where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (Some Z_,s1)+    | ("Z_",s1) <- lex s0+    ] +++    [ (n >>- Some . S_,s2)+    | ("S_",s1) <- lex s0+    , (n,s2) <- readsPrec1 11 s1+    ]+ -- | @'Z_'@ is the canonical construction of a @'Nat' Z@. instance Known Nat Z where   known = Z_@@ -68,16 +83,7 @@       S_ _ -> Nothing     S_ x -> \case       Z_   -> Nothing-      S_ y -> testEquality x y /? qed--instance DecEquality Nat where-  decideEquality = \case-    Z_ -> \case-      Z_   -> Proven  _Z-      S_ _ -> Refuted _ZneS-    S_ x -> \case-      Z_   -> Refuted $ _ZneS . sym-      S_ y -> (_S <-> _s) <?> decideEquality x y+      S_ y -> testEquality x y //? qed  _Z :: Z :~: Z _Z = Refl@@ -123,32 +129,13 @@   S_ y -> (x .^ y) .* x infixl 8 .^ -nat :: Nat n -> Int-nat = \case-  Z_   -> 0-  S_ x -> succ $ nat x--n0  :: Nat N0-n1  :: Nat N1-n2  :: Nat N2-n3  :: Nat N3-n4  :: Nat N4-n5  :: Nat N5-n6  :: Nat N6-n7  :: Nat N7-n8  :: Nat N8-n9  :: Nat N9-n10 :: Nat N10+elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n+elimNat z s = \case+  Z_   -> z+  S_ x -> s x $ elimNat z s x -n0  = Z_-n1  = S_ n0-n2  = S_ n1-n3  = S_ n2-n4  = S_ n3-n5  = S_ n4-n6  = S_ n5-n7  = S_ n6-n8  = S_ n7-n9  = S_ n8-n10 = S_ n9+natVal :: Nat n -> Int+natVal = \case+  Z_   -> 0+  S_ x -> succ $ natVal x 

@@ -1,89 +0,0 @@-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Type.Index.Quote--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ A 'QuasiQuoter' for the 'N' kind and the 'Nat' type.-----------------------------------------------------------------------------------module Data.Type.Nat.Quote where--import Data.Type.Nat-import Type.Family.Nat-import Language.Haskell.TH-import Language.Haskell.TH.Quote-import Control.Monad-import Text.Read (readMaybe)--n :: QuasiQuoter-n = QuasiQuoter-  { quoteExp  = parseNatExp-  , quotePat  = parseNatPat-  , quoteType = parseNatType-  , quoteDec  = error "n: quoteDec not defined"-  }--parseNatExp :: String -> Q Exp-parseNatExp s = maybe (fail $ "n: couldn't parse Int: " ++ show s)-  (notNeg >=> go)-  $ readMaybe s-  where-  notNeg :: Int -> Q Int-  notNeg n-    | n < 0 = fail $ "n: negative: " ++ show n-    | True  = return n-  go :: Int -> Q Exp-  go = \case-    0 -> [| Z_ |]-    n -> [| S_ $(go $ n-1) |]--parseNatPat :: String -> Q Pat-parseNatPat s = maybe (fail $ "n: couldn't parse Int: " ++ show s)-  (notNeg >=> go)-  $ readMaybe s-  where-  notNeg :: Int -> Q Int-  notNeg n-    | n < 0 = fail $ "n: negative: " ++ show n-    | True  = return n-  go :: Int -> Q Pat-  go = \case-    0 -> [p| Z_ |]-    n -> [p| S_ $(go $ n-1) |]--parseNatType :: String -> Q Type-parseNatType s = maybe (fail $ "n: couldn't parse Int: " ++ show s)-  (notNeg >=> go)-  $ readMaybe s-  where-  notNeg :: Int -> Q Int-  notNeg n-    | n < 0 = fail $ "n: negative: " ++ show n-    | True  = return n-  go :: Int -> Q Type-  go = \case-    0 -> [t| Z |]-    n -> [t| S $(go $ n-1) |]-

@@ -1,9 +1,9 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -29,7 +29,7 @@  module Data.Type.Option where -import Type.Class.HFunctor+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Maybe@@ -46,18 +46,18 @@  -- | We can take a natural transformation of @(forall x. f x -> g x)@ to -- a natural transformation of @(forall mx. 'Option' f mx -> 'Option' g mx)@.-instance HFunctor Option where-  map' f = \case+instance Functor1 Option where+  map1 f = \case     Just_ a  -> Just_ $ f a     Nothing_ -> Nothing_ -instance HFoldable Option where-  foldMap' f = \case+instance Foldable1 Option where+  foldMap1 f = \case     Just_ a  -> f a     Nothing_ -> mempty -instance HTraversable Option where-  traverse' f = \case+instance Traversable1 Option where+  traverse1 f = \case     Just_ a  -> Just_ <$> f a     Nothing_ -> pure Nothing_ 

@@ -1,10 +1,11 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -38,22 +39,76 @@  module Data.Type.Product where -import Data.Type.Combinator ((:.:)(..),IT(..),I(..))+import Data.Type.Combinator+import Data.Type.Conjunction import Data.Type.Index import Data.Type.Length-import Type.Class.HFunctor+import Data.Type.Quantifier+import Type.Class.Higher import Type.Class.Known import Type.Class.Witness import Type.Family.Constraint import Type.Family.List -import Control.Arrow ((&&&))- data Prod (f :: k -> *) :: [k] -> * where   Ø    :: Prod f Ø   (:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as) infixr 5 :< +deriving instance ListC (Eq   <$> f <$> as) => Eq   (Prod f as)+deriving instance+  ( ListC (Eq   <$> f <$> as)+  , ListC (Ord  <$> f <$> as)+  ) => Ord  (Prod f as)+deriving instance ListC (Show <$> f <$> as) => Show (Prod f as)++instance Eq1 f => Eq1 (Prod f) where+  eq1 = \case+    Ø -> \case+      Ø -> True+      _ -> False+    a :< as -> \case+      b :< bs -> a =#= b && as =#= bs+      _       -> False++instance Ord1 f => Ord1 (Prod f) where+  compare1 = \case+    Ø -> \case+      Ø -> EQ+      _ -> LT+    a :< as -> \case+      b :< bs -> compare1 a b `mappend` compare1 as bs+      _       -> GT++instance Show1 f => Show1 (Prod f) where+  showsPrec1 d = \case+    Ø -> showString "Ø"+    a :< as -> showParen (d > 5)+      $ showsPrec1 6 a+      . showString " :< "+      . showsPrec1 6 as++instance Read1 f => Read1 (Prod f) where+  readsPrec1 d s0 =+    [ (Some Ø,s1)+    | ("Ø",s1) <- lex s0+    ] ++ readParen (d > 5) ( \s1 ->+      [ (x >>- \a -> xs >>- \as -> Some $ a :< as,s4)+      | (x,s2) <- readsPrec1 6 s1+      , (":<",s3) <- lex s2+      , (xs,s4) <- readsPrec1 5 s3+      ]+    ) s0++instance TestEquality f => TestEquality (Prod f) where+  testEquality = \case+    Ø -> \case+      Ø -> qed+      _ -> Nothing+    a :< as -> \case+      b :< bs -> a =?= b //? as =?= bs //? qed+      _       -> Nothing+ -- | Construct a two element Prod. --   Since the precedence of (:>) is higher than (:<), --   we can conveniently write lists like:@@ -107,6 +162,24 @@   Ø       -> id   a :< as -> (a :<) . append' as +lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a)+lookup' a = \case+  Ø               -> Nothing+  (b :&: v) :< bs -> witMaybe (a =?= b) (Just v) $ lookup' a bs++lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g)+lookupPar a = \case+  Ø               -> Nothing+  (b :*: v) :< bs -> witMaybe (a =?= b) (Just $ Some v) $ lookupPar a bs++permute :: Known Length bs => (forall x. Index bs x -> Index as x) -> Prod f as -> Prod f bs+permute f as = permute' f as known++permute' :: (forall x. Index bs x -> Index as x) -> Prod f as -> Length bs -> Prod f bs+permute' f as = \case+  LZ   -> Ø+  LS l -> index (f IZ) as :< permute' (f . IS) as l+ -- Tuple {{{  -- | A Prod of simple Haskell types.@@ -130,6 +203,11 @@  -- }}} +elimProd :: p Ø -> (forall x xs. Index as x -> f x -> p xs -> p (x :< xs)) -> Prod f as -> p as+elimProd n c = \case+  Ø       -> n+  a :< as -> c IZ a $ elimProd n (c . IS) as+ onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as) onHead' f (a :< as) = f a :< as @@ -147,30 +225,40 @@   IZ -> head'   IS x -> index x . tail' -instance HFunctor Prod where-  map' f = \case+select :: Prod (Index as) bs -> Prod f as -> Prod f bs+select = \case+  Ø     -> pure Ø+  x:<xs -> (:<) <$> index x <*> select xs++instance Functor1 Prod where+  map1 f = \case     Ø -> Ø-    a :< as -> f a :< map' f as+    a :< as -> f a :< map1 f as -instance HIxFunctor Index Prod where-  imap' f = \case+instance IxFunctor1 Index Prod where+  imap1 f = \case     Ø -> Ø-    a :< as -> f IZ a :< imap' (f . IS) as+    a :< as -> f IZ a :< imap1 (f . IS) as -instance HFoldable Prod where-  foldMap' f = \case+instance Foldable1 Prod where+  foldMap1 f = \case     Ø       -> mempty-    a :< as -> f a `mappend` foldMap' f as+    a :< as -> f a `mappend` foldMap1 f as -instance HIxFoldable Index Prod where-  ifoldMap' f = \case+instance IxFoldable1 Index Prod where+  ifoldMap1 f = \case     Ø       -> mempty-    a :< as -> f IZ a `mappend` ifoldMap' (f . IS) as+    a :< as -> f IZ a `mappend` ifoldMap1 (f . IS) as -instance HTraversable Prod where-  traverse' f = \case+instance Traversable1 Prod where+  traverse1 f = \case     Ø       -> pure Ø-    a :< as -> (:<) <$> f a <*> traverse' f as+    a :< as -> (:<) <$> f a <*> traverse1 f as++instance IxTraversable1 Index Prod where+  itraverse1 f = \case+    Ø       -> pure Ø+    a :< as -> (:<) <$> f IZ a <*> itraverse1 (f . IS) as  instance Known (Prod f) Ø where   known = Ø

@@ -1,184 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Type.Product.Dual--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ Type combinators for type-level lists,--- where we have many functors with a single index.-----------------------------------------------------------------------------------module Data.Type.Product.Dual where--import Data.Type.Combinator ((:.:)(..),IT(..),I(..))-import Data.Type.Index-import Data.Type.Length-import Type.Class.HFunctor-import Type.Class.Known-import Type.Class.Witness-import Type.Family.Constraint-import Type.Family.List--import Control.Arrow ((&&&))-import Data.Monoid ((<>))--data FProd (fs :: [k -> *]) :: k -> * where-  ØF   :: FProd Ø a-  (:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a-infixr 5 :<<---- | Construct a two element FProd.---   Since the precedence of (:>>) is higher than (:<<),---   we can conveniently write lists like:------   >>> a :<< b :>> c------   Which is identical to:------   >>> a :<< b :<< c :<< Ø----pattern (:>>) :: (f :: k -> *) (a :: k) -> (g :: k -> *) a -> FProd '[f,g] a-pattern a :>> b = a :<< b :<< ØF-infix 6 :>>---- | Build a singleton FProd.-onlyF :: f a -> FProd '[f] a-onlyF = (:<< ØF)---- | snoc function. insert an element at the end of the FProd.-(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a-(>>:) = \case-  ØF       -> onlyF-  b :<< as -> (b :<<) . (as >>:)-infixl 6 >>:--headF :: FProd (f :< fs) a -> f a-headF (a :<< _) = a--tailF :: FProd (f :< fs) a -> FProd fs a-tailF (_ :<< as) = as---- | Get all but the last element of a non-empty FProd.-initF :: FProd (f :< fs) a -> FProd (Init' f fs) a-initF (a :<< as) = case as of-  ØF     -> ØF-  (:<<){} -> a :<< initF as---- | Get the last element of a non-empty FProd.-lastF :: FProd (f :< fs) a -> Last' f fs a-lastF (a :<< as) = case as of-  ØF      -> a-  (:<<){} -> lastF as---- | Reverse the elements of an FProd.-reverseF :: FProd fs a -> FProd (Reverse fs) a-reverseF = \case-  ØF       -> ØF-  a :<< as -> reverseF as >>: a---- | Append two FProds.-appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a-appendF = \case-  ØF       -> id-  a :<< as -> (a :<<) . appendF as---- | Map over the head of a non-empty FProd.-onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a-onHeadF f (a :<< as) = f a :<< as---- | Map over the tail of a non-empty FProd.-onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a-onTailF f (a :<< as) = a :<< f as--uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r-uncurryF f (a :<< as) = f a as--curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r-curryF f a as = f $ a :<< as--indexF :: Index fs f -> FProd fs a -> f a-indexF = \case-  IZ -> headF-  IS x -> indexF x . tailF---- | If all @f@ in @fs@ are @Functor@s, then @FProd fs@ is a @Functor@.-instance ListC (Functor <$> fs) => Functor (FProd fs) where-  fmap f = \case-    ØF       -> ØF-    a :<< as -> fmap f a :<< fmap f as---- | If all @f@ in @fs@ are @Foldable@s, then @FProd fs@ is a @Foldable@.-instance ListC (Foldable <$> fs) => Foldable (FProd fs) where-  foldMap f = \case-    ØF       -> mempty-    a :<< as -> foldMap f a <> foldMap f as---- | If all @f@ in @fs@ are @Traversable@s, then @FProd fs@ is a @Traversable@.-instance-  ( ListC (Functor     <$> fs)-  , ListC (Foldable    <$> fs)-  , ListC (Traversable <$> fs)-  ) => Traversable (FProd fs) where-  traverse f = \case-    ØF       -> pure ØF-    a :<< as -> (:<<) <$> traverse f a <*> traverse f as---- | Map over all elements of an FProd with access to the element's index.-imapF :: (forall f. Index fs f -> f a -> f b)-  -> FProd fs a -> FProd fs b-imapF f = \case-  ØF       -> ØF-  a :<< as -> f IZ a :<< imapF (f . IS) as---- | Fold over all elements of an FProd with access to the element's index.-ifoldMapF :: Monoid m-  => (forall f. Index fs f -> f a -> m)-  -> FProd fs a -> m-ifoldMapF f = \case-  ØF       -> mempty-  a :<< as -> f IZ a <> ifoldMapF (f . IS) as---- | Traverse over all elements of an FProd with access to the element's index.-itraverseF :: Applicative g-  => (forall f. Index fs f -> f a -> g (f b))-  -> FProd fs a -> g (FProd fs b)-itraverseF f = \case-  ØF       -> pure ØF-  a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as--instance Known (FProd Ø) a where-  known = ØF--instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where-  type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)-  known = known :<< known---- | An empty FProd is a no-op Witness.-instance Witness ØC ØC (FProd Ø a) where-  r \\ _ = r---- | A non-empty FProd is a Witness if both its head and tail are Witnesses.-instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where-  type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))-  r \\ (a :<< as) = r \\ a \\ as-

@@ -0,0 +1,178 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Product.Lifted+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Type combinators for type-level lists,+-- where we have many functors with a single index.+--+-----------------------------------------------------------------------------++module Data.Type.Product.Lifted where++import Data.Type.Index+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.List++import Data.Monoid ((<>))++data FProd (fs :: [k -> *]) :: k -> * where+  ØF   :: FProd Ø a+  (:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a+infixr 5 :<<++-- | Construct a two element FProd.+--   Since the precedence of (:>>) is higher than (:<<),+--   we can conveniently write lists like:+--+--   >>> a :<< b :>> c+--+--   Which is identical to:+--+--   >>> a :<< b :<< c :<< Ø+--+pattern (:>>) :: (f :: k -> *) (a :: k) -> (g :: k -> *) a -> FProd '[f,g] a+pattern a :>> b = a :<< b :<< ØF+infix 6 :>>++-- | Build a singleton FProd.+onlyF :: f a -> FProd '[f] a+onlyF = (:<< ØF)++-- | snoc function. insert an element at the end of the FProd.+(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a+(>>:) = \case+  ØF       -> onlyF+  b :<< as -> (b :<<) . (as >>:)+infixl 6 >>:++headF :: FProd (f :< fs) a -> f a+headF (a :<< _) = a++tailF :: FProd (f :< fs) a -> FProd fs a+tailF (_ :<< as) = as++-- | Get all but the last element of a non-empty FProd.+initF :: FProd (f :< fs) a -> FProd (Init' f fs) a+initF (a :<< as) = case as of+  ØF     -> ØF+  (:<<){} -> a :<< initF as++-- | Get the last element of a non-empty FProd.+lastF :: FProd (f :< fs) a -> Last' f fs a+lastF (a :<< as) = case as of+  ØF      -> a+  (:<<){} -> lastF as++-- | Reverse the elements of an FProd.+reverseF :: FProd fs a -> FProd (Reverse fs) a+reverseF = \case+  ØF       -> ØF+  a :<< as -> reverseF as >>: a++-- | Append two FProds.+appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a+appendF = \case+  ØF       -> id+  a :<< as -> (a :<<) . appendF as++-- | Map over the head of a non-empty FProd.+onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a+onHeadF f (a :<< as) = f a :<< as++-- | Map over the tail of a non-empty FProd.+onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a+onTailF f (a :<< as) = a :<< f as++uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r+uncurryF f (a :<< as) = f a as++curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r+curryF f a as = f $ a :<< as++indexF :: Index fs f -> FProd fs a -> f a+indexF = \case+  IZ -> headF+  IS x -> indexF x . tailF++-- | If all @f@ in @fs@ are @Functor@s, then @FProd fs@ is a @Functor@.+instance ListC (Functor <$> fs) => Functor (FProd fs) where+  fmap f = \case+    ØF       -> ØF+    a :<< as -> fmap f a :<< fmap f as++-- | If all @f@ in @fs@ are @Foldable@s, then @FProd fs@ is a @Foldable@.+instance ListC (Foldable <$> fs) => Foldable (FProd fs) where+  foldMap f = \case+    ØF       -> mempty+    a :<< as -> foldMap f a <> foldMap f as++-- | If all @f@ in @fs@ are @Traversable@s, then @FProd fs@ is a @Traversable@.+instance+  ( ListC (Functor     <$> fs)+  , ListC (Foldable    <$> fs)+  , ListC (Traversable <$> fs)+  ) => Traversable (FProd fs) where+  traverse f = \case+    ØF       -> pure ØF+    a :<< as -> (:<<) <$> traverse f a <*> traverse f as++-- | Map over all elements of an FProd with access to the element's index.+imapF :: (forall f. Index fs f -> f a -> f b)+  -> FProd fs a -> FProd fs b+imapF f = \case+  ØF       -> ØF+  a :<< as -> f IZ a :<< imapF (f . IS) as++-- | Fold over all elements of an FProd with access to the element's index.+ifoldMapF :: Monoid m+  => (forall f. Index fs f -> f a -> m)+  -> FProd fs a -> m+ifoldMapF f = \case+  ØF       -> mempty+  a :<< as -> f IZ a <> ifoldMapF (f . IS) as++-- | Traverse over all elements of an FProd with access to the element's index.+itraverseF :: Applicative g+  => (forall f. Index fs f -> f a -> g (f b))+  -> FProd fs a -> g (FProd fs b)+itraverseF f = \case+  ØF       -> pure ØF+  a :<< as -> (:<<) <$> f IZ a <*> itraverseF (f . IS) as++instance Known (FProd Ø) a where+  known = ØF++instance (Known f a, Known (FProd fs) a) => Known (FProd (f :< fs)) a where+  type KnownC (FProd (f :< fs)) a = (Known f a, Known (FProd fs) a)+  known = known :<< known++-- | An empty FProd is a no-op Witness.+instance Witness ØC ØC (FProd Ø a) where+  r \\ _ = r++-- | A non-empty FProd is a Witness if both its head and tail are Witnesses.+instance (Witness p q (f a), Witness s t (FProd fs a)) => Witness (p,s) (q,t) (FProd (f :< fs) a) where+  type WitnessC (p,s) (q,t) (FProd (f :< fs) a) = (Witness p q (f a), Witness s t (FProd fs a))+  r \\ (a :<< as) = r \\ a \\ as+

@@ -1,9 +1,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -33,8 +31,10 @@  module Data.Type.Quantifier where -import Data.Type.Combinator+import Type.Family.Constraint +-- Some {{{+ data Some (f :: k -> *) :: * where   Some :: f a -> Some f @@ -55,26 +55,82 @@ some :: Some f -> (forall a. f a -> r) -> r some (Some a) f = f a +(>>-) :: Some f -> (forall a. f a -> r) -> r+(>>-) = some+infixl 1 >>-+ withSome :: (forall a. f a -> r) -> Some f -> r withSome f (Some a) = f a -onSome :: (forall a. f a -> g b) -> Some f -> Some g+onSome :: (forall a. f a -> g x) -> Some f -> Some g onSome f (Some a) = Some (f a) -type Some2 f = Some (Some :.: f)+-- }}} -pattern Some2 :: f a b -> Some2 f-pattern Some2 a = Some (Comp (Some a))+-- Some2 {{{ -data All (f :: k -> *) :: * where-  All :: { instAll :: forall (a :: k). f a } -> All f+data Some2 (f :: k -> l -> *) :: * where+  Some2 :: f a b -> Some2 f --- | A data type for natural transformations.-data (f :: k -> *) :-> (g :: k -> *) where-  NT :: (forall a. f a -> g a) -> f :-> g-infixr 4 :->+some2 :: Some2 f -> (forall a b. f a b -> r) -> r+some2 (Some2 a) f = f a -data (p :: k -> l -> *) :--> (q :: k -> l -> *) where-  NT2 :: (forall a b. p a b -> q a b) -> p :--> q-infixr 4 :-->+(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r+(>>--) = some2+infixl 1 >>--++withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r+withSome2 f (Some2 a) = f a++onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g+onSome2 f (Some2 a) = Some2 (f a)++-- }}}++-- Some3 {{{++data Some3 (f :: k -> l -> m -> *) :: * where+  Some3 :: f a b c -> Some3 f++some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r+some3 (Some3 a) f = f a++(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r+(>>---) = some3+infixl 1 >>---++withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r+withSome3 f (Some3 a) = f a++onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g+onSome3 f (Some3 a) = Some3 (f a)++-- }}}++-- SomeC {{{++data SomeC (c :: k -> Constraint) (f :: k -> *) where+  SomeC :: c a => f a -> SomeC c f++someC :: SomeC c f -> (forall a. c a => f a -> r) -> r+someC (SomeC a) f = f a++(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r+(>>~) = someC+infixl 1 >>~++-- }}}++-- EveryN {{{++data Every (f :: k -> *) :: * where+  Every :: { instEvery :: forall a. f a } -> Every f++data Every2 (f :: k -> l -> *) :: * where+  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f++data Every3 (f :: k -> l -> m -> *) :: * where+  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f++-- }}} 

@@ -1,9 +1,10 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -31,17 +32,60 @@ module Data.Type.Sum where  import Data.Type.Index+import Data.Type.Quantifier -import Type.Class.HFunctor+import Type.Class.Higher import Type.Class.Witness -import Type.Family.Constraint import Type.Family.List  data Sum (f :: k -> *) :: [k] -> * where   InL :: !(f a) -> Sum f (a :< as)   InR :: !(Sum f as) -> Sum f (a :< as) +deriving instance ListC (Eq   <$> f <$> as) => Eq   (Sum f as)+deriving instance+  ( ListC (Eq   <$> f <$> as)+  , ListC (Ord  <$> f <$> as)+  ) => Ord  (Sum f as)+deriving instance ListC (Show <$> f <$> as) => Show (Sum f as)++instance Eq1 f => Eq1 (Sum f) where+  eq1 = \case+    InL a -> \case+      InL b -> a =#= b+      _     -> False+    InR a -> \case+      InR b -> a =#= b+      _     -> False++instance Ord1 f => Ord1 (Sum f) where+  compare1 = \case+    InL a -> \case+      InL b -> compare1 a b+      _     -> LT+    InR a -> \case+      InR b -> compare1 a b+      _     -> GT++instance Show1 f => Show1 (Sum f) where+  showsPrec1 d = showParen (d > 10) . \case+    InL a -> showString "InL "+           . showsPrec1 11 a+    InR b -> showString "InR "+           . showsPrec1 11 b++instance Read1 f => Read1 (Sum f) where+  readsPrec1 d = readParen (d > 10) $ \s0 ->+    [ (a >>- Some . InL,s2)+    | ("InL",s1) <- lex s0+    , (a,s2) <- readsPrec1 11 s1+    ] +++    [ (a >>- Some . InR,s2)+    | ("InR",s1) <- lex s0+    , (a,s2) <- readsPrec1 11 s1+    ]+ -- | There are no possible values of the type @Sum f Ø@. nilSum :: Sum f Ø -> Void nilSum = impossible@@ -71,37 +115,45 @@     InR s -> index x s     _     -> Nothing +elimSum :: (forall x xs. f x -> p (x :< xs))+        -> (forall x xs. Index as x -> p xs -> p (x :< xs))+        -> Sum f as+        -> p as+elimSum t n = \case+  InL a -> t a+  InR s -> n IZ $ elimSum t (n . IS) s+ -- instances {{{ -instance HFunctor Sum where-  map' f = \case+instance Functor1 Sum where+  map1 f = \case     InL a -> InL $ f a-    InR s -> InR $ map' f s+    InR s -> InR $ map1 f s -instance HIxFunctor Index Sum where-  imap' f = \case+instance IxFunctor1 Index Sum where+  imap1 f = \case     InL a -> InL $ f IZ a-    InR s -> InR $ imap' (f . IS) s+    InR s -> InR $ imap1 (f . IS) s -instance HFoldable Sum where-  foldMap' f = \case+instance Foldable1 Sum where+  foldMap1 f = \case     InL a -> f a-    InR s -> foldMap' f s+    InR s -> foldMap1 f s -instance HIxFoldable Index Sum where-  ifoldMap' f = \case+instance IxFoldable1 Index Sum where+  ifoldMap1 f = \case     InL a -> f IZ a-    InR s -> ifoldMap' (f . IS) s+    InR s -> ifoldMap1 (f . IS) s -instance HTraversable Sum where-  traverse' f = \case+instance Traversable1 Sum where+  traverse1 f = \case     InL a -> InL <$> f a-    InR s -> InR <$> traverse' f s+    InR s -> InR <$> traverse1 f s -instance HIxTraversable Index Sum where-  itraverse' f = \case+instance IxTraversable1 Index Sum where+  itraverse1 f = \case     InL a -> InL <$> f IZ a-    InR s -> InR <$> itraverse' (f . IS) s+    InR s -> InR <$> itraverse1 (f . IS) s  instance Witness p q (f a) => Witness p q (Sum f '[a]) where   type WitnessC p q (Sum f '[a]) = Witness p q (f a)

@@ -1,125 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Type.Sum.Dual--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ 'FSum' is a type combinators for representing disjoint sums of--- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@.--- As opposed to one-functor-many-indices 'Sum'.-----------------------------------------------------------------------------------module Data.Type.Sum.Dual where--import Data.Type.Index--import Type.Class.HFunctor-import Type.Class.Witness--import Type.Family.Constraint-import Type.Family.List--data FSum :: [k -> *] -> k -> * where-  FInL :: !(f a) -> FSum (f :< fs) a-  FInR :: !(FSum fs a) -> FSum (f :< fs) a---- | There are no possible values of the type @FSum Ø a@.-nilSumF :: FSum Ø a -> Void-nilSumF = impossible---- | Decompose a non-empty FSum into either its head or its tail.-decompF :: FSum (f :< fs) a -> Either (f a) (FSum fs a)-decompF = \case-  FInL a -> Left  a-  FInR s -> Right s---- | Inject an element into an FSum.-injF :: (f ∈ fs) => f a -> FSum fs a-injF = injectFSum elemIndex---- | Project an implicit index out of an FSum.-prjF :: (f ∈ fs) => FSum fs a -> Maybe (f a)-prjF = indexF elemIndex---- | Inject an element into an FSum with an explicitly---   specified Index.-injectFSum :: Index fs f -> f a -> FSum fs a-injectFSum = \case-  IZ   -> FInL-  IS x -> FInR . injectFSum x---- | Project an explicit index out of an FSum.-indexF :: Index fs f -> FSum fs a -> Maybe (f a)-indexF = \case-  IZ -> \case-    FInL a -> Just a-    _      -> Nothing-  IS x -> \case-    FInR s -> indexF x s-    _      -> Nothing--instance ListC (Functor <$> fs) => Functor (FSum fs) where-  fmap f = \case-    FInL a -> FInL $ f <$> a-    FInR s -> FInR $ f <$> s--instance ListC (Foldable <$> fs) => Foldable (FSum fs) where-  foldMap f = \case-    FInL a -> foldMap f a-    FInR s -> foldMap f s--instance-  ( ListC (Functor     <$> fs)-  , ListC (Foldable    <$> fs)-  , ListC (Traversable <$> fs)-  ) => Traversable (FSum fs) where-  traverse f = \case-    FInL a -> FInL <$> traverse f a-    FInR s -> FInR <$> traverse f s---- | Map over the single element in an FSum---   with a function that can handle any possible---   element, along with the element's index.-imapF :: (forall f. Index fs f -> f a -> f b)-  -> FSum fs a -> FSum fs b-imapF f = \case-  FInL a -> FInL $ f IZ a-  FInR s -> FInR $ imapF (f . IS) s---- | Fun fact: Since there is exactly one element in---   an FSum, we don't need the @Monoid@ instance!-ifoldMapF :: (forall f. Index fs f -> f a -> m)-  -> FSum fs a -> m-ifoldMapF f = \case-  FInL a -> f IZ a-  FInR s -> ifoldMapF (f . IS) s---- | Another fun fact: Since there is exactly one element in---   an FSum, we require only a @Functor@ instance on @g@, rather---   than @Applicative@.-itraverseF :: Functor g-  => (forall f. Index fs f -> f a -> g (f b))-  -> FSum fs a -> g (FSum fs b)-itraverseF f = \case-  FInL a -> FInL <$> f IZ a-  FInR s -> FInR <$> itraverseF (f . IS) s-

@@ -0,0 +1,119 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Sum.Lifted+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- 'FSum' is a type combinators for representing disjoint sums of+-- many functors @(fs :: [k -> *])@ at a single index @(a :: k)@.+-- As opposed to one-functor-many-indices 'Sum'.+--+-----------------------------------------------------------------------------++module Data.Type.Sum.Lifted where++import Data.Type.Index+import Type.Class.Witness+import Type.Family.List++data FSum :: [k -> *] -> k -> * where+  FInL :: !(f a) -> FSum (f :< fs) a+  FInR :: !(FSum fs a) -> FSum (f :< fs) a++-- | There are no possible values of the type @FSum Ø a@.+nilFSum :: FSum Ø a -> Void+nilFSum = impossible++-- | Decompose a non-empty FSum into either its head or its tail.+fdecomp :: FSum (f :< fs) a -> Either (f a) (FSum fs a)+fdecomp = \case+  FInL a -> Left  a+  FInR s -> Right s++-- | Inject an element into an FSum.+finj :: (f ∈ fs) => f a -> FSum fs a+finj = injectFSum elemIndex++-- | Project an implicit index out of an FSum.+fprj :: (f ∈ fs) => FSum fs a -> Maybe (f a)+fprj = findex elemIndex++-- | Inject an element into an FSum with an explicitly+--   specified Index.+injectFSum :: Index fs f -> f a -> FSum fs a+injectFSum = \case+  IZ   -> FInL+  IS x -> FInR . injectFSum x++-- | Project an explicit index out of an FSum.+findex :: Index fs f -> FSum fs a -> Maybe (f a)+findex = \case+  IZ -> \case+    FInL a -> Just a+    _      -> Nothing+  IS x -> \case+    FInR s -> findex x s+    _      -> Nothing++instance ListC (Functor <$> fs) => Functor (FSum fs) where+  fmap f = \case+    FInL a -> FInL $ f <$> a+    FInR s -> FInR $ f <$> s++instance ListC (Foldable <$> fs) => Foldable (FSum fs) where+  foldMap f = \case+    FInL a -> foldMap f a+    FInR s -> foldMap f s++instance+  ( ListC (Functor     <$> fs)+  , ListC (Foldable    <$> fs)+  , ListC (Traversable <$> fs)+  ) => Traversable (FSum fs) where+  traverse f = \case+    FInL a -> FInL <$> traverse f a+    FInR s -> FInR <$> traverse f s++-- | Map over the single element in an FSum+--   with a function that can handle any possible+--   element, along with the element's index.+imapFSum :: (forall f. Index fs f -> f a -> f b)+  -> FSum fs a -> FSum fs b+imapFSum f = \case+  FInL a -> FInL $ f IZ a+  FInR s -> FInR $ imapFSum (f . IS) s++-- | Fun fact: Since there is exactly one element in+--   an FSum, we don't need the @Monoid@ instance!+ifoldMapFSum :: (forall f. Index fs f -> f a -> m)+  -> FSum fs a -> m+ifoldMapFSum f = \case+  FInL a -> f IZ a+  FInR s -> ifoldMapFSum (f . IS) s++-- | Another fun fact: Since there is exactly one element in+--   an FSum, we require only a @Functor@ instance on @g@, rather+--   than @Applicative@.+itraverseFSum :: Functor g+  => (forall f. Index fs f -> f a -> g (f b))+  -> FSum fs a -> g (FSum fs b)+itraverseFSum f = \case+  FInL a -> FInL <$> f IZ a+  FInR s -> FInR <$> itraverseFSum (f . IS) s+

@@ -0,0 +1,66 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Sym+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- A @singleton@-esque type for representing type-level Symbols.+--+-----------------------------------------------------------------------------++module Data.Type.Sym where++import Type.Class.Higher+import Type.Class.Known+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.Symbol+import Data.Proxy++data Sym :: Symbol -> * where+  Sym :: KnownSymbol x => Sym x++deriving instance Eq   (Sym x)+deriving instance Ord  (Sym x)++instance Show (Sym x) where+  showsPrec d x = showParen (d > 0)+    $ showString "Sym :: Sym "+    . shows (symbol x)++instance Eq1   Sym+instance Ord1  Sym+instance Show1 Sym++instance TestEquality Sym where+  testEquality Sym Sym = sameSymbol Proxy Proxy++instance KnownSymbol x => Known Sym x where+  type KnownC Sym x = KnownSymbol x+  known = Sym++instance Witness ØC (KnownSymbol x) (Sym x) where+  r \\ Sym = r++symbol :: Sym x -> String+symbol x = symbolVal x \\ x+

@@ -6,7 +6,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}@@ -44,7 +44,6 @@ import Data.Type.Nat import Data.Type.Product (Prod(..),curry',pattern (:>)) -import Type.Class.HFunctor import Type.Class.Known import Type.Class.Witness @@ -52,18 +51,28 @@ import Type.Family.List import Type.Family.Nat -import Control.Applicative-import Control.Arrow-import Control.Monad (join) import qualified Data.List as L import Data.Monoid-import qualified Data.Foldable as F  data VT (n :: N) (f :: k -> *) :: k -> * where   ØV   :: VT Z f a   (:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a infixr 4 :* +elimVT :: p Z+       -> (forall x. f a -> p x -> p (S x))+       -> VT n f a+       -> p n+elimVT z s = \case+  ØV      -> z+  a :* as -> s a $ elimVT z s as++elimV :: p Z+      -> (forall x. a -> p x -> p (S x))+      -> V n a+      -> p n+elimV z s = elimVT z $ s . getI+ type V n = VT n I pattern (:+) :: a -> V n a -> V (S n) a pattern a :+ as = I a :* as@@ -151,8 +160,8 @@  withVT :: [f a] -> (forall n. VT n f a -> r) -> r withVT as k = case as of-  []     -> k ØV-  a : as -> withVT as $ \v -> k $ a :* v+  []      -> k ØV+  a : as' -> withVT as' $ \v -> k $ a :* v  withV :: [a] -> (forall n. V n a -> r) -> r withV as k = withVT (I <$> as) k@@ -290,9 +299,9 @@ mzipWith :: Monoid a => (a -> a -> b) -> [a] -> [a] -> [b] mzipWith f as bs = case (as,bs) of   ([]  ,[]  ) -> []-  (a:as,[]  ) -> f a      mempty : mzipWith f as []-  ([]  ,b:bs) -> f mempty b      : mzipWith f [] bs-  (a:as,b:bs) -> f a      b      : mzipWith f as bs+  (a:as',[]  ) -> f a      mempty  : mzipWith f as' []+  ([]   ,b:bs') -> f mempty b      : mzipWith f []  bs'+  (a:as',b:bs') -> f a      b      : mzipWith f as' bs'  zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS zipLines f a b = compose $ L.intersperse (showChar '\n') $ mzipWith

@@ -1,56 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}--------------------------------------------------------------------------------- |--- Module      :  Type.Class.HFunctor--- Copyright   :  Copyright (C) 2015 Kyle Carter--- License     :  BSD3------ Maintainer  :  Kyle Carter <kylcarte@indiana.edu>--- Stability   :  experimental--- Portability :  RankNTypes------ Higher order functors, foldables, and traversables,--- along with their indexed variants.--- (oh, and bifunctors tacked on for good measure.)-------------------------------------------------------------------------------module Type.Class.HFunctor where--class HFunctor (t :: (k -> *) -> l -> *) where-  -- | Take a natural transformation to a lifted natural transformation.-  map' :: (forall (a :: k). f a -> g a) -> t f b -> t g b--class HIxFunctor (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where-  imap' :: (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b--class HFoldable (t :: (k -> *) -> l -> *) where-  foldMap' :: Monoid m => (forall (a :: k). f a -> m) -> t f b -> m--class HIxFoldable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where-  ifoldMap' :: Monoid m => (forall (a :: k). i b a -> f a -> m) -> t f b -> m--class (HFunctor t, HFoldable t) => HTraversable (t :: (k -> *) -> l -> *) where-  traverse' :: Applicative h => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)--class (HIxFunctor i t, HIxFoldable i t) => HIxTraversable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where-  itraverse' :: Applicative h => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)--class HBifunctor (t :: (k -> *) -> (l -> *) -> m -> *) where-  bimap' :: (forall (a :: k). f a -> h a)-         -> (forall (a :: l). g a -> i a)-         -> t f g b-         -> t h i b-

@@ -0,0 +1,236 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Type.Class.Higher+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Higher order analogs of type classes from the Prelude.+----------------------------------------------------------------------------++module Type.Class.Higher where++import Data.Type.Quantifier++-- EqN {{{++class Eq1 (f :: k -> *) where+  eq1 :: f a -> f a -> Bool+  default eq1 :: Eq (f a) => f a -> f a -> Bool+  eq1 = (==)+  neq1 :: f a -> f a -> Bool+  neq1 a b = not $ eq1 a b++(=#=) :: Eq1 f => f a -> f a -> Bool+(=#=) = eq1+infix 4 =#=++class Eq2 (f :: k -> l -> *) where+  eq2 :: f a b -> f a b -> Bool+  default eq2 :: Eq (f a b) => f a b -> f a b -> Bool+  eq2 = (==)+  neq2 :: f a b -> f a b -> Bool+  neq2 a b = not $ eq2 a b++(=##=) :: Eq2 f => f a b -> f a b -> Bool+(=##=) = eq2+infix 4 =##=++class Eq3 (f :: k -> l -> m -> *) where+  eq3 :: f a b c -> f a b c -> Bool+  default eq3 :: Eq (f a b c ) => f a b c -> f a b c -> Bool+  eq3 = (==)+  neq3 :: f a b c -> f a b c -> Bool+  neq3 a b = not $ eq3 a b++(=###=) :: Eq3 f => f a b c -> f a b c -> Bool+(=###=) = eq3+infix 4 =###=++-- }}}++-- OrdN {{{++class Eq1 f => Ord1 (f :: k -> *) where+  compare1 :: f a -> f a -> Ordering+  default compare1 :: Ord (f a) => f a -> f a -> Ordering+  compare1 = compare+  (<#) :: f a -> f a -> Bool+  a <# b = compare1 a b == LT+  (>#) :: f a -> f a -> Bool+  a ># b = compare1 a b == GT+  (<=#) :: f a -> f a -> Bool+  a <=# b = compare1 a b /= GT+  (>=#) :: f a -> f a -> Bool+  a >=# b = compare1 a b /= LT+infix 4 <#, >#, <=#, >=#++class Eq2 f => Ord2 (f :: k -> l -> *) where+  compare2 :: f a b -> f a b -> Ordering+  default compare2 :: Ord (f a b) => f a b -> f a b -> Ordering+  compare2 = compare+  (<##) :: f a b -> f a b -> Bool+  a <## b = compare2 a b == LT+  (>##) :: f a b -> f a b -> Bool+  a >## b = compare2 a b == GT+  (<=##) :: f a b -> f a b -> Bool+  a <=## b = compare2 a b /= GT+  (>=##) :: f a b -> f a b -> Bool+  a >=## b = compare2 a b /= LT+infix 4 <##, >##, <=##, >=##++class Eq3 f => Ord3 (f :: k -> l -> m -> *) where+  compare3 :: f a b c -> f a b c -> Ordering+  default compare3 :: Ord (f a b c) => f a b c -> f a b c -> Ordering+  compare3 = compare+  (<###) :: f a b c -> f a b c -> Bool+  a <### b = compare3 a b == LT+  (>###) :: f a b c -> f a b c -> Bool+  a >### b = compare3 a b == GT+  (<=###) :: f a b c -> f a b c -> Bool+  a <=### b = compare3 a b /= GT+  (>=###) :: f a b c -> f a b c -> Bool+  a >=### b = compare3 a b /= LT+infix 4 <###, >###, <=###, >=###++-- }}}++-- ShowN {{{++class Show1 (f :: k -> *) where+  showsPrec1 :: Int -> f a -> ShowS+  default showsPrec1 :: Show (f a) => Int -> f a -> ShowS+  showsPrec1 = showsPrec+  show1 :: f a -> String+  show1 = ($ "") . shows1++shows1 :: Show1 f => f a -> ShowS+shows1 = showsPrec1 0+++class Show2 (f :: k -> l -> *) where+  showsPrec2 :: Int -> f a b -> ShowS+  default showsPrec2 :: Show (f a b) => Int -> f a b -> ShowS+  showsPrec2 = showsPrec+  show2 :: f a b -> String+  show2 = ($ "") . shows2++shows2 :: Show2 f => f a b -> ShowS+shows2 = showsPrec2 0+++class Show3 (f :: k -> l -> m -> *) where+  showsPrec3 :: Int -> f a b c -> ShowS+  default showsPrec3 :: Show (f a b c) => Int -> f a b c -> ShowS+  showsPrec3 = showsPrec+  show3 :: f a b c -> String+  show3 = ($ "") . shows3++shows3 :: Show3 f => f a b c -> ShowS+shows3 = showsPrec3 0++-- }}}++-- ReadN {{{++class Read1 (f :: k -> *) where+  readsPrec1 :: Int -> ReadS (Some f)++reads1 :: Read1 f => ReadS (Some f)+reads1 = readsPrec1 0++readMaybe1 :: Read1 f => String -> Maybe (Some f)+readMaybe1 s = case reads1 s of+  [(f,"")] -> Just f+  _        -> Nothing+++class Read2 (f :: k -> l -> *) where+  readsPrec2 :: Int -> ReadS (Some2 f)++reads2 :: Read2 f => ReadS (Some2 f)+reads2 = readsPrec2 0++readMaybe2 :: Read2 f => String -> Maybe (Some2 f)+readMaybe2 s = case reads2 s of+  [(f,"")] -> Just f+  _        -> Nothing+++class Read3 (f :: k -> l -> m -> *) where+  readsPrec3 :: Int -> ReadS (Some3 f)++reads3 :: Read3 f => ReadS (Some3 f)+reads3 = readsPrec3 0++readMaybe3 :: Read3 f => String -> Maybe (Some3 f)+readMaybe3 s = case reads3 s of+  [(f,"")] -> Just f+  _        -> Nothing++-- }}}++-- FunctorN {{{++class Functor1 (t :: (k -> *) -> l -> *) where+  -- | Take a natural transformation to a lifted natural transformation.+  map1 :: (forall (a :: k). f a -> g a) -> t f b -> t g b++class IxFunctor1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  imap1 :: (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b++-- }}}++-- FoldableN {{{++class Foldable1 (t :: (k -> *) -> l -> *) where+  foldMap1 :: Monoid m => (forall (a :: k). f a -> m) -> t f b -> m++class IxFoldable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  ifoldMap1 :: Monoid m => (forall (a :: k). i b a -> f a -> m) -> t f b -> m++-- }}}++-- TraversableN {{{++class (Functor1 t, Foldable1 t) => Traversable1 (t :: (k -> *) -> l -> *) where+  traverse1 :: Applicative h => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)++class (IxFunctor1 i t, IxFoldable1 i t) => IxTraversable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i where+  itraverse1 :: Applicative h => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)++-- }}}++-- BifunctorN {{{++class Bifunctor1 (t :: (k -> *) -> (l -> *) -> m -> *) where+  bimap1 :: (forall (a :: k). f a -> h a)+         -> (forall (a :: l). g a -> i a)+         -> t f g b+         -> t h i b++class IxBifunctor1 (i :: m -> k -> *) (j :: m -> l -> *) (t :: (k -> *) -> (l -> *) -> m -> *) | t -> i j where+  ibimap1 :: (forall (a :: k). i b a -> f a -> f' a)+          -> (forall (a :: l). j b a -> g a -> g' a)+          -> t f  g  b+          -> t f' g' b++-- }}}+

@@ -1,9 +1,8 @@+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE LambdaCase #-}

@@ -1,3 +1,6 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ConstraintKinds #-}@@ -47,12 +50,16 @@ import Type.Family.Constraint  import Data.Type.Equality as Exports-import Data.Void          as Exports+import Data.Void          as Exports hiding (absurd)+import qualified Data.Void as Void  import Prelude hiding (id,(.)) import Control.Category+import Control.Arrow import Unsafe.Coerce +-- Wit {{{+ -- | A reified 'Constraint'. data Wit :: Constraint -> * where   Wit :: c => Wit c@@ -60,6 +67,10 @@ data Wit1 :: (k -> Constraint) -> k -> * where   Wit1 :: c a => Wit1 c a +-- }}}++-- (:-) {{{+ -- | Reified evidence of 'Constraint' entailment. -- -- Given a term of @p :- q@, the Constraint @q@ holds@@ -77,9 +88,10 @@   id              = Sub Wit   Sub bc . Sub ab = Sub $ bc \\ ab -type (:-:) = Bij (:-)-infixr 4 :-:+-- }}} +-- Witness {{{+ -- | A general eliminator for entailment. -- -- Given a term of type @t@ with an instance @Witness p q t@@@ -94,17 +106,96 @@   (\\) :: p => (q => r) -> t -> r infixl 1 \\ +-- | Convert a 'Witness' to a canonical reified 'Constraint'.+witnessed :: Witness ØC q t => t -> Wit q+witnessed t = Wit \\ t+ -- | Convert a 'Witness' to a canonical reified entailment. entailed :: Witness p q t => t -> p :- q entailed t = Sub (Wit \\ t) --- | Convert a 'Witness' to a canonical reified 'Constraint'.-witnessed :: Witness ØC q t => t -> Wit q-witnessed t = Wit \\ t+-- }}} +-- Constraint Combinators {{{++class Fails (c :: Constraint) where+  failC :: c :- Fail++absurdC :: Fails a => a :- b+absurdC = contraC failC++class c => Const (c :: Constraint) (d :: k) where+  constC :: Wit c++instance c => Const c d where+  constC = Wit++class f (g a) => (∘) (f :: l -> Constraint) (g :: k -> l) (a :: k) where+  compC :: Wit (f (g a))++instance f (g a) => (f ∘ g) a where+  compC = Wit+infixr 9 ∘++class (f a,g a) => (∧) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k) where+  conjC :: (Wit (f a),Wit (g a))+infixr 7 ∧++instance (f a,g a) => (f ∧ g) a where+  conjC = (Wit,Wit)++class (∨) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k) where+  disjC :: Either (Wit (f a)) (Wit (g a))+infixr 6 ∨++eitherC :: forall f g a b. f a :- b -> g a :- b -> (f ∨ g) a :- b+eitherC f g = Sub $ case ((disjC :: Either (Wit (f a)) (Wit (g a))),f,g) of+  (Left  a,Sub b,_    ) -> b \\ a+  (Right a,_    ,Sub b) -> b \\ a++pureC :: b => a :- b+pureC = Sub Wit++contraC :: a :- Fail -> a :- b+contraC = (bottom .)++-- }}}++-- Forall {{{++class Forall (p :: k -> Constraint) (q :: k -> Constraint) where+  forall :: p a :- q a+  default forall :: q a => p a :- q a+  forall = pureC++-- }}}++-- Initial/Terminal {{{++commute :: (a ~ b) :- (b ~ a)+commute = Sub Wit++type family Holds (b :: Bool) (c :: Constraint) :: Constraint where+  Holds True  c = c+  Holds False c = ØC++falso :: (b ~ False) :- Holds b c+falso = Sub Wit++top :: a :- ØC+top = Sub Wit++type Fail = (True ~ False)++bottom :: Fail :- c+bottom = falso+ instance Witness ØC c (Wit c) where   r \\ Wit = r +instance Witness ØC (c a) (Wit1 c a) where+  r \\ Wit1 = r+ -- | An entailment @p :- q@ is a Witness of @q@, given @p@. instance Witness p q (p :- q) where   r \\ Sub Wit = r@@ -119,19 +210,43 @@   type KnownC Wit c = c   known = Wit +instance c a => Known (Wit1 c) a where+  type KnownC (Wit1 c) a = c a+  known = Wit1+ -- | Constraint chaining under @Maybe@.-(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r-(/?) = \case+(//?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r+(//?) = \case   Just t -> (\\ t)   _      -> \_ -> Nothing-infixr 0 /?+infixr 0 //? +witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r+witMaybe mt y n = case mt of+  Just t -> y \\ t+  _      -> n+ qed :: Maybe (a :~: a) qed = Just Refl  impossible :: a -> Void impossible = unsafeCoerce +(=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b)+(=?=) = testEquality+infix 4 =?=++class TestEquality1 (f :: k -> l -> *) where+  testEquality1 :: f a c -> f b c -> Maybe (a :~: b)++(=??=) :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b)+(=??=) = testEquality1+infix 4 =??=++-- }}}++-- Dec {{{+ data Dec a   = Proven   a   | Refuted (a -> Void)@@ -147,22 +262,14 @@   Proven  a -> y a   Refuted b -> n b -data Bij p a b = Bij-  { fwd :: p a b-  , bwd :: p b a-  }--($->) :: Bij p a b -> p a b-($->) = fwd-(<-$) :: Bij p a b -> p b a-(<-$) = bwd-infixr 1 $->, <-$+-- }}} -instance Category p => Category (Bij p) where-  id    = Bij id id-  g . f = Bij (fwd g . fwd f) (bwd f . bwd g)+absurd :: Arrow p => p Void a+absurd = arr Void.absurd  {-+-- Category Classes {{{+ class Category c => Monoidal (c :: k -> k -> *) where   type Tensor c :: k -> k -> k   type Unit   c :: k@@ -197,17 +304,7 @@ (***) :: Monoidal p => Bij p a b -> Bij p c d -> Bij p (Tensor p a c) (Tensor p b d) f *** g = (fwd f .*. fwd g) <-> (bwd f .*. bwd g) infixr 3 ***--} -type (<->) = Bij (->)-infixr 5 <->--(<->) :: p a b -> p b a -> Bij p a b-(<->) = Bij--(<?>) :: r <-> s -> Dec r -> Dec s-(<?>) p = \case-  Proven  a -> Proven  $ p $-> a-  Refuted f -> Refuted $ \a -> f $ p <-$ a-infix 3 <?>+-- }}}+-} 

@@ -0,0 +1,105 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Type.Family.Either+-- Copyright   :  Copyright (C) 2015 Kyle Carter+-- License     :  BSD3+--+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>+-- Stability   :  experimental+-- Portability :  RankNTypes+--+-- Convenient type families for working with type-level @Either@s.+----------------------------------------------------------------------------++module Type.Family.Either where++import Type.Family.Constraint+import Type.Family.Monoid+import Type.Class.Witness++-- | Take a @Maybe Constraint@ to a @Constraint@.+type family EitherC (ec :: Either k Constraint) :: Constraint where+  EitherC (Left  a) = ØC+  EitherC (Right c) = c++type family IsLeft (a :: Either k l) :: Bool where+  IsLeft (Left  a) = True+  IsLeft (Right b) = False++type family IsRight (a :: Either k l) :: Bool where+  IsRight (Left  a) = False+  IsRight (Right b) = True++leftCong :: (a ~ b) :- (IsLeft a ~ IsLeft b)+leftCong = Sub Wit++rightCong :: (a ~ b) :- (IsRight a ~ IsRight b)+rightCong = Sub Wit++leftNotRight :: (Left a ~ Right b) :- Fail+leftNotRight = leftCong++-- | Map over a type-level @Maybe@.+type family (f :: k -> l) <$> (a :: Either m k) :: Either m l where+  f <$> Left  a = Left a+  f <$> Right b = Right (f b)+infixr 4 <$>++eitherFmapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))+eitherFmapCong = Sub Wit++type family (f :: Either m (k -> l)) <&> (a :: k) :: Either m l where+  Left  x <&> a = Left x+  Right f <&> a = Right (f a)+infixl 5 <&>++eitherPamfCong :: (f ~ g,a ~ b) :- ((f <&> a) ~ (g <&> b))+eitherPamfCong = Sub Wit++type family (f :: Either m (k -> l)) <*> (a :: Either m k) :: Either m l where+  Left  x <*> Left y  = Left (x <> y)+  Left  x <*> a       = Left x+  f       <*> Left x  = Left x+  Right f <*> Right a = Right (f a)+infixr 4 <*>++eitherApCong :: (f ~ g,a ~ b) :- ((f <*> a) ~ (g <*> b))+eitherApCong = Sub Wit++type family (a :: Either m k) <|> (b :: Either m k) :: Either m k where+  Left  x <|> b = b+  Right a <|> b = Right a+infixr 4 <|>++eitherAltCong :: (a ~ c,b ~ d) :- ((a <|> b) ~ (c <|> d))+eitherAltCong = Sub Wit++type family FromLeft (e :: Either k l) :: k where+  FromLeft (Left a) = a++type family FromRight (e :: Either k l) :: l where+  FromRight (Right b) = b++fromLeftCong :: (a ~ b) :- (FromLeft a ~ FromLeft b)+fromLeftCong = Sub Wit++fromRightCong :: (a ~ b) :- (FromRight a ~ FromRight b)+fromRightCong = Sub Wit++type instance Mempty = Left Mempty+type instance a <> b = a <|> b+

@@ -26,16 +26,12 @@ -- type-level lists. ---------------------------------------------------------------------------- -module Type.Family.List-  ( module Type.Family.List-  , (==)-  ) where+module Type.Family.List where  import Type.Family.Constraint import Type.Family.Monoid--import Data.Type.Bool-import Data.Type.Equality+import Type.Family.Tuple hiding (type (<$>),type (<*>),type (<&>))+import Type.Class.Witness  type Ø    = '[] type (:<) = '(:)@@ -44,30 +40,79 @@ -- | Type-level singleton list. type Only a = '[a] +-- Null,Append {{{++type family Null (as :: [k]) :: Bool where+  Null Ø         = True+  Null (a :< as) = False++nullCong :: (a ~ b) :- (Null a ~ Null b)+nullCong = Sub Wit++nilNotCons :: (Ø ~ (a :< as)) :- Fail+nilNotCons = nullCong+ -- | Appends two type-level lists. type family (as :: [k]) ++ (bs :: [k]) :: [k] where   Ø         ++ bs = bs   (a :< as) ++ bs = a :< (as ++ bs) infixr 5 ++ +appendCong :: (a ~ b,c ~ d) :- ((a ++ c) ~ (b ++ d))+appendCong = Sub Wit++-- }}}++-- Snoc,Reverse {{{+ -- | Type-level list snoc. type family (as :: [k]) >: (a :: k) :: [k] where   Ø         >: a = Only a   (b :< as) >: a = b :< (as >: a) infixl 6 >: +snocCong :: (as ~ bs,a ~ b) :- ((as >: a) ~ (bs >: b))+snocCong = Sub Wit+ type family Reverse (as :: [k]) :: [k] where   Reverse  Ø        = Ø   Reverse (a :< as) = Reverse as >: a +reverseCong :: (as ~ bs) :- (Reverse as ~ Reverse bs)+reverseCong = Sub Wit++-- }}}++-- Head,Tail,Init,Last {{{++type family Head (as :: [k]) :: k where+  Head (a :< as) = a++type family Tail (as :: [k]) :: [k] where+  Tail (a :< as) = as++type family Init (as :: [k]) :: [k] where+  Init (a :< as) = Init' a as+ type family Init' (a :: k) (as :: [k]) :: [k] where   Init' a Ø = Ø   Init' a (b :< as) = a :< Init' b as +initCong :: (a ~ b,as ~ bs) :- (Init' a as ~ Init' b bs)+initCong = Sub Wit++type family Last (as :: [k]) :: k where+  Last (a :< as) = Last' a as+ type family Last' (a :: k) (as :: [k]) :: k where   Last' a Ø         = a   Last' a (b :< as) = Last' b as +lastCong :: (a ~ b,as ~ bs) :- (Last' a as ~ Last' b bs)+lastCong = Sub Wit++-- }}}+ -- | Takes a type-level list of 'Constraint's to a single -- 'Constraint', where @ListC cs@ holds iff all elements -- of @cs@ hold.@@ -75,6 +120,8 @@   ListC  Ø        = ØC   ListC (c :< cs) = (c, ListC cs) +-- Map et al {{{+ -- | Map an @(f :: k -> l)@ over a type-level list @(as :: [k])@, -- giving a list @(bs :: [l])@. type family (f :: k -> l) <$> (a :: [k]) :: [l] where@@ -82,6 +129,9 @@   f <$> (a :< as) = f a :< (f <$> as) infixr 4 <$> +listMapCong :: (f ~ g,as ~ bs) :- ((f <$> as) ~ (g <$> bs))+listMapCong = Sub Wit+ -- | Map a list of @(fs :: [k -> l])@ over a single @(a :: k)@, -- giving a list @(bs :: [l])@. type family (f :: [k -> l]) <&> (a :: k) :: [l] where@@ -93,6 +143,36 @@   fs <*> Ø         = Ø   fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as) infixr 4 <*>++-- }}}++-- Tuples {{{++type family Fsts (ps :: [(k,l)]) :: [k] where+  Fsts  Ø        = Ø+  Fsts (p :< ps) = Fst p :< Fsts ps++type family Snds (ps :: [(k,l)]) :: [l] where+  Snds  Ø        = Ø+  Snds (p :< ps) = Snd p :< Snds ps++type family Zip (as :: [k]) (bs :: [l]) :: [(k,l)] where+  Zip  Ø         Ø        = Ø+  Zip (a :< as) (b :< bs) = a#b :< Zip as bs++type family Fsts3 (ps :: [(k,l,m)]) :: [k] where+  Fsts3  Ø        = Ø+  Fsts3 (p :< ps) = Fst3 p :< Fsts3 ps++type family Snds3 (ps :: [(k,l,m)]) :: [l] where+  Snds3  Ø        = Ø+  Snds3 (p :< ps) = Snd3 p :< Snds3 ps++type family Thds3 (ps :: [(k,l,m)]) :: [m] where+  Thds3  Ø        = Ø+  Thds3 (p :< ps) = Thd3 p :< Thds3 ps++-- }}}  type instance Mempty = Ø type instance a <> b = a ++ b

@@ -25,46 +25,67 @@ -- Convenient type families for working with type-level @Maybe@s. ---------------------------------------------------------------------------- -module Type.Family.Maybe-  ( module Type.Family.Maybe-  , type (==)-  ) where+module Type.Family.Maybe where  import Type.Family.Constraint import Type.Family.Monoid--import Data.Type.Equality+import Type.Class.Witness  -- | Take a @Maybe Constraint@ to a @Constraint@. type family MaybeC (mc :: Maybe Constraint) :: Constraint where   MaybeC Nothing  = ØC   MaybeC (Just c) = c +type family IsNothing (a :: Maybe k) :: Bool where+  IsNothing Nothing  = True+  IsNothing (Just a) = False++nothingCong :: (a ~ b) :- (IsNothing a ~ IsNothing b)+nothingCong = Sub Wit++nothingNotJust :: (Nothing ~ Just a) :- Fail+nothingNotJust = nothingCong+ -- | Map over a type-level @Maybe@. type family (f :: k -> l) <$> (a :: Maybe k) :: Maybe l where   f <$> Nothing = Nothing   f <$> Just a  = Just (f a) infixr 4 <$> +maybeFmapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))+maybeFmapCong = Sub Wit+ type family (f :: Maybe (k -> l)) <&> (a :: k) :: Maybe l where   Nothing <&> a = Nothing   Just f  <&> a = Just (f a) infixl 5 <&> +maybePamfCong :: (f ~ g,a ~ b) :- ((f <&> a) ~ (g <&> b))+maybePamfCong = Sub Wit+ type family (f :: Maybe (k -> l)) <*> (a :: Maybe k) :: Maybe l where   Nothing <*> a       = Nothing   f       <*> Nothing = Nothing   Just f  <*> Just a  = Just (f a) infixr 4 <*> +maybeApCong :: (f ~ g,a ~ b) :- ((f <*> a) ~ (g <*> b))+maybeApCong = Sub Wit+ type family (a :: Maybe k) <|> (b :: Maybe k) :: Maybe k where   Nothing <|> a       = a   a       <|> Nothing = a   Just a  <|> Just b  = Just a infixr 4 <|> +maybeAltCong :: (a ~ c,b ~ d) :- ((a <|> b) ~ (c <|> d))+maybeAltCong = Sub Wit+ type family FromJust (m :: Maybe k) :: k where   FromJust (Just a) = a++fromJustCong :: (a ~ b) :- (FromJust a ~ FromJust b)+fromJustCong = Sub Wit  type instance Mempty = Nothing type instance a <> b = a <|> b

@@ -27,19 +27,33 @@ -- ----------------------------------------------------------------------------- -module Type.Family.Nat-  ( module Type.Family.Nat-  , type (==)-  ) where+module Type.Family.Nat where  import Data.Type.Equality import Type.Family.List+import Type.Class.Witness  data N   = Z   | S N   deriving (Eq,Ord,Show) +fromInt :: Int -> Maybe N+fromInt n = case compare n 0 of+  LT -> Nothing+  EQ -> Just Z+  GT -> S <$> fromInt (n-1)++type family IsZero (x :: N) :: Bool where+  IsZero Z     = True+  IsZero (S x) = False++zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)+zeroCong = Sub Wit++zNotS :: (Z ~ S x) :- Fail+zNotS = zeroCong+ type family NatEq (x :: N) (y :: N) :: Bool where   NatEq  Z     Z    = True   NatEq  Z    (S y) = False@@ -51,23 +65,52 @@   Iota Z     = Ø   Iota (S x) = x :< Iota x +iotaCong :: (x ~ y) :- (Iota x ~ Iota y)+iotaCong = Sub Wit+ type family Pred (x :: N) :: N where   Pred (S n) = n +predCong :: (x ~ y) :- (Pred x ~ Pred y)+predCong = Sub Wit+ type family (x :: N) + (y :: N) :: N where   Z   + y = y   S x + y = S (x + y) infixr 6 + +addCong :: (w ~ y,x ~ z) :- ((w + x) ~ (y + z))+addCong = Sub Wit+ type family (x :: N) * (y :: N) :: N where   Z   * y = Z   S x * y = (x * y) + y infixr 7 * +mulCong :: (w ~ y,x ~ z) :- ((w * x) ~ (y * z))+mulCong = Sub Wit+ type family (x :: N) ^ (y :: N) :: N where   x ^   Z = S Z   x ^ S y = (x ^ y) * x infixl 8 ^++expCong :: (w ~ y,x ~ z) :- ((w ^ x) ~ (y ^ z))+expCong = Sub Wit++type family Len (as :: [k]) :: N where+  Len  Ø        = Z+  Len (a :< as) = S (Len as)++lenCong :: (as ~ bs) :- (Len as ~ Len bs)+lenCong = Sub Wit++type family Ix (x :: N) (as :: [k]) :: k where+  Ix Z     (a :< as) = a+  Ix (S x) (a :< as) = Ix x as++ixCong :: (x ~ y,as ~ bs) :- (Ix x as ~ Ix y bs)+ixCong = Sub Wit  -- | Convenient aliases for low-value Peano numbers. type N0  = Z

@@ -0,0 +1,7 @@++module Type.Family.Symbol+  ( module GHC.TypeLits+  ) where++import GHC.TypeLits (Symbol,KnownSymbol,sameSymbol,symbolVal)+

@@ -30,20 +30,54 @@ module Type.Family.Tuple where  import Type.Family.Monoid+import Type.Class.Witness  type (#) = '(,) infixr 6 # +-- Fst,Snd,Thd et al {{{+ type family Fst (p :: (k,l)) :: k where   Fst '(a,b) = a +fstCong :: (p ~ q) :- (Fst p ~ Fst q)+fstCong = Sub Wit+ type family Snd (p :: (k,l)) :: l where   Snd '(a,b) = b +sndCong :: (p ~ q) :- (Snd p ~ Snd q)+sndCong = Sub Wit++type family Fst3 (p :: (k,l,m)) :: k where+  Fst3 '(a,b,c) = a++fst3Cong :: (p ~ q) :- (Fst3 p ~ Fst3 q)+fst3Cong = Sub Wit++type family Snd3 (p :: (k,l,m)) :: l where+  Snd3 '(a,b,c) = b++snd3Cong :: (p ~ q) :- (Snd3 p ~ Snd3 q)+snd3Cong = Sub Wit++type family Thd3 (p :: (k,l,m)) :: m where+  Thd3 '(a,b,c) = c++thd3Cong :: (p ~ q) :- (Thd3 p ~ Thd3 q)+thd3Cong = Sub Wit++-- }}}++-- Map et al {{{+ type family (f :: k -> l) <$> (a :: (m,k)) :: (m,l) where   f <$> (a#b) = a # f b infixr 4 <$> +pairMapCong :: (f ~ g,a ~ b) :- ((f <$> a) ~ (g <$> b))+pairMapCong = Sub Wit+ type family (f :: (m,k -> l)) <&> (a :: k) :: (m,l) where   (r#f) <&> a = r # f a infixr 4 <&>@@ -52,18 +86,11 @@   (r#f) <*> (s#a) = (r <> s) # f a infixr 4 <*> +-- }}}+ -- | A type-level pair is a Monoid over its pairwise components. type instance Mempty = Mempty # Mempty type instance (r#a) <> (s#b) = (r <> s) # (a <> b)--type family Fst3 (p :: (k,l,m)) :: k where-  Fst3 '(a,b,c) = a--type family Snd3 (p :: (k,l,m)) :: l where-  Snd3 '(a,b,c) = b--type family Thd3 (p :: (k,l,m)) :: m where-  Thd3 '(a,b,c) = c  type instance Mempty = '(Mempty,Mempty,Mempty) type instance '(a,b,c) <> '(d,e,f) = '(a<>d,b<>e,c<>f)

@@ -1,5 +1,5 @@ name: type-combinators-version: 0.1.2.1+version: 0.2.0.0 category: Data synopsis: A collection of data types for type-level programming cabal-version: >=1.10@@ -21,32 +21,30 @@         Data.Type.Disjunction         Data.Type.Fin         Data.Type.Index-        Data.Type.Index.Quote         Data.Type.Length         Data.Type.Nat-        Data.Type.Nat.Quote         Data.Type.Option         Data.Type.Product-        Data.Type.Product.Dual+        Data.Type.Product.Lifted         Data.Type.Sum-        Data.Type.Sum.Dual+        Data.Type.Sum.Lifted+        Data.Type.Sym         Data.Type.Quantifier         Data.Type.Vector-        Type.Class.HFunctor+        Type.Class.Higher         Type.Class.Known         Type.Class.Witness         Type.Family.Constraint+        Type.Family.Either         Type.Family.List         Type.Family.Maybe         Type.Family.Monoid         Type.Family.Nat+        Type.Family.Symbol         Type.Family.Tuple     build-depends:-        base >=4.8 && <4.9,-        containers,-        template-haskell,-        transformers,-        mtl+        base >=4.8 && <4.9     default-language: Haskell2010     hs-source-dirs: src+    ghc-options: -Wall -fno-warn-unticked-promoted-constructors