_      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com      see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com Composition of * -> * types. The Pred> type family realizes type-level predicates (over types) that $ yield a type-level Boolean: either  or . Predicates are often  universes. The Wrapper9 class is used to make term-level programming newtypes a 4 little more lightweight from the user perspective. type instance Med IdM a = a. The Med: type family encodes the behavior of recursion mediators. ,Explicitly takes the inner type as a proxy. "   see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comThe empty universe. Universe sum. Universe product.  !"The universe of all types; it has no contraints. "#(:?) helps us write guarded (:::) instances (see   /http://hackage.haskell.org/trac/ghc/ticket/5590) $%A universe determines a set of types; open or closed. (:::) is  comparable to the Sat class (e.g. from SYB3). &' For use with (:::) instances that use (:?). ( Sometimes it's helpful to specify which t must be in the universe.  !"#$%&'(%&#$'(!"  !""#$$%&&'(see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com)ArrowTSS9 can be partially applied, and hence occur as the second  argument of NT , where as  f _ -> g _ cannot. *+Natural pairs. ,- Natural transformations. We use " to lighten the user interface at 9 the value level, though it clutters the types a little. ./0123 Defining an NT via type-level backtracking;  uses  to + short-circuit, preferring inhabitation of u over v. 45678 Analog to  Control.Arrow.first. 9)*+,-./0123456789/-.01234567+,8)*9)**+,,-../0123456789see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com:-a named intermediate (user hook); crucially: type instance Rep (N t) =  Rep t. ;<meta information =>arguments to a  * -> * -> * ?@argument to a * -> * ABa recursive occurrence CD a dependency EFunit GHvoid I!Structural representations (e.g. Data.Yoko.Generic's RM) of a * type E can be derived as a data family indexed by the core representation (Rep)  of that type. J:;<=>?@ABCDEFGHIJIHFGDEBC@A>?<=:;J:;;<==>??@AABCCDEEFGGHIJsee LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com :<>@BDFHIJ IHFDB@><:Jsee LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comK Elem t ts is  if t occurs in the type sum ts. LThe higher-order universe Exists. c inhabits Exists p if there  exists a type t in the type-sum c for which  ~  p t. NB  that cB is not necessarily a type-sum; i.e. there is no well-typed total  function from  Exists p c to TSum c. MNOPAll "! is satisfied by any type-sum. QThe higher-order universe All. c inhabits All u if c is a type-sum  and all types in it inhabit u. RSTUType-sum union. We re-use : as type-sum singleton and H as the empty  type-sum. KLMNOPQRSTU UQTSRPLONMK KLONMMNOPQTSRRSTUsee LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comV Each ts f provides a .- t f for each t in the type-sum ts. WNormWD combines two type-sums into a right-associated type-sum containing  no duplicates. XNorm uses NormW! to remove duplicates from (i.e.  normalize) a  type-sum. YfrUni1 sometimes requires a stronger context than does toUni, so we  separate the two methods. Z[\]2Finite universes can be represented as type-sums. ^A Uni ts t9 value can also be understood in terms of more primitive  universes, ,  and  for H, ;:, and U,  respectively. _Uni ts4 is a universe containing the types in the type-sum ts. `aInu t' is a universe of type-sums containing t. bcde<Any finite universe can be used to determine type equality. fghijklmnoeach' is the principal means of defining an Each value. pqrJust a specialization: prjEach x f = 1 f x. steachOrNT fs gs builds an .- that uses fs for as many types in the  universe v as possible, and uses gs for the rest. It's an extension of  3 to Each. VWXYZ[\]^_`abcdefghijklmnopqrsta_`^bc][\dYZeXWVfghijklmnopqrstVWXYZZ[\\]^_``abcdefghijklmnopqrstsee LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comuDefining instances:  8 type instance Dom (AsComp fn) t = WrapComp (Dom fn t) 8 type instance Rng (AsComp fn) t = WrapComp (Rng fn t)  inhabits = AppBy $ ('AsComp fn) -> wrap . apply fn . unwrap vwOnly instance: +type instance WrapCompF_ (f (g a)) = f :. g. xOnly instance: .type instance WrapComp_ (f (g a)) = (f :. g) a. yUsed by YieldsArrowTSSU fn to structure the range of fn. zUsed by YieldsArrowTSSU fn to structure the domain of fn. {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. |Rng fn t is the range of fn at type t; it's the term-level range of  fn at t. }Dom fn t is the domain of fn at type t; it's the term-level domain  of fn at t. ~ Domain fn# is the universe of types at which fn can be applied; it's  the type-level domain of fn. applyD is analogous to . apply = applyU inhabits. Just a specialization: :yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn.  Defines an .- u+ from a suitably polymorphic type-function fn if u < is finite and the function yields an arrow at each type in u. uvwxyz{|}~~}|{zyuvxwuvvwxyz{|}~ see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com Generic& represents a recursion-mediated type N a as a  recursion-mediated Rep a. The opposite of "representation" is (the  represented) "object". In yoko, the :7 core type is used for a lightweight representation of ; constructor types -- each will define its own instance of RM (N _). RM stands is for "recursively mediated", and m is the " mediator (of recursive occurrences)".   data instance RM m V  data instance RM m U = U $ newtype instance RM m (D a) = D a , newtype instance RM m (R t) = R (Med m t) 1 newtype instance RM m (F f c) = F (f (RM m c)) @ newtype instance RM m (FF ff c d) = FF (ff (RM m c) (RM m d)) - newtype instance RM m (M i c) = M (RM m c) :<>@BDFHIJ  see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comA FromAtA function is applicable only at the specified mediator and type;  crucially #type instance MApp (FromAt m) n = m. 6mediator-functions can also modify the mediator; e.g.   type instance } (RMMap u fn m) c = RM m c  type instance |% (RMMap u fn m) c = RM (MApp fn m) c +mediator-functions can be mapped across an  type/value.  see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com CApp fn c applies the type-function fn to all recursive occurrences  (i.e. B ) in the Data.Yoko.Core type c.  CMap fn m c applies fn$ to all recursive occurrences (i.e. B) in a  Data.Yoko.Core type c that's mediated by m. The domain (}) is RM  m c and the range (|) is RM m (CApp (fn m) c). The  is Idiom  (fn m). The TApp5 type family encodes the type-level functionality of   Type.Yoko.Fun functions.  see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com  !"#$%&'()*+,-./0123456789KLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comThe DataType class. $A type-sum of the types in this type's binding group, including  itself.  Siblings t% ought to be the same for every type t in the J binding group. (It also ought to be equivalent to the transitive closure  of  Recurs . DCs, by definition.) The data constructor universe.  is to be preferred as much as  possible.  The string name of this datatype's original package.  The string name of this datatype's original module. Disband. this type into one of its data constructors. Evidence that t& is the range of the constructor type dc. The "Datatype Constructor" class. The range of this constructor. %The string name of this constructor. EThe evidence that this constructor inhabits the datatype constructor  universe of its range. )Project this constructor from its range. %Embed this constructor in its range. The Recurs# of a constructor type is the type- Type.Yoko.Sum of types % that occur in this constructor. NB:  Recurs t  isSubsumedBy Siblings (Range  dc). The Tag9 of a constructor type is a type-level reflection of its  constructor name. see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com$A fundamental notion of identity in yoko, the TagRepIs tag c universe contains all constructor types dc where (Tag dc ~ tag, c ~ Rep dc).  + type instance Pred (TagRepIs tag c) dc = B And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c)) Just a specialization: %dcDispatch = (. disband) . dcDispatch'. Just a specialization:  dcDispatch' nt (,+ ( tag) fds) = 1  nt tag fds. Just a specialization: bandDCs = band. (see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com Same as  ImageInDTD/, but uses an implicitly applicative function. A constructor type dc inhabits ImageHasTagRepU t fn if  fn3 can be mapped across the recursive occurrences in dc, and  t% has a constructor isomorphic to the fn -image of dc Often times, we';re interested in the universe of types accomodating a data  constructor'"s image under some type-function. A type t inhabits HasTagRepU tag c if t is a  and there exists a t  constructor satisfying  tag c. Given HasTagRepU tag c t, a trivially-mediated c value can be embedded into  t. Given ImageInDTU t fn dc, a trivially-mediated dc value can be  embedded into t. see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com  !"#$%&'()*+,-./0123456789:<>@BDFHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.com  algebraDC determines the "alegbra" from the constructor type and  mediator.  algebraUni determines the "algebra"! from the type-sum and mediator.   algebraDT4 determines the algebra from the type and mediator. A t-algebra reduces a disbanded t to the same mediation of t.  see LANGUAGE pragmas (... GHC) experimentalnicolas.frisby@gmail.comt inhabits  CataU ts m if  t is an instance of  and ts ~ Siblings t , the recursive reduction can be mapped as a  function via   across all constructors of t and  all of t'+s siblings also inhabit the same universe.  Builds an V of algebras via .   Uses the m-mediated algebras for t's siblings to reduce a t to Med  m t.  !"#$%&'()*+,-./012234567899:;<==>?@ABCDDEEFFGHIJKLMNOPQRRSSTTUUVVWWXXYZ[\]^_`abcdefghijklmnoppqrstuvwxyz{|}~                                 !!^_` S T U V W X      yoko-0.2Type.Yoko.TypeType.Yoko.TSTSSType.Yoko.UniverseType.Yoko.NaturalData.Yoko.Core Type.Yoko.SumType.Yoko.BTree Type.Yoko.FunType.Yoko.FunAData.Yoko.GenericType.Yoko.MFunType.Yoko.TFunAData.Yoko.ReflectBaseData.Yoko.ReflectData.Yoko.InDTData.Yoko.ReduceData.Yoko.CataData.Yoko.CoreTypes Type.Yoko Data.Yokotagged-0.2.3.1 Data.ProxyProxytype-equality-0.1.0.2Data.Type.EqualityRefl:=:eqTEqT type-ord-0.1 Type.Ord.BaseIsEQtype-spine-0.1 Type.SpineqKtype-ord-spine-cereal-0.1Type.Ord.SpineSerializeCompareTraversableTSTSS traverseTSTSS FunctorTSTSS fmapTSTSS:.ComposePredUnwrapWrapperwrapunwrapIdMMed composeWithVoidU:||RightULeftU:&&fstUsndUBothNoneU:?Anno:::inhabits inhabits_ inhabitsForArrowTSSNPNTNT_nt_appNTappNTForNTconstNTconstNT_constNTFfirstNTfirstNP appNTtoNPNMFFFRDUVRep:*ElemExistsOnRightOnLeftHereTSumAllSumSSumNSumV:+EachNormWNormEtiniffrUniFinitetoUni InhabitantsPrimUniUniInuprimUniprimUni1finiteNPeqTFinnoneone_oneoneFboth|||.|.||..||eacheachFeachF_prjEachprjEachFeachOrNTAsComp WrapCompFWrapCompRngFDomFYieldsArrowTSSURngDomDomainAppByapplyUapply eachArrowDomainAAppAByIdiomapplyAapplyAUGenericrepobjRMNIRMIRMNRMunDunMunRvoidabsurdFromAttoAtMAppRMMapCAppCMapTAppDTSiblingsDCU packageName moduleNamedisbandDCs LeftmostRange DisbandedAnRMN SiblingOfDCOfDCRangeoccNametagtofrRecursTag disbandedbandTagRepIsRMNTormnToIsDCUnNOnlyDC SiblingsUuniqueDC uniqueRMN uniqueRMN' dcDispatch dcDispatch'bandDCsfr_DCOf ImageInDTDA ImageInDTUHasTagRepImageU HasTagRepU hasTagRepU imageInDTU imageInDTAU AlgebraDC algebraDC AlgebraUni AlgebraDT algebraDTAlgebraUAlgebraAlg algebraFinCataU SiblingAlgsAlgebrasalgebrascatascataghc-prim GHC.TypesTruetype-booleans-0.1 Type.BooleansFalseIfAndOrNotNandNorXorBeqType.Spine.Stage0KSKTSSqPderiveFindCombineIsJustJustNothing WrapCompF_ WrapComp_baseGHC.Base$yieldsArrowTSSUunFunFF pureDomain pureDomainAOneOf algebraUnitwocataD