yoko 0.1 → 0.2

raw patch · 25 files changed

+392/−473 lines, 25 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES +9/−0
• Data/Yoko/Algebra.hs +0/−86
• Data/Yoko/Cata.hs +78/−0
• Data/Yoko/InDT.hs +23/−23
• Data/Yoko/Reduce.hs +38/−15
• Data/Yoko/Reflect.hs +22/−4
• Data/Yoko/ReflectBase.hs +16/−12
• Examples/Ex.hs +6/−0
• Examples/ExG.hs +60/−0
• Examples/InnerGeneric.hs +2/−2
• Examples/LL.hs +2/−2
• Examples/LLGeneric.hs +2/−2
• Examples/ReflectAux.hs +2/−1
• Examples/TermGeneric.hs +7/−8
• Examples/TermInner.hs +1/−1
• Examples/TermTest.hs +20/−9
• LICENSE +24/−1
• README +1/−249
• Type/Yoko/BTree.hs +36/−17
• Type/Yoko/Fun.hs +19/−19
• Type/Yoko/FunA.hs +4/−4
• Type/Yoko/Natural.hs +2/−2
• Type/Yoko/Sum.hs +2/−2
• Type/Yoko/Universe.hs +10/−10
• yoko.cabal +6/−4

@@ -0,0 +1,9 @@+0.1 -> 0.2+===============++* improved the treatment of automatically generating algebras+* emphasizing DCOf over DCU+* moved all of the documentation from README to http://code.google.com/p/yoko+* still obsessively tweaking names throughout the library+* improved the treatment of unique constructors+* added SiblingOf and a corresponding superclass constraint to DT

@@ -1,86 +0,0 @@-{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,-  UndecidableInstances #-}--{- |--Module      :  Data.Yoko.Algebra-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Algebras and catamorphisms for mutually-recursive datatypes.---}-module Data.Yoko.Algebra-  (Alg, Algebra(..), Algebras, SiblingAlgs, algebras, CataD(..), catas, cata,-  module Data.Yoko.Reduce) where-    -import Type.Yoko--import Data.Yoko.Generic-import Data.Yoko.Reflect-import Data.Yoko.Reduce----- | A @t@-algebra maps a sum of a @t@'s constructors into a mediation of @t@.-type Alg m t = AnRMNUni m (DCs t) -> Med m t-newtype Algebra m t = Alg (Alg m t)-type instance Unwrap (Algebra m) t = Alg m t-instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x--data ReduceD m t where-  ReduceD :: (Reduce m (DCs t), t ~ LeftmostRange (DCs t)) => ReduceD m t-instance (Reduce m (DCs t), t ~ LeftmostRange (DCs t)-         ) => t ::: ReduceD m where inhabits = ReduceD--type Algebras ts m = Each ts (Algebra m)-type SiblingAlgs t m = Algebras (Siblings t) m---- | Builds an 'Each' of algebras via 'Reduce'.-algebras :: forall ts m. (ts ::: All (ReduceD m)) => [qP|m|] -> Algebras ts m-algebras _ = each [qP|ReduceD m :: *->*|] $ \ReduceD -> reduce------- | @t@ inhabits @CataD ts m@ if------   1. @t@ is an instance of 'DT' and @ts ~ Siblings t@------   2. the recursive reduction can be mapped as a 'FromAt' function via---   'RMMap' across all constructors of @t@ and------   3. all of @t@'s siblings also inhabit the same universe.-data CataD ts m t where-  CataD :: (DT t, ts ~ Siblings t, t ::: Uni ts,-            DCs t ::: All-              (YieldsArrowTSSD-               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),-            ts ::: All (CataD ts m)-           ) => CataD ts m t-instance (DT t, ts ~ Siblings t, t ::: Uni ts,-          DCs t ::: All-            (YieldsArrowTSSD-             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),-          ts ::: All (CataD ts m)-         ) => t ::: CataD ts m where inhabits = CataD--catas :: forall m ts. (ts ::: All (CataD ts m)) =>-         Algebras ts m -> Each ts (FromAt m IdM)-catas fs = each [qP|CataD ts m :: *->*|] $ \d@CataD -> cataD d fs--cataD :: forall m t. CataD (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t-cataD CataD fs =-  prjEach (inhabitsFor [qP|t|]) fs .-  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $-             RMMap $ catas fs) . firstNP toUni . disband---- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med--- m t@.-cata :: (t ::: CataD (Siblings t) m) => SiblingAlgs t m -> t -> Med m t-cata = cataD inhabits

@@ -0,0 +1,78 @@+{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+  UndecidableInstances #-}++{- |++Module      :  Data.Yoko.Algebra+Copyright   :  (c) The University of Kansas 2011+License     :  BSD3++Maintainer  :  nicolas.frisby@gmail.com+Stability   :  experimental+Portability :  see LANGUAGE pragmas (... GHC)++Catamorphism for mutually-recursive datatypes.++-}+module Data.Yoko.Cata+  (Algebras, SiblingAlgs, algebras, CataU(..), catas, cata,+  module Data.Yoko.Reduce) where+    +import Type.Yoko++import Data.Yoko.Generic+import Data.Yoko.Reflect+import Data.Yoko.Reduce++++++type Algebras ts m = Each ts (Algebra m)+type SiblingAlgs t m = Algebras (Siblings t) m++-- | Builds an 'Each' of algebras via 'AlgebraDT'.+algebras :: forall ts m. (ts ::: All (AlgebraU m)) => [qP|m|] -> Algebras ts m+algebras _ = each [qP|AlgebraU m :: *->*|] $ \AlgebraU -> algebraDT+++++-- | @t@ inhabits @CataU ts m@ if+--+--   1. @t@ is an instance of 'DT' and @ts ~ Siblings t@+--+--   2. the recursive reduction can be mapped as a 'FromAt' function via+--   'RMMap' across all constructors of @t@ and+--+--   3. all of @t@'s siblings also inhabit the same universe.+data CataU ts m t where+  CataU :: (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),+            DCs t ::: All+              (YieldsArrowTSSU+               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),+            ts ::: All (CataU ts m)+           ) => CataU ts m t+instance (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),+          DCs t ::: All+            (YieldsArrowTSSU+             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),+          ts ::: All (CataU ts m)+         ) => t ::: CataU ts m where inhabits = CataU++catas :: forall m ts. (ts ::: All (CataU ts m)) =>+         Algebras ts m -> Each ts (FromAt m IdM)+catas fs = each [qP|CataU ts m :: *->*|] $ \d@CataU -> cataD d fs++cataD :: forall m t. CataU (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t+cataD CataU fs =+  appNT fs (inhabits :: Uni (Siblings t) t) .+  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $+             RMMap $ catas fs) . disband++-- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med+-- m t@.+cata :: (t ::: CataU (Siblings t) m) => SiblingAlgs t m -> t -> Med m t+cata = cataD inhabits

@@ -24,18 +24,18 @@   --- | A type @t@ inhabits @HasTagRepDCD tag c@ if @t@ is a 'DT' and there exists a @t@+-- | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@ -- constructor satisfying @'TagRepIs' tag c@.-data HasTagRepDCD tag c t where-  HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->-           HasTagRepDCD tag c t+data HasTagRepU tag c t where+  HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->+                HasTagRepU tag c t instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)-         ) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits+         ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits --- | Given @HasTagRepDCD tag c t@, a trivially-mediated @c@ value can be embedded into+-- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into -- @t@.-hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t-hasTagRepDCD (HasTagRepDCD d) = w d where+hasTagRepU :: HasTagRepU tag c t -> RMI c -> t+hasTagRepU (HasTagRepU d) = w d where   w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t   w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj   w (OnLeft u) = w u; w (OnRight u) = w u@@ -46,33 +46,33 @@  -- | Often times, we're interested in the universe of types accomodating a data -- constructor's image under some type-function.-type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))+type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc)) --- | A constructor type @dc@ inhabits @ImageHasTagRepDCD t fn@ if+-- | A constructor type @dc@ inhabits @ImageHasTagRepU t fn@ if -- -- 1. @fn@ can be mapped across the recursive occurrences in @dc@, and -- -- 2. @t@ has a constructor isomorphic to the @fn@-image of @dc@ -data ImageInDTD t fn dc where-  ImageInDTD :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)-                ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc-instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc-         ) => dc ::: ImageInDTD t fn where-  inhabits = ImageInDTD inhabits+data ImageInDTU t fn dc where+  ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)+                ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc+instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc+         ) => dc ::: ImageInDTU t fn where+  inhabits = ImageInDTU inhabits --- | Given @ImageInDTD t fn dc@, a trivially-mediated @dc@ value can be+-- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be -- embedded into @t@.-imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t-imageInDTD fn (ImageInDTD d) = hasTagRepDCD d . apply (CMap fn) . rep+imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t+imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep  -- | Same as @ImageInDTD@, but uses an implicitly applicative function. data ImageInDTDA t fn dc where   ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)-                 ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc-instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc+                 ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc+instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc          ) => dc ::: ImageInDTDA t fn where   inhabits = ImageInDTDA inhabits -imageInDTAD :: Functor (Idiom (fn IdM)) =>+imageInDTAU :: Functor (Idiom (fn IdM)) =>                (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t-imageInDTAD fn (ImageInDTDA d) = fmap (hasTagRepDCD d) . applyA (CMap fn) . rep+imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep

@@ -12,10 +12,12 @@ Stability   :  experimental Portability :  see LANGUAGE pragmas (... GHC) -Reduction of a band of constructors into a mediation of their range.+A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.  -}-module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where+module Data.Yoko.Reduce+  (Alg, Algebra(..), AlgebraU(..),+   algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where  import Type.Yoko @@ -24,25 +26,46 @@   -type AnRMNUni m ts = AnRMN m (Uni ts)  +-- | A @t@-algebra reduces a disbanded @t@ to the same mediation of @t@.+type Alg m t = Disbanded m t -> Med m t+newtype Algebra m t = Alg (Alg m t)+type instance Unwrap (Algebra m) t = Alg m t+instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x --- | @reduce@ embeds a mediated sum of constructors into a mediation of their--- range.-class (dcs ::: All IsDC) => Reduce m dcs where-  reduce :: AnRMNUni m dcs -> Med m (LeftmostRange dcs)+data AlgebraU m t where+  AlgebraU :: (DT t, AlgebraDT m t) => AlgebraU m t+instance (DT t, AlgebraDT m t+         ) => t ::: AlgebraU m where inhabits = AlgebraU +++++algebraFin :: (AlgebraUni m (Inhabitants u), Finite u) =>+             AnRMN m u -> Med m (LeftmostRange (Inhabitants u))+algebraFin = algebraUni . finiteNP++++-- | @algebraDT@ determines the algebra from the type and mediator.+class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t+++-- | @algebraUni@ determines the \"algebra\" from the type-sum and mediator.+class AlgebraUni m dcs where+  algebraUni :: AnRMN m (Uni dcs) -> Med m (LeftmostRange dcs)+ instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),-          Reduce m ts, Reduce m us) => Reduce m (ts :+ us) where-  reduce = reduce `two` reduce-instance ReduceDC m dc => Reduce m (N dc) where-  reduce = reduceDC . unRMNUni where-    unRMNUni :: AnRMNUni m (N dc) -> RMN m dc-    unRMNUni (NP (Uni (Here Refl)) x) = x+          AlgebraUni m ts, AlgebraUni m us) => AlgebraUni m (ts :+ us) where+  algebraUni = algebraUni `two` algebraUni+instance AlgebraDC m dc => AlgebraUni m (N dc) where+  algebraUni (NP (Uni (Here Refl)) x) = algebraDC x --- | @reduceDC@ embeds a mediated constructor into a mediation of its range.-class DC dc => ReduceDC m dc where reduceDC :: RMN m dc -> Med m (Range dc)+-- | @algebraDC@ determines the \"alegbra\" from the constructor type and+-- mediator.+class DC dc => AlgebraDC m dc where algebraDC :: RMN m dc -> Med m (Range dc)   

@@ -22,7 +22,7 @@ import Type.Yoko  import Data.Yoko.Generic-import Data.Yoko.ReflectBase+import Data.Yoko.ReflectBase hiding (DCU)   @@ -44,7 +44,25 @@   +type OnlyDC t = UnN (DCs t)+type family UnN a+type instance UnN (N dc) = dc +uniqueDC :: (DT t, N (OnlyDC t) ~ DCs t, t ~ Range (OnlyDC t)) => t -> RMNI (OnlyDC t)+uniqueDC = uniqueRMN . disband++uniqueRMN :: (Finite u, N (UnN (Inhabitants u)) ~ Inhabitants u+             ) => AnRMN m u -> RMN m (UnN (Inhabitants u))+uniqueRMN x = case finiteNP x of NP (Uni (Here Refl)) x -> x++uniqueRMN' :: (Finite (DCOf (Range dc)), N dc ~ DCs (Range dc)+              ) => AnRMN m (DCOf (Range dc)) -> RMN m dc+uniqueRMN' = uniqueRMN+++++ data IsDC dc where IsDC :: DC dc => IsDC dc type instance Pred IsDC t = True instance DC dc => dc ::: IsDC where inhabits = IsDC@@ -57,13 +75,13 @@   -- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.-dcDispatch :: DT t => NT (DCU t) (RMNTo IdM b) -> t -> b+dcDispatch :: DT t => NT (DCOf t) (RMNTo IdM b) -> t -> b dcDispatch = (. disband) . dcDispatch'  -- | Just a specialization: @dcDispatch' nt ('NP' ('DCOf' tag) fds) = 'appNT' -- nt tag fds@.-dcDispatch' :: DT t => NT (DCU t) (RMNTo IdM b) -> Disbanded IdM t -> b-dcDispatch' nt (NP (DCOf tag) fds) = appNT nt tag fds+dcDispatch' :: DT t => NT (DCOf t) (RMNTo IdM b) -> Disbanded IdM t -> b+dcDispatch' nt (NP tag fds) = appNT nt tag fds   

@@ -40,12 +40,12 @@    -- | The evidence that this constructor inhabits the datatype constructor   -- universe of its range.-  tag :: DCU (Range dc) dc; tag = inhabits+  tag :: DCOf (Range dc) dc; tag = inhabits    -- | Project this constructor from its range.   to :: Range dc -> Maybe (RMNI dc)-  to (disband -> NP tg fds) = case tg of-    DCOf (eqT (tag :: DCU (Range dc) dc) -> Just Refl) -> Just fds+  to (disband -> NP tg fds) = case eqT tg (tag :: DCOf (Range dc) dc) of+    Just Refl -> Just fds     _ -> Nothing    -- | Embed this constructor in its range.@@ -57,11 +57,14 @@ type instance Inhabitants (DCOf t) = Inhabitants (DCU t) instance Finite (DCU t) => Finite (DCOf t) where toUni (DCOf x) = toUni x type instance Pred (DCOf t) dc = Elem dc (DCs t)---- | @UniqueDC@ is for newtypes and GADT constructors where the type @dc@--- determines the constructor.-class UniqueDC dc where uniqueTo :: Range dc -> RMNI dc+instance EqT (DCU t) => EqT (DCOf t) where eqT (DCOf x) (DCOf y) = eqT x y +data SiblingOf t s where SiblingOf :: (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s+instance (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => s ::: SiblingOf t where inhabits = SiblingOf inhabits+type instance Inhabitants (SiblingOf t) = Siblings t+instance Finite (SiblingOf t) where toUni (SiblingOf x) = x+type instance Pred (SiblingOf t) s = Elem s (Siblings t)+instance EqT (SiblingOf t) where eqT (SiblingOf x) (SiblingOf y) = eqT x y   @@ -69,7 +72,7 @@ type Disbanded m t = AnRMN m (DCOf t)  disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)-disbanded fds = NP (DCOf tag) fds+disbanded fds = NP tag fds  band :: Disbanded IdM t -> t band (NP (DCOf _) fds) = fr fds@@ -81,12 +84,12 @@ type instance LeftmostRange (N dc) = Range dc type instance LeftmostRange (c :+ d) = LeftmostRange c -type DCs t = Inhabitants (DCU t)+type DCs t = Inhabitants (DCOf t)  -- | The "DataType" class. class (Finite (DCU t), EqT (DCU t),-       DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistD),-       Siblings t ::: TSum -- need GHC 7.2: , t ~ LeftmostRange (DCs t)+       DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistU),+       Siblings t ::: All (SiblingOf t)       ) => DT t where   -- | The string name of this datatype's original package.   packageName :: [qP|t|] -> String@@ -99,7 +102,8 @@   -- of @Recurs . DCs@, by definition.)   type Siblings t  -  -- | The data constructor universe.+  -- | The data constructor universe. 'DCOf' is to be preferred as much as+  -- possible.   data DCU t :: * -> * -- universe of constructor types    -- | /Disband/ this type into one of its data constructors.

@@ -0,0 +1,6 @@+module Examples.Ex where++data Tree1 a = Leaf a | Branch (Tree1 a) (Tree1 a)++data Even a = Zero | Even a (Odd a)+data Odd  a = Odd a (Even a)

@@ -0,0 +1,60 @@+{-# LANGUAGE EmptyDataDecls, TypeFamilies, TemplateHaskell, FlexibleInstances, TypeOperators, MultiParamTypeClasses, GADTs, UndecidableInstances #-}++{-# OPTIONS_GHC -fcontext-stack=50 #-}++module Examples.ExG where++import qualified Examples.Ex as Ex+import Examples.ReflectAux++++data Leaf a; data Branch a++data Zero a; data Even a; data Odd a++concat `fmap` mapM derive+  [''Ex.Tree1, ''Leaf, ''Branch,+   ''Ex.Even, ''Zero, ''Even,+   ''Ex.Odd, ''Odd]++type instance Tag (Leaf a) = $(return $ encode "Leaf")+newtype instance RM m (N (Leaf a)) = Leaf a+instance (True ~ IsEQ (Compare a a)) => DC (Leaf a) where+  occName _ = "Leaf"+  type Range (Leaf a) = Ex.Tree1 a+  fr ~(Leaf a) = Ex.Leaf a+type instance Rep (Leaf a) = D a+instance Generic (Leaf a) where+  rep ~(Leaf a) = D a+  obj ~(D a) = Leaf a++type instance Tag (Branch a) = $(return $ encode "Branch")+data instance RM m (N (Branch a)) =+  Branch (Med m (Ex.Tree1 a)) (Med m (Ex.Tree1 a))+instance (True ~ IsEQ (Compare a a)) => DC (Branch a) where+  occName _ = "Branch"+  type Range (Branch a) = Ex.Tree1 a+  fr ~(Branch a b) = Ex.Branch a b+type instance Rep (Branch a) = R (Ex.Tree1 a) :* R (Ex.Tree1 a)+instance Generic (Branch a) where+  rep ~(Branch a b) = FF (R a, R b)+  obj ~(FF (R a, R b)) = Branch a b++type instance Inhabitants (DCU (Ex.Tree1 a)) = N (Leaf a) :+ N (Branch a)+instance (True ~ IsEQ (Compare a a)) => DT (Ex.Tree1 a) where+  packageName _ = "yoko-0.1"+  moduleName _ = "Examples.ExG"+  type Siblings (Ex.Tree1 a) = N (Ex.Tree1 a)+  data DCU (Ex.Tree1 a) dc where+    Leaf_ :: DCU (Ex.Tree1 a) (Leaf a)+    Branch_ :: DCU (Ex.Tree1 a) (Branch a)+  disband (Ex.Leaf a) = disbanded $ Leaf a+  disband (Ex.Branch a b) = disbanded $ Branch a b+instance Finite (DCU (Ex.Tree1 a)) where+  toUni x = Uni $ case x of+    Leaf_ -> OnLeft $ Here Refl+    Branch_ -> OnRight $ Here Refl+instance (a ~ b) => (Leaf b) ::: DCU (Ex.Tree1 a) where inhabits = Leaf_+instance (a ~ b) => (Branch b) ::: DCU (Ex.Tree1 a) where inhabits = Branch_+instance EqT (DCU (Ex.Tree1 a)) where eqT = eqTFin

@@ -65,12 +65,12 @@ instance Finite (DCU Inner) where   toUni Lam_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits instance Etinif (DCU Inner) where-  fromUni (Uni x) = case x of+  frUni (Uni x) = case x of     (OnLeft  (OnLeft  (Here Refl))) -> Lam_     (OnLeft  (OnRight (Here Refl))) -> Var_     (OnRight (Here Refl))  -> App_ instance (t ::: Uni (DCs Inner)) => t ::: DCU Inner where-  inhabits = fromUni inhabits+  inhabits = frUni inhabits instance EqT (DCU Inner) where eqT = eqTFin  

@@ -44,8 +44,8 @@  instance (IdM ~ m) => Inner ::: DomainA (LL m) where   inhabits = AppABy $ \_ -> dcDispatch $-    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAD LL---  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAD LL+    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAU LL+--  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAU LL   

@@ -64,12 +64,12 @@ instance Finite (DCU Term) where   toUni DVar_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits instance Etinif (DCU Term) where-  fromUni (Uni x) = case x of+  frUni (Uni x) = case x of     (OnLeft  (OnLeft  (Here Refl))) -> DVar_     (OnLeft  (OnRight (Here Refl))) -> Var_     (OnRight (Here Refl))  -> App_ instance (t ::: Uni (DCs Term)) => t ::: DCU Term where-  inhabits = fromUni inhabits+  inhabits = frUni inhabits instance EqT (DCU Term) where eqT = eqTFin  

@@ -11,8 +11,9 @@ Just bundles up some imports for the various @*Generic@ modules.  -}-module Examples.ReflectAux (encode, module Data.Yoko) where+module Examples.ReflectAux (encode, module Data.Yoko, DCU) where  import Type.Serialize  import Data.Yoko hiding (qK)+import Data.Yoko.ReflectBase (DCU)

@@ -69,12 +69,12 @@ instance Finite (DCU B.Type) where   toUni TBool_ = inhabits; toUni TInt_ = inhabits; toUni TArrow_ = inhabits instance Etinif (DCU B.Type) where-  fromUni (Uni x) = case x of+  frUni (Uni x) = case x of     (OnLeft          (Here Refl)) -> TBool_     (OnRight (OnLeft  (Here Refl))) -> TInt_     (OnRight (OnRight (Here Refl))) -> TArrow_ instance (t ::: Uni (DCs B.Type)) => t ::: DCU B.Type where-  inhabits = fromUni inhabits+  inhabits = frUni inhabits instance EqT (DCU B.Type) where eqT = eqTFin  type instance Tag Lam = $(return $ encode "Lam")@@ -121,13 +121,13 @@   toUni Lam_ = inhabits; toUni Var_ = inhabits   toUni App_ = inhabits; toUni Let_ = inhabits instance Etinif (DCU B.Term) where-  fromUni (Uni x) = case x of+  frUni (Uni x) = case x of     (OnLeft  (OnLeft (Here Refl))) -> Lam_     (OnLeft  (OnRight (Here Refl))) -> Var_     (OnRight (OnLeft (Here Refl))) -> App_     (OnRight (OnRight (Here Refl))) -> Let_ instance (t ::: Uni (DCs B.Term)) => t ::: DCU B.Term where-  inhabits = fromUni inhabits+  inhabits = frUni inhabits instance EqT (DCU B.Term) where eqT = eqTFin  type instance Tag Decl = $(return $ encode "Decl")@@ -135,9 +135,8 @@ instance DC Decl where   occName _ = "Decl"   type Range Decl = B.Decl-  to = Just . uniqueTo; fr ~(Decl ds tm) = B.Decl ds tm+  to = Just . uniqueDC; fr ~(Decl ds tm) = B.Decl ds tm data instance RM m (N Decl) = Decl B.Type (Med m B.Term)-instance UniqueDC Decl where uniqueTo ~(B.Decl ds tm) = Decl ds tm instance DT B.Decl where   packageName _ = "datatype-reflect"   moduleName _ = "DeclBase"@@ -148,9 +147,9 @@ instance Finite (DCU B.Decl) where   toUni Decl_ = inhabits instance Etinif (DCU B.Decl) where-  fromUni (Uni (Here Refl)) = Decl_+  frUni (Uni (Here Refl)) = Decl_ instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where-  inhabits = fromUni inhabits+  inhabits = frUni inhabits instance EqT (DCU B.Decl) where eqT = eqTFin  

@@ -46,7 +46,7 @@  instance (IdM ~ m) => Term ::: Domain (Elab m) where   inhabits = AppBy $ \_ -> dcDispatch $-    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTD Elab+    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTU Elab  elab_Let (G.Let ds tm) =   foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds

@@ -14,7 +14,7 @@ Portability :  see LANGUAGE pragmas (... GHC)  A denotational semantics for the simple-typed lambda calculus via-"Data.Yoko.Algebra".+"Data.Yoko.Cata".  -} module Examples.TermTest where@@ -23,7 +23,8 @@ import qualified Examples.TermGeneric as G  import Type.Yoko-import Data.Yoko.Algebra+import Data.Yoko.Cata+import Data.Yoko   -- | Since our family of abstract data types don't correspond to the@@ -52,17 +53,27 @@ type instance Med SemM Term = Sem type instance Med SemM Decl = (Type, Sem) -instance ReduceDC SemM G.Lam where reduceDC = eLam-instance ReduceDC SemM G.Var where reduceDC = eVar-instance ReduceDC SemM G.App where reduceDC = eApp-instance ReduceDC SemM G.Let where reduceDC = eLet+instance AlgebraDT SemM Term where algebraDT = algebraFin+instance AlgebraDC SemM G.Lam where algebraDC = eLam+instance AlgebraDC SemM G.Var where algebraDC = eVar+instance AlgebraDC SemM G.App where algebraDC = eApp+instance AlgebraDC SemM G.Let where algebraDC = eLet -instance ReduceDC SemM G.Decl where reduceDC = eDecl+instance AlgebraDT SemM Decl where algebraDT = eDecl . uniqueRMN +-- | 'eval' will work for any family of mutually recursive types that all have+-- @'AlgebraDT' SemM@ instances. eval x = ($ x) $ cata $ algebras [qP|SemM|] --- NB equivalent-eval' x = ($ x) $ cata $ (reduce .|. reduce) -- :: AlgebraFam Term SemM)+eval'     x = ($ x) $ cata $ (algebraDT  .|. algebraDT :: SiblingAlgs Term SemM)+eval''    x = ($ x) $ cata $ (algebraDT  .|. algebraDT)+eval'''   x = ($ x) $ cata $ (algebraFin .|. algebraDT :: SiblingAlgs Term SemM)+eval''''  x = ($ x) $ cata $ (algebraFin .|. algebraDT)+eval''''' x = ($ x) $ cata $ (algebraDT  .|. (eDecl . uniqueRMN'))++--instance AlgebraDT SemM Decl where algebraDT = algebraFin+--instance AlgebraDC SemM G.Decl where algebraDC = eDecl+--eval''''' x = ($ x) $ cata $ (algebraFin .|. algebraFin :: SiblingAlgs Term SemM)   

@@ -1,1 +1,24 @@-BSD3+Copyright (c) 2011, University of Kansas+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++  * Redistributions of source code must retain the above copyright notice, this+    list of conditions and the following disclaimer.++  * Redistributions in binary form must reproduce the above copyright notice,+    this list of conditions and the following disclaimer in the documentation+    and/or other materials provided with the distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+

@@ -1,249 +1,1 @@-drex (read "dee-recks")--While the "d" is just for "datatype", "rex" is bit of a double entendre.--The representation classes (DT, Generic, Gist) each disinvest their parameter-of its nominality, similar to how a king disinvests nobles of their titles.--Each class also dismantles, or "wrecks", its parameter: DT takes a single type-to a sum of its constructors, Generic maps a constructor to its underlying-shape, and Gist forgets the shape and mediation.--... Also, it sounds like "T-rex".--===================--See http://j.mp/tNLx40 for a Google spreadsheet cataloging the various d-rex-concepts and components.--====================--#1 Basic Universes--The @:::@ class in the @Universe@ module is pervasive in d-rex. The constraint-@t ::: u@ is read "t inhabits u" (or "t satisfies u", if you must). @u@ is a-/universe/, a type that represents a possibly finite, possibly paradoxical-collection of types. Universes can be /open/ or /closed/. @Lit@, for example,-is closed.--  in module Ex-    data Lit t where IntLit :: Lit Int; CharLit :: Lit Char--@ShowD@ is open, since new instances of @Show@ can be declared anywhere.--  in module Ex-    data ShowD t where ShowD :: Show t => ShowD t--(The "D" suffix is for "dictionary", since this GADT operationally reifies the-@Show@ dictionary. @(\ShowD x -> show x) :: ShowD t -> t -> String@ -- note-that there's no @Show t@ constraint in that type.--Some closed universes are also finite. There exists an isomorphism between such-a universes and a finite set of types (#4 below).--#2 Constructor Universes--d-rex's principle novelty is its support of the finite closed universe of a-datatype's constructors, codifed as the indexed data family @DCU@. The @open@-method of the @DT@ type class converts from a type to its universe of-constructors. @close@ goes back the other way.--As d-rex breaks a datatype into its universe of constructors, it also generates-a new void type per constructor. For example, d-rex breaks @Either a b@ into--  in module G-    data Left a b; data Right a b--With these types, d-rex declares the constructor universe of @Either a b@.--  in module G-    data instance DCU (Either a b) where-      Left_  :: DCU (Either a b) (Left  a b)-      Right_ :: DCU (Either a b) (Right a b)--Note that each constructor type inherits the original type's parameters. d-rex-also declares an instance of the data family @RM@ for each constructor -- the-resulting types are called /fields types/.--  in module G-    newtype instance RM (N (Left  a b)) m = Left a-    newtype instance RM (N (Right a b)) m = Right b--  in module ReflectBaseR-    type Fields dc = RM (N dc)--(Clearly, d-rex re-uses the constructor names. Hence, the generic declarations-must always generated in a separate module to enable namespace management.)--The data family @RM@, the @m@ parameter, type family @App@, and @N@ are-explained in the next section. In the interim, we'll make do with a couple-brief declarations.--  in module Type-    data IdT; type instance App IdT a = a--There now exists an isomorphism between @Either a b@ and-@forall dc. (DCU (Either a b) dc, Fields dc IdT).--  Left x    =~= (Left_, G.Left x)-  Right x   =~= (Right_, G.Right x)--The @DCU@ tag is a crucial part of this pair -- without it, G.Left and G.Right-would have inequal types!--#3 Recursion-mediated types--The data family @RM@ stands for "recursion-mediated". The idea is that the @m@-parameter is applied to all recursive type occurences in a constructor's-fields.--  in module T-    data Even a = Zero | Even a (Odd a)-    data Odd  a = Odd a (Even a) --  in module G-    data Zero a; data Even a; data Odd a-    data instance RM (N (Zero   a)) m-    data instance RM (N (G.Even a)) m = Even a (App m (T.Odd  a))-    data instance RM (N (G.Odd  a)) m = Odd  a (App m (T.Even a))--  in module Type-    data True = True; data False = False--  in module Ex-    data ParityM-    type instance App ParityM (T.Even a) = False-    type instance App ParityM (T.Odd  a) = True--    ex0 = Even 'e' True :: Fields (G.Even Char) ParityM-    ex1 = Odd 'o' False :: Fields (G.Odd  Char) ParityM--The recursion-mediated representation of the fields types enables their-re-use. For example, the same fields type can be used to define a bottom-up-reducer, where the recursive occurrences have been replaced with the result of-the catamorphism.--  in module Ex-    data LengthM-    type instance App LengthM (T.Even a) = Int-    type instance App LengthM (T.Odd  a) = Int--    type Reducer m dc = Fields dc m -> App m dc--    ex2 :: Reducer Len (G.Even a)-    ex2 (G.Even _ i) = 1 + i --Since @App@ is a type family, it's not necessarily injective. @LengthM@-demonstrates where injectivity would not be desirable. Indeed, d-rex relies on-this as discussed in #6 below. Unfortunately, non-injectivity can muddle type-inference. For example, the inferred type of @G.Even 'c' 3@ involves a type-variable: @(Num i, App m (T.Even Char) ~ i) => Fields (G.Even Char) m@. We-provide the function @mediated@ for directly specifying the mediator.--  in module Util-    mediated :: [qP|m|] -> RM c m -> RM c m-    mediated = const id--  in module Ex-    -- inferred ex3 :: Fields (G.Even Char) LengthM-    ex3 = mediated [qP|LengthM|] $ G.Even 'c' 3--(@qP@ is just a quasiquoter for proxies -- useful for passing types as values.)--The data family @RM@ is indexed by the core representational types. Most of-these are common to many representation-based generic programming-libraries. They indeed compromise a closed universe @Core@; that particular-universe per se is not codified in d-rex, but its closedness is the crux of all-representational generic programming.--  in module Core-    type family Rep a-    data V                            -- void-    data U = U                        -- unit-    newtype D a = D a                 -- a dependency-    newtype R t = R t                 -- a recursive occurrence-    newtype F f c = F (f c)           -- argument to a *->*-    newtype FF ff c d = FF (ff c d)   -- arguments to a *->*->*-    newtype M i c = M c               -- meta information--    newtype N t = N t                 -- a named type (user hook)--    type (:+) = FF Either-    type (:*) = FF (,)-    type (:->) = FF (->)--The structure of many constructors' fields, like T.Even can be codified in-terms of these basic types.--  in module G-    type Rep (G.Even a) = FF (,) (D a) (R a)--The recursion-mediated types are indexed by these core types. Note that the-following declarations are in a separate module, so the constructor names don't-actually clash.--  in module GenericR-    data family RM c m-    data instance RM V m-    data instance RM U m = U-    newtype instance RM (D a) m = D a-    newtype instance RM (R t) m = R (App m t)-    newtype instance RM (F f c) m = F (f (RM c m))-    newtype instance RM (FF ff c d) m = FF (ff (RM c m) (RM d m))-    newtype instance RM (M i c) m = M (RM c m)--These just follow the semantics of recusiion-mediated types.--The only core type without an @RM@ instance is @N@. @N@ is crucial to d-rex's-usability. It is the interface boundary between the d-rex kernel and the user-datatype. As demonstrated earlier in this section and in section #2, @RM (N -)@-instances are provided for each fields type. There is also a corresponding-instance of @Rep@ and @Generic@.--  in module GenericR-    class Generic a where-      rep :: RM (N a) m -> RM (Rep a) m-      obj :: RM (Rep a) m -> RM (N a) m--  in module G-    instance Generic (G.Even a) where-      rep ~(G.Even a o) = FF (D a, R o)-      obj ~(FF (D a, R o))) = G.Even a o--INVARIANT: the RHS of a Rep should never include an @N@. @N@ is just in place-to delay the representation of a type.--#4 Sets of types--d-rex also uses a universe of types constructed via V, :+, and N to represent-finite sets (implemented as type-level binary trees) of types. The @Finite@-type class recognizes the isomorphism between a finite closed universes and a-set of types.--  in module TypeBTree-    type family Inhabitants u-    class Finite u where-      path :: u t -> Small (Inhabitants u) t-      tag  :: Small (Inhabitants u) t -> u t--  in module Ex-    type instance Inhabitants (DCU Lit) = N Int :+ N Char--    type instance Inhabitants (DCU (Either a b)) =-      N (G.Left a b) :+ N (G.Right a b)--    type instance Inhabitants (DCU (T.Even a)) =-      N (G.Zero a) :+ N (G.Even a)--@Inhabitants@/@Finite@ recognizes @V@, @:+@, and @N@ as the closed-representational core of finite closed universes in the same way that-@Rep@/@Generic@ encode isomorphisms between the full ensemble of core types and-the large set of Haskell types they can represent.--#5 Other Universes--Exists, Small, All, MFun, MMap ...--#6 Tag-Gist equivalence and Conversions--...+See the documentation at http://code.google.com/p/yoko

@@ -40,7 +40,7 @@  type instance Pred (Uni ts) t = Elem t ts -instance (ts ::: TSum) => EqT (Uni ts) where+instance EqT (Uni ts) where   eqT (Uni u) (Uni v) = w u v where     w :: forall ts a b. Inu a ts -> Inu b ts -> Maybe (a :=: b)     w (Here Refl) (Here Refl) = Just Refl@@ -64,24 +64,27 @@ primUni (Uni u) = w u where   w :: Inu t ts -> PrimUni ts t   w (Here Refl) = Refl-  w (OnLeft u) = LeftD $ w u-  w (OnRight v) = RightD $ w v+  w (OnLeft u) = LeftU $ w u+  w (OnRight v) = RightU $ w v  primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t-primUni1 (Uni (OnLeft u)) = LeftD $ Uni u-primUni1 (Uni (OnRight v)) = RightD $ Uni v+primUni1 (Uni (OnLeft u)) = LeftU $ Uni u+primUni1 (Uni (OnRight v)) = RightU $ Uni v     -- | Finite universes can be represented as type-sums. type family Inhabitants u-class (Inhabitants u ::: TSum) => Finite u where+class Finite u where   toUni :: u t -> Uni (Inhabitants u) t --- | @fromUni@ sometimes requires a stronger context than does @toUni@, so we+finiteNP :: Finite u => NP u f -> NP (Uni (Inhabitants u)) f+finiteNP = firstNP toUni++-- | @frUni@ sometimes requires a stronger context than does @toUni@, so we -- separate the two methods.-class Finite u => Etinif u where fromUni :: Uni (Inhabitants u) t -> u t+class Finite u => Etinif u where frUni :: Uni (Inhabitants u) t -> u t  -- | Any finite universe can be used to determine type equality. eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v@@ -89,11 +92,27 @@ eqTFin x y = eqT (toUni x) (toUni y)  type instance Inhabitants (Uni ts) = ts-instance (ts ::: TSum) => Finite (Uni ts) where toUni = id-instance Finite (Uni ts) => Etinif (Uni ts) where fromUni = id+instance Finite (Uni ts) where toUni = id+instance Finite (Uni ts) => Etinif (Uni ts) where frUni = id +type instance Inhabitants VoidU = V +type instance Inhabitants ((:=:) t) = N t+instance Finite ((:=:) t) where toUni Refl = Uni (Here Refl)+instance Etinif ((:=:) t) where frUni (Uni (Here Refl)) = Refl +type instance Inhabitants (u :|| v) = Inhabitants u :+ Inhabitants v+instance (Finite u, Finite v) => Finite (u :|| v) where+  toUni (LeftU u) = case toUni u of+    Uni x -> Uni $ OnLeft $ x+  toUni (RightU v) = case toUni v of+    Uni x -> Uni $ OnRight $ x+instance (Etinif u, Etinif v) => Etinif (u :|| v) where+  frUni uv = case primUni1 uv of+    LeftU u -> LeftU $ frUni u+    RightU v -> RightU $ frUni v++ -- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a -- type-sum. type family Norm c@@ -139,21 +158,21 @@   -- | @each@ is the principal means of defining an @Each@ value.-each :: forall u ts f. (ts ::: All u) => [qP|u :: *->*|] ->-        (forall a. u a -> Unwrap f a) -> Each ts f-each _ = \fs -> w inhabits fs where+each :: forall u v f. (Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->+        (forall a. u a -> Unwrap f a) -> NT v f+each _ = \fs -> firstNT toUni $ w inhabits fs where   w :: forall ts. All u ts ->        (forall a. (a ::: u) => u a -> Unwrap f a) -> Each ts f   w SumV _ = none "TypeBTree.each"   w (SumN u) fns = one $ fns u   w (SumS c d) fns = w c fns `both` w d fns   -eachF :: forall u ts f. (Wrapper f, ts ::: All u) => [qP|u :: *->*|] ->-         (forall a. u a -> f a) -> Each ts f+eachF :: forall u v f. (Wrapper f, Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->+         (forall a. u a -> f a) -> NT v f eachF p f = each p (unwrap . f) -eachF_ :: forall f ts. (Wrapper f, ts ::: All NoneD) => (forall a. f a) -> Each ts f-eachF_ f = eachF Proxy ((\NoneD -> f) :: forall a. NoneD a -> f a)+eachF_ :: forall f v. (Wrapper f, Inhabitants v ::: All NoneU, Finite v) => (forall a. f a) -> NT v f+eachF_ f = eachF Proxy ((\NoneU -> f) :: forall a. NoneU a -> f a)   

@@ -19,8 +19,8 @@ -}  module Type.Yoko.Fun-  (Domain(..), Dom, Rng, applyD, apply,-   YieldsArrowTSSD, DomF, RngF, eachArrow,+  (Domain(..), Dom, Rng, applyU, apply,+   YieldsArrowTSSU, DomF, RngF, eachArrow,    AsComp(..), WrapComp, WrapCompF   ) where @@ -45,42 +45,42 @@ type family Rng (fn :: * -> *) t  -- | @applyD@ is analogous to '$'.-applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t-applyD (AppBy f) = f+applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t+applyU (AppBy f) = f --- | @apply = applyD inhabits@.+-- | @apply = applyU inhabits@. apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t-apply = applyD inhabits+apply = applyU inhabits   --- | @YieldsArrowTSSD fn@ also gaurantees that @fn@ at @t@ yields a type of the+-- | @YieldsArrowTSSU fn@ also gaurantees that @fn@ at @t@ yields a type of the -- shape @(DomF fn) t -> (RngF fn) t@; i.e. it guarantees that @Dom fn t@ and -- @Rng fn t@ both don't depend on @t@ and also are an application of a @* -> -- *@ to @t@.-data YieldsArrowTSSD fn t where-  YieldsArrowTSSD ::+data YieldsArrowTSSU fn t where+  YieldsArrowTSSU ::     (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t-    ) => Domain fn t -> YieldsArrowTSSD fn t+    ) => Domain fn t -> YieldsArrowTSSU fn t instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t-         ) => t ::: YieldsArrowTSSD fn where inhabits = YieldsArrowTSSD inhabits+         ) => t ::: YieldsArrowTSSU fn where inhabits = YieldsArrowTSSU inhabits --- | Used by @YieldsArrowTSSD fn@ to structure the domain of @fn@.+-- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@. type family DomF (fn :: * -> *) :: * -> *--- | Used by @YieldsArrowTSSD fn@ to structure the range of @fn@.+-- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@. type family RngF (fn :: * -> *) :: * -> * --- | Just a specialization: @yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD fn@.-yieldsArrowTSSD :: YieldsArrowTSSD fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t-yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD fn+-- | Just a specialization: @yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn@.+yieldsArrowTSSU :: YieldsArrowTSSU fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t+yieldsArrowTSSU (YieldsArrowTSSU domU) fn = applyU domU fn  -- | Defines an @'NT' u@ from a suitably polymorphic type-function @fn@ if @u@ -- is finite and the function yields an arrow at each type in @u@. eachArrow :: forall fn u.-  (Finite u, Inhabitants u ::: All (YieldsArrowTSSD fn)+  (Finite u, Inhabitants u ::: All (YieldsArrowTSSU fn)   ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))-eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $-  \d -> yieldsArrowTSSD d fn+eachArrow fn = each [qP|YieldsArrowTSSU fn :: *->*|] $+  \d -> yieldsArrowTSSU d fn   

@@ -17,7 +17,7 @@ -}  module Type.Yoko.FunA-  (Idiom, DomainA(..), applyA, applyAD) where+  (Idiom, DomainA(..), applyA, applyAU) where  import Type.Yoko.Fun import Type.Yoko.Universe@@ -30,7 +30,7 @@ newtype DomainA fn t = AppABy (fn t -> Dom fn t -> Idiom fn (Rng fn t))  applyA :: (t ::: DomainA fn) => fn t -> Dom fn t -> Idiom fn (Rng fn t)-applyA = applyAD inhabits+applyA = applyAU inhabits -applyAD :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)-applyAD (AppABy f) = f+applyAU :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)+applyAU (AppABy f) = f

@@ -43,8 +43,8 @@ -- short-circuit, preferring inhabitation of @u@ over @v@. orNT :: NT u f -> NT v f -> NT (u :|| v) f orNT (NT f) (NT g) = NT $ \uv -> case uv of-  LeftD  u -> f u-  RightD v -> g v+  LeftU  u -> f u+  RightU v -> g v   constNT :: Unwrap f t -> NT ((:=:) t) f

@@ -46,8 +46,8 @@ instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where   inhabits = SumS inhabits inhabits --- | @All 'NoneD'@ is satisfied by any type-sum.-type TSum = All NoneD+-- | @All 'NoneU'@ is satisfied by any type-sum.+type TSum = All NoneU   

@@ -1,6 +1,6 @@ {-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,   FlexibleContexts, ScopedTypeVariables, FlexibleInstances,-  UndecidableInstances, GADTs, Rank2Types #-}+  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}  {- | @@ -44,13 +44,13 @@   -- | The universe of all types; it has /no/ contraints.-data NoneD a = NoneD-instance a ::: NoneD where inhabits = NoneD+data NoneU a = NoneU+instance a ::: NoneU where inhabits = NoneU  type Both = (:&&) infixr 3 :&& -- | Universe product.-data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstD :: u a, sndD :: v a} -> (u :&& v) a+data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstU :: u a, sndU :: v a} -> (u :&& v) a instance (a ::: u, a ::: v) => a ::: u :&& v where   inhabits = inhabits :&& inhabits @@ -58,21 +58,21 @@   -instance (a ~ b) => b ::: ((:=:) a) where inhabits = Refl+instance (a ~ b) => b ::: (:=:) a where inhabits = Refl   infixr 2 :|| -- | Universe sum. data (u :|| v) a where-  LeftD  :: u a -> (u :|| v) a-  RightD :: v a -> (u :|| v) a+  LeftU  :: u a -> (u :|| v) a+  RightU :: v a -> (u :|| v) a  instance (anno ~ Pred u a, a ::: u :|| v :? anno) => a ::: u :|| v where   inhabits = inhabits_ [qP|anno|] instance (True  ~ Pred u a, a ::: u) => a ::: u :|| v :? True where-  inhabits = Anno $ LeftD inhabits+  inhabits = Anno $ LeftU inhabits instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where-  inhabits = Anno $ RightD inhabits+  inhabits = Anno $ RightU inhabits   type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)@@ -80,7 +80,7 @@   -- | The empty universe.-data VoidU t = VoidU -- the empty universe+data VoidU t -- the empty universe   

@@ -1,5 +1,5 @@ name: yoko-version: 0.1+version: 0.2 synopsis: generic programming with disbanded constructors   description: @yoko@ views a nominal datatype as a /band/ of constructors, each@@ -29,7 +29,7 @@   constructor, say @John@, to be used independently of its original range type   and sibling constructors.   .-  As a generic programming library, @yoko@ extends @intant-generics@ with+  As a generic programming library, @yoko@ extends @instant-generics@ with   support for constructor-centric generic programming. The @Examples/LL.hs@   file distributed with the @yoko@ source demonstrates defining a   lambda-lifting conversion between the two types @Inner@, which has lambdas,@@ -54,6 +54,8 @@   .   Existing generic libraries don't use constructor names to the degree that   @yoko@ does, and so cannot accomodate generic /conversions/ nearly as well.+  .+  See the wiki at <http://code.google.com/p/yoko> for more documentation.  category: Generics, Reflection @@ -66,7 +68,7 @@ build-type: Simple cabal-version: >= 1.6 -extra-source-files: README, Examples/*.hs+extra-source-files: README, CHANGES, Examples/*.hs   @@ -98,7 +100,7 @@                    Data.Yoko.Reflect,                    Data.Yoko.InDT,                    Data.Yoko.Reduce,-                   Data.Yoko.Algebra+                   Data.Yoko.Cata  --                   Examples.TermBase, --                   Examples.TermGeneric,