yoko (empty) → 0.1
raw patch · 38 files changed
+2907/−0 lines, 38 filesdep +basedep +taggeddep +tagged-thsetup-changed
Dependencies added: base, tagged, tagged-th, type-booleans, type-cereal, type-digits, type-equality, type-ord, type-ord-spine-cereal, type-spine
Files
- Data/Yoko.hs +19/−0
- Data/Yoko/Algebra.hs +86/−0
- Data/Yoko/Core.hs +83/−0
- Data/Yoko/CoreTypes.hs +17/−0
- Data/Yoko/Generic.hs +156/−0
- Data/Yoko/InDT.hs +78/−0
- Data/Yoko/Reduce.hs +54/−0
- Data/Yoko/Reflect.hs +103/−0
- Data/Yoko/ReflectBase.hs +106/−0
- Examples/InnerBase.hs +8/−0
- Examples/InnerGeneric.hs +90/−0
- Examples/LL.hs +63/−0
- Examples/LL0.hs +57/−0
- Examples/LLBase.hs +13/−0
- Examples/LLBasics.hs +71/−0
- Examples/LLDirect.hs +81/−0
- Examples/LLGeneric.hs +89/−0
- Examples/Main.hs +25/−0
- Examples/ReflectAux.hs +18/−0
- Examples/TermBase.hs +24/−0
- Examples/TermGeneric.hs +191/−0
- Examples/TermInner.hs +60/−0
- Examples/TermTest.hs +82/−0
- LICENSE +1/−0
- README +249/−0
- Setup.hs +2/−0
- Type/Yoko.hs +36/−0
- Type/Yoko/BTree.hs +175/−0
- Type/Yoko/Fun.hs +136/−0
- Type/Yoko/FunA.hs +36/−0
- Type/Yoko/MFun.hs +97/−0
- Type/Yoko/Natural.hs +82/−0
- Type/Yoko/Sum.hs +102/−0
- Type/Yoko/TFunA.hs +110/−0
- Type/Yoko/TSTSS.hs +29/−0
- Type/Yoko/Type.hs +84/−0
- Type/Yoko/Universe.hs +87/−0
- yoko.cabal +107/−0
+ Data/Yoko.hs view
@@ -0,0 +1,19 @@+{- |++Module : Data.Yoko+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++-}+module Data.Yoko+ (module Type.Yoko, module Data.Yoko.Generic, module Data.Yoko.Reflect, module Data.Yoko.InDT+ ) where++import Type.Yoko+import Data.Yoko.Generic+import Data.Yoko.Reflect+import Data.Yoko.InDT
+ Data/Yoko/Algebra.hs view
@@ -0,0 +1,86 @@+{-# 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
+ Data/Yoko/Core.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, EmptyDataDecls #-}++{-# LANGUAGE TemplateHaskell #-}++{- |++Module : Data.Yoko.Core+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The core structural types; \"sum of products\" and such.++-}++module Data.Yoko.Core where++import Type.Yoko.Type (derive)++--import Polarity++++-- | Structural representations (e.g. "Data.Yoko.Generic"'s 'RM') of a @*@ type+-- can be derived as a data family indexed by the core representation (@Rep@)+-- of that type.+type family Rep a++++-- | void+data V+-- | unit+data U = U+-- | a dependency+newtype D a = D a+-- | a recursive occurrence+newtype R t = R t+-- | argument to a @* -> *@+newtype F f c = F (f c)+-- | arguments to a @* -> * -> *@+newtype FF ff c d = FF (ff c d)+-- | meta information+newtype M i c = M c++-- | a named intermediate (user hook); crucially: @type instance Rep (N t) =+-- Rep t@.+newtype N t = N t++type instance Rep (N t) = Rep t -- this is the crucial meaning of N++++concat `fmap` mapM derive [''V, ''U, ''D, ''R, ''F, ''FF, ''M, ''N]++++infixr 6 :*+type (:*) = FF (,)++++++{-+type instance Polarity ([qK|*->*->*|] M) (ki :* kt :* U) = Neutral+type instance Polarity ([qK|*->*|] (M i)) (kt :* U) = Pos++type instance Polarity ([qK|*->*|] R) (ka :* U) = Pos++type instance Polarity ([qK|(*->*)->*->*|] F) (kf :* kt :* U) = Pos+type instance Polarity ([qK|*->*|] (F f)) (kt :* U) =+ Polarity ([qK|*->*|] f) (kt :* U)++type instance Polarity ([qK|(*->*->*)->*->*->*|] FF) (kff :* kt :* ks :* U) = Pos+type instance Polarity ([qK|*->*->*|] (FF ff)) (kt :* ks :* U) =+ Polarity ([qK|*->*->*|] ff) (kt :* ks :* U)+type instance Polarity ([qK|*->*|] (FF ff t)) (ks :* U) =+ Polarity ([qK|*->*|] (ff t)) (ks :* U)+-}
+ Data/Yoko/CoreTypes.hs view
@@ -0,0 +1,17 @@+{- |++Module : Data.Yoko.CoreTypes+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Just the "Data.Yoko.Core" types -- doesn't export the constructors.++-}++module Data.Yoko.CoreTypes (Rep, V, U, D, R, F, FF, M, N, (:*)) where++import Data.Yoko.Core
+ Data/Yoko/Generic.hs view
@@ -0,0 +1,156 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, QuasiQuotes, StandaloneDeriving,+ FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,+ MultiParamTypeClasses, TypeOperators, EmptyDataDecls #-}++{- |++Module : Data.Yoko.Generic+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Representations of many Haskell types as compositions of "Data.Yoko.Core"+types.++-}++module Data.Yoko.Generic+ (module Data.Yoko.Generic, module Data.Yoko.CoreTypes) where++import Data.Yoko.CoreTypes+--import qualified Data.Yoko.Core as Core++import Type.Yoko.Type+--import Type.Yoko.Universe ((:::)(..))++--import qualified Control.Arrow as Arrow+ ++{- | @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)+ 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)+@++-}+data family RM m c+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)+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)++-- | In @yoko@, the 'N' core type is used for a lightweight representation of+-- constructor types -- each will define its own instance of @RM (N _)@.+type RMN m dc = RM m (N dc)++type RMI = RM IdM+type RMNI dc = RMN IdM dc++++-- | @Generic@ represents a recursion-mediated type @N a@ as a+-- recursion-mediated @Rep a@. The opposite of \"representation\" is (the+-- represented) \"object\".+class Generic a where+ rep :: RM m (N a) -> RM m (Rep a)+ obj :: RM m (Rep a) -> RM m (N a)++{-asRep :: (Generic a, Generic b) => (RM m (Rep a) -> RM m (Rep b)) -> RM m (N a) -> RM m (N b)+asRep f = obj . f . rep++asGist :: (Gist c, Gist d) => (Gst c m -> Gst d n) -> RM m c -> RM n d+asGist f = frip . f . gist++convertR :: (Gist c, Gst c m ~ Gst c n) => RM m c -> RM n c+convertR = asGist id-}+++{-+-- @gist@ folds the mediator @m@ into the type and forgets all the frippery of+-- the core representation. (The opposite of \"gist\" is \"frippery\".)+type family Gst c m+class Gist c where+ gist :: RM m c -> Gst c m+ frip :: Gst c m -> RM m c++data AsRep u t where AsRep :: u (Rep t) -> AsRep u t+instance (Rep t ::: u) => t ::: AsRep u where inhabits = AsRep inhabits++data GistD c where GistD :: Gist c => GistD c+instance Gist c => c ::: GistD where inhabits = GistD+gistD :: GistD c -> RM m c -> Gst c m; gistD GistD = gist+fripD :: GistD c -> Gst c m -> RM m c; fripD GistD = frip++++type instance Gst (F f c) m = f (Gst c m)+instance (Functor f, Gist c) => Gist (F f c) where+ gist (F x) = fmap gist x+ frip = F . fmap frip+type instance Gst (FF Either c d) m = Either (Gst c m) (Gst d m)+instance (Gist c, Gist d) => Gist (FF Either c d) where+ gist = (gist Arrow.+++ gist) . unFF+ frip = FF . (frip Arrow.+++ frip)+type instance Gst (FF (,) c d) m = (,) (Gst c m) (Gst d m)+instance (Gist c, Gist d) => Gist (FF (,) c d) where+ gist = (gist Arrow.*** gist) . unFF+ frip = FF . (frip Arrow.*** frip)+type instance Gst (D a) m = a+instance Gist (D a) where gist (D x) = x; frip = D+type instance Gst (M i c) m = Gst c m+instance Gist c => Gist (M i c) where+ gist = gist . unM; frip = M . frip+type instance Gst (R t) m = Med m t+instance Gist (R t) where gist (R x) = x; frip = R+type instance Gst U m = ()+instance Gist U where gist _ = (); frip _ = U+type instance Gst V m = Core.V+instance Gist V where gist = absurd "gist[V]"; frip _ = void "gist[V]"+type instance Gst (N n) m = Gst (Rep n) m+instance (Generic t, Gist (Rep t)) => Gist (N t) where+ gist = gist . rep; frip = obj . frip+-}+++unD :: RM m (D a) -> a+unD (D x) = x++unM :: RM m (M i c) -> RM m c+unM (M x) = x++unR :: RM m (R t) -> Med m t+unR (R x) = x+deriving instance Eq (Med m t) => Eq (RM m (R t))+deriving instance Show (Med m t) => Show (RM m (R t))++instance Eq (RM m V) where _ == _ = True -- undefined?+instance Show (RM m V) where show _ = "<void>"+void :: String -> RM m V+void n = error $ "GenericR.void: " ++ n+absurd :: String -> RM m V -> a+absurd n = error $ "GenericR.absurd: " ++ n++unF (F x) = x+unFF (FF x) = x+deriving instance Eq (ff (RM m c) (RM m d)) => Eq (RM m (FF ff c d))+deriving instance Show (ff (RM m c) (RM m d)) => Show (RM m (FF ff c d))++++++concat `fmap` mapM derive [''RM]
+ Data/Yoko/InDT.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses,+ FlexibleContexts, UndecidableInstances, Rank2Types #-}++{- |++Module : Data.Yoko.InDT+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Various universes determined by a data constructor type's suitability to be+embedded in a data type.++-}+module Data.Yoko.InDT where++import Type.Yoko++import Data.Yoko.Generic+import Data.Yoko.Reflect++++-- | A type @t@ inhabits @HasTagRepDCD 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+instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)+ ) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits++-- | Given @HasTagRepDCD 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+ 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++++++-- | 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))++-- | A constructor type @dc@ inhabits @ImageHasTagRepDCD 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++-- | Given @ImageInDTD 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++-- | 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+ ) => dc ::: ImageInDTDA t fn where+ inhabits = ImageInDTDA inhabits++imageInDTAD :: 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
+ Data/Yoko/Reduce.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE QuasiQuotes, ScopedTypeVariables, TypeOperators, GADTs,+ MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances,+ FlexibleInstances, UndecidableInstances, TypeFamilies #-}++{- |++Module : Data.Yoko.Reduce+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Reduction of a band of constructors into a mediation of their range.++-}+module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where++import Type.Yoko++import Data.Yoko.Generic+import Data.Yoko.Reflect++++type AnRMNUni m ts = AnRMN m (Uni ts)++++-- | @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)++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++-- | @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)++++type OneOf ts = NP (Uni ts)++two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)+two f g (NP (Uni tag) x) = case tag of+ OnLeft u -> f $ NP (Uni u) x+ OnRight v -> g $ NP (Uni v) x
+ Data/Yoko/Reflect.hs view
@@ -0,0 +1,103 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,+ ScopedTypeVariables, FlexibleContexts, UndecidableInstances, QuasiQuotes,+ TypeOperators, TypeSynonymInstances, Rank2Types, ViewPatterns #-}++{- |++Module : Data.Yoko.Reflect+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Definitions on top of the basic @yoko@ reflection concepts "Data.Yoko.ReflectBase".++-}++module Data.Yoko.Reflect+ (module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where++import Type.Yoko++import Data.Yoko.Generic+import Data.Yoko.ReflectBase++++type instance Tag (N dc) = Tag dc++++type instance Recurs (D a) = V+type instance Recurs (F f c) = Recurs c+type instance Recurs (FF ff c d) =+ NormW (Recurs c) (Recurs d) -- NormW avoiding duplication+type instance Recurs (M i c) = Recurs c+type instance Recurs (N t) = Recurs (Rep t)+type instance Recurs (R t) = N t+type instance Recurs U = V+type instance Recurs V = V++type SiblingsU t = Uni (Siblings t)+++++data IsDC dc where IsDC :: DC dc => IsDC dc+type instance Pred IsDC t = True+instance DC dc => dc ::: IsDC where inhabits = IsDC++newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b}+type instance Unwrap (RMNTo m b) dc = RMN m dc -> b+instance Wrapper (RMNTo m b) where wrap = RMNTo; unwrap = rmnTo+++++-- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.+dcDispatch :: DT t => NT (DCU 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+++++{- | 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 =+ And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))+@++-}+data TagRepIs tag c dc where+ TagRepIs :: (Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc+instance (Tag dc ~ tag, c ~ Rep dc) => dc ::: TagRepIs tag c where+ inhabits = TagRepIs+type instance Pred (TagRepIs tag c) dc =+ And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))++{-data TagGistEQ tag gst m dc where+ TagGistEQ :: (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst+ ) => TagGistEQ tag gst m dc+instance (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst+ ) => dc ::: TagGistEQ tag gst m where inhabits = TagGistEQ+type instance Pred (TagGistEQ tag gst m) dc =+ And (IsEQ (Compare (Tag dc) tag))+ (IsEQ (Compare (Gst (N dc) m) gst))-}++++++-- | Just a specialization: @bandDCs = band@.+bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band++fr_DCOf :: DCOf t dc -> RMNI dc -> t; fr_DCOf (DCOf _) = fr
+ Data/Yoko/ReflectBase.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, TypeOperators,+ FlexibleContexts, ScopedTypeVariables, ViewPatterns, FlexibleInstances,+ QuasiQuotes, UndecidableInstances, Rank2Types #-}++{- |++Module : Data.Yoko.ReflectBase+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The basic @yoko@ reflection concepts.++-}+module Data.Yoko.ReflectBase where++import Type.Yoko+import Data.Yoko.Generic+++-- | The @Tag@ of a constructor type is a type-level reflection of its+-- constructor name.+type family Tag dc++-- | 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)@.+type family Recurs t++-- | The \"Datatype Constructor\" class.+class (DT (Range dc), dc ::: DCU (Range dc), Generic dc) => DC dc where+ -- | The string name of this constructor.+ occName :: [qP|dc|] -> String ++ -- | The range of this constructor.+ type Range dc++ -- | The evidence that this constructor inhabits the datatype constructor+ -- universe of its range.+ tag :: DCU (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+ _ -> Nothing++ -- | Embed this constructor in its range.+ fr :: RMNI dc -> Range dc++-- | Evidence that @t@ is the range of the constructor type @dc@.+data DCOf t dc where DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc+instance (DC dc, t ~ Range dc) => dc ::: DCOf t where inhabits = DCOf inhabits+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+++++type AnRMN m u = NP u (RM m :. N)+type Disbanded m t = AnRMN m (DCOf t)++disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)+disbanded fds = NP (DCOf tag) fds++band :: Disbanded IdM t -> t+band (NP (DCOf _) fds) = fr fds++++-- @LeftmostRange@ returns the @Range@ of the leftmost type in a type-sum.+type family LeftmostRange dcs+type instance LeftmostRange (N dc) = Range dc+type instance LeftmostRange (c :+ d) = LeftmostRange c++type DCs t = Inhabitants (DCU 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)+ ) => DT t where+ -- | The string name of this datatype's original package.+ packageName :: [qP|t|] -> String+ -- | The string name of this datatype's original module.+ moduleName :: [qP|t|] -> String++ -- | 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+ -- binding group. (It also ought to be equivalent to the transitive closure+ -- of @Recurs . DCs@, by definition.)+ type Siblings t+ + -- | The data constructor universe.+ data DCU t :: * -> * -- universe of constructor types++ -- | /Disband/ this type into one of its data constructors.+ disband :: t -> Disbanded IdM t
+ Examples/InnerBase.hs view
@@ -0,0 +1,8 @@+module Examples.InnerBase where++import Examples.TermBase (Type(..))++data Inner = Lam Type Inner+ | Var Int+ | App Inner Inner+ deriving Show
+ Examples/InnerGeneric.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,+ FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,+ TypeSynonymInstances, EmptyDataDecls #-}++{-# OPTIONS_GHC -fcontext-stack=250 #-}++{- |++Module : Examples.InnerGeneric+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The declaration that hook 'Examples.InnerBase.Inner' into @yoko@. This will+eventually be generated via Template Haskell.++-}+module Examples.InnerGeneric where++import qualified Examples.TermBase as B+import Examples.InnerBase (Inner)+import qualified Examples.InnerBase as I++import Examples.ReflectAux++data Lam; data Var; data App++concat `fmap` mapM derive [''Inner, ''Lam, ''Var, ''App]++type instance Tag Lam = $(return $ encode "Lam")+type instance Recurs Lam = N Inner+instance DC Lam where+ occName _ = "Lam"+ type Range Lam = Inner+ fr ~(Lam ty tm) = I.Lam ty tm+data instance RM m (N Lam) = Lam B.Type (Med m Inner)+type instance Tag Var = $(return $ encode "Var")+type instance Recurs Var = V+instance DC Var where+ occName _ = "Var"+ type Range Var = Inner+ fr ~(Var i) = I.Var i+data instance RM m (N Var) = Var Int+type instance Tag App = $(return $ encode "App")+type instance Recurs App = N Inner+instance DC App where+ occName _ = "App"+ type Range App = Inner+ fr ~(App tm0 tm1) = I.App tm0 tm1+data instance RM m (N App) = App (Med m Inner) (Med m Inner)+instance DT Inner where+ packageName _ = "datatype-reflect"+ moduleName _ = "InnerBase"+ type Siblings Inner = N Inner+ data DCU Inner dc where+ Lam_ :: DCU Inner Lam; Var_ :: DCU Inner Var+ App_ :: DCU Inner App+ disband (I.Lam ty tm) = disbanded $ Lam ty tm+ disband (I.Var i) = disbanded $ Var i+ disband (I.App tm0 tm1) = disbanded $ App tm0 tm1+type instance Inhabitants (DCU Inner) = (N Lam :+ N Var) :+ N App+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+ (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+instance EqT (DCU Inner) where eqT = eqTFin+++++type instance Rep Var = D Int+instance Generic Var where+ rep ~(Var i) = D i+ obj ~(D i) = Var i+type instance Rep Lam = D B.Type :* R Inner+instance Generic Lam where+ rep ~(Lam ty tm) = FF (D ty, R tm)+ obj ~(FF (D ty, R tm)) = Lam ty tm+type instance Rep App = R Inner :* R Inner+instance Generic App where+ rep ~(App tm0 tm1) = FF (R tm0, R tm1)+ obj ~(FF (R tm0, R tm1)) = App tm0 tm1
+ Examples/LL.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses,+ FlexibleInstances, UndecidableInstances #-}++{-# OPTIONS_GHC -fcontext-stack=200 #-}++module Examples.LL where++import qualified Examples.InnerBase as I++import qualified Data.Set as Set+import qualified Data.IntMap as IM++import Examples.LLBasics++import qualified Examples.InnerGeneric as IG+import qualified Examples.LLGeneric ()++import Data.Yoko++++++lambdaLift :: Inner -> [Type] -> Prog+lambdaLift x e = Prog (reverse tlds) main where+ (main, tlds) = runMnd (ll x) (e, IM.empty, 0)++llLam (IG.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where+ updE (rho, rn) = (ty : rho, support `prepend` rn) where+ support =+ IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm+llVar (IG.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i++---------------------------------------- default+ll :: Inner -> Mnd Term; ll = applyA (LL :: LL IdM Inner)++data LL m t = LL; type instance Idiom (LL m) = Mnd+type instance Unwrap (LL m) t = LL m t+instance Wrapper (LL m) where wrap = id; unwrap = id++type instance Dom (LL m) t = Med m t+type instance Rng (LL m) t = Med m (TApp (LL m) t)+type instance TApp (LL m) Inner = Term -- instance for each type in binding group++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++++++env0 = [TBool, TBool, TArrow TInt TInt, TInt]+ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0+ex1 = ex0 `I.App` I.Var 3+ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`+ (I.Lam (TArrow TInt TInt) $ I.Var 0)++-- *LL> lambdaLift ex1 env0+-- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),+-- ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))+-- ] (App (App (DVar 0) (Var 2)) (Var 3))
+ Examples/LL0.hs view
@@ -0,0 +1,57 @@++++++module Examples.LL0 where++import qualified Examples.InnerBase as I++import qualified Data.Set as Set+import qualified Data.IntMap as IM++import Examples.LLBasics+++++++++++lambdaLift :: Inner -> [Type] -> Prog+lambdaLift x e = Prog (reverse tlds) main where+ (main, tlds) = runMnd (ll x) (e, IM.empty, 0)++ll (I.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where+ updE (rho, rn) = (ty : rho, support `prepend` rn) where+ support =+ IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm+ll (I.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i++---------------------------------------- default+ll (I.App tm1 tm2) = App <$> ll tm1 <*> ll tm2+ ++++++++++++env0 = [TBool, TBool, TArrow TInt TInt, TInt]+ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0+ex1 = ex0 `I.App` I.Var 3+ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`+ (I.Lam (TArrow TInt TInt) $ I.Var 0)++-- *LL> lambdaLift ex1 env0+-- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),+-- ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))+-- ] (App (App (DVar 0) (Var 2)) (Var 3))
+ Examples/LLBase.hs view
@@ -0,0 +1,13 @@+module Examples.LLBase where++import Examples.TermBase (Type(..))++++data Term = DVar Int | Var Int | App Term Term+ deriving Show++type TLD = ([Type], Type, Term)++data Prog = Prog [TLD] Term+ deriving Show
+ Examples/LLBasics.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE FlexibleInstances, TypeOperators, MultiParamTypeClasses,+ TypeFamilies, UndecidableInstances #-}++module Examples.LLBasics+ (module Examples.LLBasics, module Examples.TermBase,+ module Examples.InnerBase, module Examples.LLBase,+ local, asks, (<$>), (<*>)) where++import Examples.TermBase (Type(..))+import Examples.InnerBase (Inner)+import qualified Examples.InnerBase as I+import Examples.LLBase++import qualified Control.Arrow as Arrow+import qualified Data.Set as Set; import Data.Set (Set)+import qualified Data.IntMap as IM; import Data.IntMap (IntMap)+import Data.Maybe (fromMaybe)++import Control.Monad.Reader.Class (MonadReader(..), asks)+import Control.Monad (ap)+import Control.Applicative (Applicative(pure, (<*>)), (<$>))++++type Frees = Set Int; type Rename = IntMap Int++bump :: Frees -> Frees+bump = Set.map (subtract 1) . Set.filter (> 0)++lookupRN :: Rename -> Int -> Int+lookupRN rn i = fromMaybe i $ IM.lookup i rn++prepend :: Rename -> Rename -> Rename+prepend f = IM.unionWith const f .+ IM.fromDistinctAscList . map ((+ 1) Arrow.*** (+ 1)) . IM.toAscList++++fvs :: Inner -> Frees+fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm+fvs (I.Var i) = Set.singleton i+fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2++++newtype Mnd a = Mnd {runMnd :: ([Type], Rename, Int) -> (a, [TLD])}+instance Functor Mnd where fmap f = (>>= return . f)+instance Applicative Mnd where pure = return; (<*>) = ap+instance Monad Mnd where+ return a = Mnd $ \_ -> (a, [])+ m >>= k = Mnd $ \e@(tys, rn, sh) -> case runMnd m e of+ ~(a, w) -> Arrow.second (w ++) $ runMnd (k a) (tys, rn, sh + length w)+instance (e ~ ([Type], Rename)) => MonadReader e Mnd where+ ask = Mnd $ \ ~(x, y, _) -> ((x, y), []);+ local f (Mnd g) =+ Mnd $ \ ~(x, y, z) -> case f (x, y) of+ ~(x', y') -> g (x', y', z)++numEmissions :: Mnd Int+numEmissions = Mnd $ \ ~(_, _, z) -> (z, [])++emit :: [TLD] -> Mnd ()+emit w = Mnd $ \_ -> ((), w)++newTLD :: Type -> Frees -> Mnd Term -> Mnd Term+-- NB could check if such a TLD already exists+newTLD ty fvs m = do+ (rho, rn) <- ask; sh <- numEmissions+ let fvs' = reverse $ Set.toAscList $ bump fvs+ m >>= \tm -> emit [(map (rho !!) fvs', ty, tm)]+ return $ foldl ((. Var . lookupRN rn) . App) (DVar sh) fvs'
+ Examples/LLDirect.hs view
@@ -0,0 +1,81 @@+{- |++Module : Examples.LLDirect+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Lambda-lifts 'Examples.InnerBase.Inner' to 'Examples.LLBase.LL' without using+@yoko@. Compare to "Examples.LL0" and "Examples.LL".++-}+module Examples.LLDirect where++import Examples.TermBase (Type(..))+import Examples.InnerBase (Inner)+import qualified Examples.InnerBase as I+import Examples.LLBase++import qualified Data.Set as Set; import Data.Set (Set)+import qualified Data.IntMap as IM; import Data.IntMap (IntMap)++++fvs :: Inner -> Set Int+fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm+fvs (I.Var i) = Set.singleton i+fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2++bump :: Set Int -> Set Int+bump = Set.map (subtract 1) . Set.filter (> 0)++renm :: IntMap Int -> Int -> Term -> Term+renm m dv tm@(Var i) = maybe tm Var $ IM.lookup i m+renm m dv (App tm1 tm2) = App (renm m dv tm1) (renm m dv tm2)+renm _ dv (DVar i) = DVar (i + dv)++renmP :: IntMap Int -> Int -> Prog -> Prog+renmP m dv (Prog tlds main) = Prog (map each tlds) (renm m dv main) where+ each (tys, ty, tm) = (tys, ty, renm m dv tm)+++++type Env = [Type]++lambdaLift :: Inner -> Env -> Prog+lambdaLift (I.Lam ty tm) rho = newTLD ty rho (fvs tm) $ lambdaLift tm (ty : rho)+lambdaLift (I.Var i) rho = Prog [] $ Var i+lambdaLift (I.App tm1 tm2) rho = Prog (tlds1 ++ tlds2) $ App main1 main2 where+ Prog tlds1 main1 = lambdaLift tm1 rho+ Prog tlds2 main2 = renmP IM.empty (length tlds1) $ lambdaLift tm2 rho++++newTLD :: Type -> Env -> Set Int -> Prog -> Prog+-- NB could check if such a TLD already exists; lambdaLift@I.App would need to handle+-- that too+newTLD ty rho fvs (Prog tlds main) =+ Prog ((map (rho !!) fvs', ty, renm rn 0 main) : tlds) $+ foldl ((. Var) . App) (DVar 0) fvs'+ where rn = IM.fromDistinctAscList $ zip (Set.toAscList fvs) [0..]+ fvs' = reverse $ Set.toAscList $ bump fvs++++++env0 = [TBool, TBool, TArrow TInt TInt, TInt]+ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0+ex1 = ex0 `I.App` I.Var 3+ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`+ (I.Lam (TArrow TInt TInt) $ I.Var 0)+++-- *LL> ll ex1 env0+-- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),+-- ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))+-- ] (App (App (DVar 0) (Var 2)) (Var 3))
+ Examples/LLGeneric.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,+ FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,+ TypeSynonymInstances, EmptyDataDecls #-}++{-# OPTIONS_GHC -fcontext-stack=250 #-}++{- |++Module : Examples.LLGeneric+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The declaration that hook 'Examples.LLBase.Term' into @yoko@. This will+eventually be generated via Template Haskell.++-}+module Examples.LLGeneric where++import Examples.LLBase (Term)+import qualified Examples.LLBase as B++import Examples.ReflectAux++data DVar; data Var; data App++concat `fmap` mapM derive [''Term, ''DVar, ''Var, ''App]++type instance Tag DVar = $(return $ encode "DVar")+type instance Recurs DVar = V+instance DC DVar where+ occName _ = "DVar"+ type Range DVar = Term+ fr ~(DVar i) = B.DVar i+data instance RM m (N DVar) = DVar Int+type instance Tag Var = $(return $ encode "Var")+type instance Recurs Var = V+instance DC Var where+ occName _ = "Var"+ type Range Var = Term+ fr ~(Var i) = B.Var i+data instance RM m (N Var) = Var Int+type instance Tag App = $(return $ encode "App")+type instance Recurs App = N Term+instance DC App where+ occName _ = "App"+ type Range App = Term+ fr ~(App tm0 tm1) = B.App tm0 tm1+data instance RM m (N App) = App (Med m Term) (Med m Term)+instance DT Term where+ packageName _ = "datatype-reflect"+ moduleName _ = "TermBase"+ type Siblings Term = N Term+ data DCU Term dc where+ DVar_ :: DCU Term DVar; Var_ :: DCU Term Var+ App_ :: DCU Term App+ disband (B.DVar i) = disbanded $ DVar i+ disband (B.Var i) = disbanded $ Var i+ disband (B.App tm0 tm1) = disbanded $ App tm0 tm1+type instance Inhabitants (DCU Term) = (N DVar :+ N Var) :+ N App+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+ (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+instance EqT (DCU Term) where eqT = eqTFin+++++type instance Rep DVar = D Int+instance Generic DVar where+ rep ~(DVar i) = D i+ obj ~(D i) = DVar i+type instance Rep Var = D Int+instance Generic Var where+ rep ~(Var i) = D i+ obj ~(D i) = Var i+type instance Rep App = R Term :* R Term+instance Generic App where+ rep ~(App tm0 tm1) = FF (R tm0, R tm1)+ obj ~(FF (R tm0, R tm1)) = App tm0 tm1
+ Examples/Main.hs view
@@ -0,0 +1,25 @@+{- |++Module : Examples.Main+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Just bundles up the three examples.++-}+module Main where++import Examples.TermTest+import Examples.TermInner+import Examples.LL++++main = do+ print $ Examples.TermTest.ex1+ print $ Examples.TermInner.ex1+ print $ lambdaLift Examples.LL.ex1 env0
+ Examples/ReflectAux.hs view
@@ -0,0 +1,18 @@+{- |++Module : Examples.ReflectAux+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Just bundles up some imports for the various @*Generic@ modules.++-}+module Examples.ReflectAux (encode, module Data.Yoko) where++import Type.Serialize++import Data.Yoko hiding (qK)
+ Examples/TermBase.hs view
@@ -0,0 +1,24 @@+{- |++Module : Examples.TermBase+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++-}+module Examples.TermBase where++data Type = TBool | TInt | TArrow Type Type+ deriving Show++data Term = Lam Type Term+ | Var Int+ | App Term Term+ | Let [Decl] Term+ deriving Show++data Decl = Decl Type Term+ deriving Show
+ Examples/TermGeneric.hs view
@@ -0,0 +1,191 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,+ FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,+ TypeSynonymInstances, EmptyDataDecls #-}++{-# OPTIONS_GHC -fcontext-stack=250 #-}++{- |++Module : Examples.TermGeneric+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The declaration that hook 'Examples.TermBase.Type', 'Examples.TermBase.Term',+and 'Examples.TermBase.Decl' into @yoko@. This will eventually be generated via+Template Haskell.++-}+module Examples.TermGeneric where++import qualified Examples.TermBase as B++import Examples.ReflectAux++data TBool; data TInt; data TArrow+data Lam; data Var; data App; data Let+data Decl++concat `fmap` mapM derive+ [''B.Type, ''TBool, ''TInt, ''TArrow,+ ''B.Term, ''Lam, ''Var, ''App, ''Let,+ ''B.Decl, ''Decl]++type instance Tag TBool = $(return $ encode "TBool")+type instance Recurs TBool = U+instance DC TBool where+ occName _ = "TBool"+ type Range TBool = B.Type+ fr _ = B.TBool+data instance RM m (N TBool) = TBool+type instance Tag TInt = $(return $ encode "TInt")+type instance Recurs TInt = U+instance DC TInt where+ occName _ = "TInt"+ type Range TInt = B.Type+ fr _ = B.TInt+data instance RM m (N TInt) = TInt+type instance Tag TArrow = $(return $ encode "TArrow")+type instance Recurs TArrow = N B.Type+instance DC TArrow where+ occName _ = "TArrow"+ type Range TArrow = B.Type+ fr ~(TArrow d r) = B.TArrow d r+data instance RM m (N TArrow) = TArrow (Med m B.Type) (Med m B.Type)+instance DT B.Type where+ packageName _ = "datatype-reflect"+ moduleName _ = "TermBase"+ type Siblings B.Type = N B.Type+ data DCU B.Type dc where+ TBool_ :: DCU B.Type TBool; TInt_ :: DCU B.Type TInt+ TArrow_ :: DCU B.Type TArrow+ disband B.TBool = disbanded TBool+ disband B.TInt = disbanded TInt+ disband (B.TArrow d r) = disbanded $ TArrow d r+type instance Inhabitants (DCU B.Type) = N TBool :+ N TInt :+ N TArrow+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+ (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+instance EqT (DCU B.Type) where eqT = eqTFin++type instance Tag Lam = $(return $ encode "Lam")+type instance Recurs Lam = N B.Term+instance DC Lam where+ occName _ = "Lam"+ type Range Lam = B.Term+ fr ~(Lam ty tm) = B.Lam ty tm+data instance RM m (N Lam) = Lam B.Type (Med m B.Term)+type instance Tag Var = $(return $ encode "Var")+type instance Recurs Var = U+instance DC Var where+ occName _ = "Var"+ type Range Var = B.Term+ fr ~(Var i) = B.Var i+data instance RM m (N Var) = Var Int+type instance Tag App = $(return $ encode "App")+type instance Recurs App = N B.Term+instance DC App where+ occName _ = "App"+ type Range App = B.Term+ fr ~(App tm0 tm1) = B.App tm0 tm1+data instance RM m (N App) = App (Med m B.Term) (Med m B.Term)+type instance Tag Let = $(return $ encode "Let")+type instance Recurs Let = N B.Decl :+ N B.Term+instance DC Let where+ occName _ = "Let"+ type Range Let = B.Term+ fr ~(Let ds tm) = B.Let ds tm+data instance RM m (N Let) = Let [Med m B.Decl] (Med m B.Term)+instance DT B.Term where+ packageName _ = "datatype-reflect"+ moduleName _ = "TermBase"+ type Siblings B.Term = N B.Term :+ N B.Decl+ data DCU B.Term dc where+ Lam_ :: DCU B.Term Lam; Var_ :: DCU B.Term Var+ App_ :: DCU B.Term App; Let_ :: DCU B.Term Let+ disband (B.Lam ty tm) = disbanded $ Lam ty tm+ disband (B.Var i) = disbanded $ Var i+ disband (B.App tm0 tm1) = disbanded $ App tm0 tm1+ disband (B.Let ds tm) = disbanded $ Let ds tm+type instance Inhabitants (DCU B.Term) = (N Lam :+ N Var) :+ (N App :+ N Let)+instance Finite (DCU B.Term) where+ toUni Lam_ = inhabits; toUni Var_ = inhabits+ toUni App_ = inhabits; toUni Let_ = inhabits+instance Etinif (DCU B.Term) where+ fromUni (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+instance EqT (DCU B.Term) where eqT = eqTFin++type instance Tag Decl = $(return $ encode "Decl")+type instance Recurs Decl = N B.Term+instance DC Decl where+ occName _ = "Decl"+ type Range Decl = B.Decl+ to = Just . uniqueTo; 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"+ type Siblings B.Decl = N B.Term :+ N B.Decl+ data DCU B.Decl dc where Decl_ :: DCU B.Decl Decl+ disband ~(B.Decl ty tm) = disbanded $ Decl ty tm+type instance Inhabitants (DCU B.Decl) = N Decl+instance Finite (DCU B.Decl) where+ toUni Decl_ = inhabits+instance Etinif (DCU B.Decl) where+ fromUni (Uni (Here Refl)) = Decl_+instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where+ inhabits = fromUni inhabits+instance EqT (DCU B.Decl) where eqT = eqTFin++++type instance Rep TBool = V+instance Generic TBool where+ rep _ = void "rep[TBool]"+ obj _ = TBool+type instance Rep TInt = V+instance Generic TInt where+ rep _ = void "rep[TInt]"+ obj _ = TInt+type instance Rep TArrow = R B.Type :* R B.Type+instance Generic TArrow where+ rep ~(TArrow ty0 ty1) = FF (R ty0, R ty1)+ obj ~(FF (R ty0, R ty1)) = TArrow ty0 ty1++type instance Rep Var = D Int+instance Generic Var where+ rep ~(Var i) = D i+ obj ~(D i) = Var i+type instance Rep Lam = D B.Type :* R B.Term+instance Generic Lam where+ rep ~(Lam ty tm) = FF (D ty, R tm)+ obj ~(FF (D ty, R tm)) = Lam ty tm+type instance Rep App = R B.Term :* R B.Term+instance Generic App where+ rep ~(App tm0 tm1) = FF (R tm0, R tm1)+ obj ~(FF (R tm0, R tm1)) = App tm0 tm1+type instance Rep Let = F [] (R B.Decl) :* R B.Term+instance Generic Let where+ rep ~(Let ds tm) = FF (F (map R ds), R tm)+ obj ~(FF (F rds, R tm)) = Let (map unR rds) tm++type instance Rep Decl = D B.Type :* R B.Term+instance Generic Decl where+ rep ~(Decl ty tm) = FF (D ty, R tm)+ obj ~(FF (D ty, R tm)) = Decl ty tm
+ Examples/TermInner.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,+ UndecidableInstances #-}++{-# OPTIONS_GHC -fcontext-stack=200 #-}++{- |++Module : Examples.TermInner+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++A let-elaboration via "Data.Yoko.InDT".++-}+module Examples.TermInner where++import Examples.TermBase+import Examples.InnerBase (Inner)+import qualified Examples.InnerBase as I+import qualified Examples.TermGeneric as G+import Examples.InnerGeneric ()++import Type.Yoko++import Data.Yoko.InDT+import Data.Yoko.Reflect++++++elaborate :: Term -> Inner; elaborate = apply (Elab :: Elab IdM Term)++data Elab m t = Elab+type instance Unwrap (Elab m) t = Elab m t+instance Wrapper (Elab m) where wrap = id; unwrap = id++type instance Dom (Elab m) t = Med m t+type instance Rng (Elab m) t = Med m (TApp (Elab m) t)++type instance TApp (Elab m) Term = Inner++instance (IdM ~ m) => Term ::: Domain (Elab m) where+ inhabits = AppBy $ \_ -> dcDispatch $+ eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTD Elab++elab_Let (G.Let ds tm) =+ foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds++++++ex0 = Let [Decl TInt (Var 111), Decl TBool (Var 222)] (Var 0)++ex1 = elaborate ex0
+ Examples/TermTest.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE QuasiQuotes, TypeFamilies, FlexibleInstances,+ MultiParamTypeClasses, GADTs, PatternGuards #-}++{-# OPTIONS_GHC -fcontext-stack=200 #-}++{- |++Module : Examples.TermTest+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++A denotational semantics for the simple-typed lambda calculus via+"Data.Yoko.Algebra".++-}+module Examples.TermTest where++import Examples.TermBase+import qualified Examples.TermGeneric as G++import Type.Yoko+import Data.Yoko.Algebra+++-- | Since our family of abstract data types don't correspond to the+-- object-language types, we need a tagged universal value space.+data Val = VBool Bool | VInt Int | VFun (Val -> Val)+instance Show Val where+ show (VBool b) = show b; show (VInt i) = show i; show (VFun _) = "<fun>"++++eLam (G.Lam _ t) e = VFun $ t . (: e)+eVar (G.Var i) = (!! i)+eApp (G.App t1 t2) e+ | VFun f <- t1 e = f (t2 e)+ | otherwise = error "failed projection in reduce[App]"+eLet (G.Let ds t) = foldr cons t ds where cons (_, s) t e = t (s e : e)++eDecl (G.Decl ty t) = (ty, t)+++-- | The semantic domain of the reduction.+type Sem = [Val] -> Val++-- | The recursion mediator for our denotation.+data SemM = SemM+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 ReduceDC SemM G.Decl where reduceDC = eDecl++eval x = ($ x) $ cata $ algebras [qP|SemM|]++-- NB equivalent+eval' x = ($ x) $ cata $ (reduce .|. reduce) -- :: AlgebraFam Term SemM)++++++vSucc = VFun $ \(VInt i) -> VInt $ i + 1+++ex0 = eval (Var 0) [VBool True]+ex1 = eval (Let [Decl (TInt `TArrow` TInt) $ Lam TInt (Var 0) `App` Var 0 `App` Var 1]+ (Var 0)) [vSucc, VInt 9]+ex2' = eval (Decl TInt (Var 0))+ex2 = snd ex2' [VInt 3]+++--ex1' = eval' (Let [Decl (TInt `TArrow` TInt) (Var 0 `App` Var 1)]+-- (Var 0)) [vSucc, VInt 9]
+ LICENSE view
@@ -0,0 +1,1 @@+BSD3
+ README view
@@ -0,0 +1,249 @@+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++...
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Type/Yoko.hs view
@@ -0,0 +1,36 @@+{- |++Module : Type.Yoko+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++-}++module Type.Yoko (+ module Type.Yoko.Type,+ module Type.Yoko.Universe,+ module Type.Yoko.Natural,+ module Type.Yoko.BTree,+ module Type.Yoko.Sum,+ module Type.Yoko.TSTSS,+ module Type.Yoko.Fun,+ module Type.Yoko.FunA,+ module Type.Yoko.MFun,+ module Type.Yoko.TFunA+ ) where++import Type.Yoko.Type+import Type.Yoko.Universe+import Type.Yoko.Natural+import Type.Yoko.BTree+import Type.Yoko.Sum+import Type.Yoko.TSTSS++import Type.Yoko.Fun+import Type.Yoko.FunA+import Type.Yoko.MFun+import Type.Yoko.TFunA
+ Type/Yoko/BTree.hs view
@@ -0,0 +1,175 @@+{-# LANGUAGE TypeFamilies, ScopedTypeVariables, QuasiQuotes, Rank2Types,+ GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,+ UndecidableInstances, EmptyDataDecls, TypeOperators #-}++{-# LANGUAGE TemplateHaskell #-}++{- |++Module : Type.Yoko.BTree+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Operators for the type-sums from "Type.Yoko.Sum".++-}++module Type.Yoko.BTree where++import Type.Yoko.Type+import Type.Yoko.Universe+import Type.Yoko.Natural+import Data.Yoko.Core+import Type.Yoko.Sum++++++-- | @Inu t@ is a universe of type-sums containing @t@.+type Inu t = Exists ((:=:) t)++-- | @Uni ts@ is a universe containing the types in the type-sum @ts@.+newtype Uni ts t = Uni (Inu t ts)++instance (ts ::: Inu t) => t ::: Uni ts where inhabits = Uni inhabits++type instance Pred (Uni ts) t = Elem t ts++instance (ts ::: TSum) => 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+ w (OnLeft u) (OnLeft v) = w u v+ w (OnRight u) (OnRight v) = w u v+ w _ _ = Nothing ++++++-- | A @Uni ts t@ value can also be understood in terms of more primitive+-- universes, 'VoidU', @':=:'@ and @':||'@ for 'V', 'N', and @':+'@,+-- respectively.+type family PrimUni ts :: * -> *+type instance PrimUni V = VoidU+type instance PrimUni (N t) = (:=:) t+type instance PrimUni (ts :+ us) = PrimUni ts :|| PrimUni us++primUni :: Uni ts t -> PrimUni ts t+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++primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t+primUni1 (Uni (OnLeft u)) = LeftD $ Uni u+primUni1 (Uni (OnRight v)) = RightD $ Uni v+++++-- | Finite universes can be represented as type-sums.+type family Inhabitants u+class (Inhabitants u ::: TSum) => Finite u where+ toUni :: u t -> Uni (Inhabitants u) t++-- | @fromUni@ 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++-- | Any finite universe can be used to determine type equality.+eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v+ ) => u a -> v b -> Maybe (a :=: b)+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++++-- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a+-- type-sum.+type family Norm c+type instance Norm V = V+type instance Norm (N t) = N t+type instance Norm (ts :+ us) = NormW (ts :+ us) V++-- | @NormW@ combines two type-sums into a right-associated type-sum containing+-- no duplicates.+type family NormW c acc+type instance NormW V acc = acc+type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc)+type instance NormW (ts :+ us) acc = NormW ts (NormW us acc)+++++-- | @Each ts f@ provides a @'NT' t f@ for each @t@ in the type-sum @ts@.+type Each ts = NT (Uni ts)++none :: String -> Each V f+none s = NT $ error $ "TypeBTree.none: " ++ s++one_ :: [qP|f :: *->*|] -> Unwrap f t -> Each (N t) f+one_ p x = firstNT primUni $ constNT_ p x++one :: Unwrap f t -> Each (N t) f+one = one_ Proxy++oneF :: Wrapper f => f t -> Each (N t) f+oneF x = firstNT primUni $ constNTF x++infixr 6 |||, .|.+both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f+both f g = firstNT primUni1 $ orNT f g; (|||) = both++infixl 5 ||.; infixr 5 .||+(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f+(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f+(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f+f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g++++-- | @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+ 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 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)++++-- | Just a specialization: @prjEach x f = 'appNT' f x@.+prjEach :: Uni ts t -> Each ts f -> Unwrap f t+prjEach x f = appNT f x++prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t+prjEachF = (wrap .) . prjEach+++++-- | @eachOrNT fs gs@ builds an 'NT' that uses @fs@ for as many types in the+-- universe @v@ as possible, and uses @gs@ for the rest. It's an extension of+-- 'orNT' to @Each@.+eachOrNT :: forall u v f w.+ (Inhabitants v ::: All (u :|| w), Finite v) => NT u f -> NT w f -> NT v f+eachOrNT fs dflt = firstNT toUni $ each Proxy $ appNT $ orNT fs dflt
+ Type/Yoko/Fun.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE TypeFamilies, FlexibleContexts, Rank2Types, QuasiQuotes,+ TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances,+ MultiParamTypeClasses, UndecidableInstances #-}++{- |++Module : Type.Yoko.Fun+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++An explicit perspective on (both parametric and ad-hoc) polymorphic+functions. The datatype representing such a function must be of kind @* -> *@;+the parameter is the type at which the function is to be instantiated.++-}++module Type.Yoko.Fun+ (Domain(..), Dom, Rng, applyD, apply,+ YieldsArrowTSSD, DomF, RngF, eachArrow,+ AsComp(..), WrapComp, WrapCompF+ ) where++import Type.Yoko.Type+import Type.Yoko.Universe+import Type.Yoko.Natural+import Type.Yoko.Sum+import Type.Yoko.BTree+++++-- | @Domain fn@ is the universe of types at which @fn@ can be applied; it's+-- the type-level domain of @fn@.+newtype Domain fn t = AppBy (fn t -> Dom fn t -> Rng fn t)++-- | @Dom fn t@ is the domain of @fn@ at type @t@; it's the term-level domain+-- of @fn@ at @t@.+type family Dom (fn :: * -> *) t+-- | @Rng fn t@ is the range of @fn@ at type @t@; it's the term-level range of+-- @fn@ at @t@.+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++-- | @apply = applyD inhabits@.+apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t+apply = applyD inhabits++++-- | @YieldsArrowTSSD 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 ::+ (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t+ ) => Domain fn t -> YieldsArrowTSSD 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++-- | Used by @YieldsArrowTSSD fn@ to structure the domain of @fn@.+type family DomF (fn :: * -> *) :: * -> *+-- | Used by @YieldsArrowTSSD 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++-- | 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)+ ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))+eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $+ \d -> yieldsArrowTSSD d fn++++++type instance Dom (fn :. f) a = Dom fn (f a)+type instance Rng (fn :. f) a = Rng fn (f a)+type instance DomF (fn :. f) = DomF fn+type instance RngF (fn :. f) = RngF fn+instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where+ inhabits = AppBy $ \(Compose fn) -> apply fn++++++-- | Only instance: @type instance WrapComp_ (f (g a)) = (f :. g) a@.+type WrapComp a = WrapComp_ a+type family WrapComp_ a+type instance WrapComp_ (f (g a)) = (f :. g) a++-- | Only instance: @type instance WrapCompF_ (f (g a)) = f :. g@.+type WrapCompF a = WrapCompF_ a+type family WrapCompF_ a :: * -> *+type instance WrapCompF_ (f (g a)) = f :. g++++++{- | Defining instances:++@+ type instance Dom (AsComp fn) t = WrapComp (Dom fn t)+ type instance Rng (AsComp fn) t = WrapComp (Rng fn t)+ inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap+@++-}+newtype AsComp (fn :: * -> *) t = AsComp (fn t)++type instance Unwrap (AsComp fn) t = fn t+instance Wrapper (AsComp fn) where wrap = AsComp; unwrap (AsComp x) = x++type instance Dom (AsComp fn) t = WrapComp (Dom fn t)+type instance Rng (AsComp fn) t = WrapComp (Rng fn t)++type instance DomF (AsComp fn) = WrapCompF (Dom fn ())+type instance RngF (AsComp fn) = WrapCompF (Rng fn ())++instance (t ::: Domain fn, Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)+ ) => t ::: Domain (AsComp fn) where+ inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
+ Type/Yoko/FunA.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}++{- |++Module : Type.Yoko.FunA+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++"Type.Yoko.Fun" functions that /implicitly/ return an applicative functor. The+implicitness means that the 'Rng' type instance is not expected to include the+applicative functor.++-}++module Type.Yoko.FunA+ (Idiom, DomainA(..), applyA, applyAD) where++import Type.Yoko.Fun+import Type.Yoko.Universe++++++type family Idiom (fn :: * -> *) :: * -> *+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++applyAD :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)+applyAD (AppABy f) = f
+ Type/Yoko/MFun.hs view
@@ -0,0 +1,97 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,+ ScopedTypeVariables, UndecidableInstances, QuasiQuotes, TypeFamilies,+ GADTs, TypeOperators, Rank2Types #-}++{- |++Module : Type.Yoko.MFun+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++An enrichment of "Type.Yoko.Fun" where functions must be of kind @* -> * -> *@;+the first parameter is a mediator and the second is (as expected by+"Type.Yoko.Fun") the type at which the function is to be instantiated.++-}++module Type.Yoko.MFun where++import Type.Yoko.TSTSS++import Type.Yoko.Type+import Type.Yoko.Universe+import Type.Yoko.Natural++import Type.Yoko.Fun++import Data.Yoko.Generic+++++-- | mediator-functions can be mapped across an 'RM' type/value.+newtype RMMap u fn m c = RMMap (NT u (fn m))++{- | mediator-functions can also modify the mediator; e.g.++@+ type instance 'Dom' (RMMap u fn m) c = RM m c+ type instance 'Rng' (RMMap u fn m) c = RM (MApp fn m) c+@++-}+type family MApp (fn :: * -> * -> *) m++type instance Dom (RMMap u fn m) c = RM m c+type instance Rng (RMMap u fn m) c = RM (MApp fn m) c++type instance MApp (RMMap u fn) m = MApp fn m++instance (t ::: u, t ::: Domain (fn m), Wrapper (fn m),+ Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t+ ) => R t ::: Domain (RMMap u fn m) where+ inhabits = AppBy $ \(RMMap fns) ->+ R . apply (fns `appNTF` inhabitsFor [qP|t|]) . unR++instance (Rep t ::: Domain (RMMap u fn m), Generic t+ ) => N t ::: Domain (RMMap u fn m) where+ inhabits = AppBy $ \(RMMap fn) -> obj . apply (RMMap fn) . rep++instance D a ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ -> D . unD+instance U ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ _ -> U+instance (Functor f, c ::: Domain (RMMap u fn m)+ ) => F f c ::: Domain (RMMap u fn m) where+ inhabits = AppBy $ \(RMMap fn) -> F . fmap (apply (RMMap fn)) . unF+instance (c ::: Domain (RMMap u fn m), d ::: Domain (RMMap u fn m),+ FunctorTSTSS ff) => FF ff c d ::: Domain (RMMap u fn m) where+ inhabits = AppBy $ \(RMMap fn) -> FF .+ fmapTSTSS (apply (RMMap fn)) (apply (RMMap fn)) . unFF+instance (c ::: Domain (RMMap u fn m)) => M i c ::: Domain (RMMap u fn m) where+ inhabits = AppBy $ \(RMMap fn) -> M . apply (RMMap fn) . unM++++++type instance DomF (RMMap u fn m) = RM m+type instance RngF (RMMap u fn m) = RM (MApp fn m)+++++-- | A @FromAt@ function is applicable only at the specified mediator and type;+-- crucially @type instance MApp (FromAt m) n = m@.+newtype FromAt m n a = FromAt {toAt :: Med n a -> Med m a}++type instance Unwrap (FromAt m n) a = Med n a -> Med m a+instance Wrapper (FromAt m n) where wrap = FromAt; unwrap (FromAt x) = x++type instance Dom (FromAt m n) t = Med n t+type instance Rng (FromAt m n) t = Med m t+instance a ::: Domain (FromAt m n) where inhabits = AppBy toAt++type instance MApp (FromAt m) n = m
+ Type/Yoko/Natural.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE ExistentialQuantification, QuasiQuotes, TypeOperators,+ Rank2Types, GADTs, ScopedTypeVariables, TypeFamilies #-}++{- |++Module : Type.Yoko.Natural+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Natural transformations and pairs.++-}++module Type.Yoko.Natural where++import Type.Yoko.Type+import Type.Yoko.Universe++++type NT_ u f = forall t. u t -> f t++-- | Natural transformations. We use 'Unwrap' to lighten the user interface at+-- the value level, though it clutters the types a little.+newtype NT u f = NT (forall t. u t -> Unwrap f t)++nt_ :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f+nt_ p f = NT f+++appNT :: NT u f -> u t -> Unwrap f t+appNT (NT f) x = f x++appNTF :: Wrapper f => NT u f -> NT_ u f+appNTF (NT f) x = wrap (f x)+++-- | Defining an @NT@ via type-level backtracking; ':||' uses 'Pred' to+-- 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+++constNT :: Unwrap f t -> NT ((:=:) t) f+constNT = constNT_ Proxy++constNT_ :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f+constNT_ p x = nt_ p $ \Refl -> x++constNTF :: Wrapper f => f t -> NT ((:=:) t) f+constNTF x = NT $ \Refl -> unwrap x+++firstNT :: NT_ u g -> NT g f -> NT u f+firstNT g (NT f) = NT $ f . g++++++-- | Natural pairs.+data NP u f = forall t. NP (u t) (Unwrap f t)++-- | Analog to "Control.Arrow"@.first@.+firstNP :: NT_ u v -> NP u f -> NP v f+firstNP f (NP u x) = NP (f u) x+++-- | @ArrowTSS@ can be partially applied, and hence occur as the second+-- argument of @NT@, where as @f _ -> g _@ cannot.+newtype ArrowTSS f g a = ArrowTSS (f a -> g a)+type instance Unwrap (ArrowTSS f g) a = f a -> g a+instance Wrapper (ArrowTSS f g) where wrap = ArrowTSS; unwrap (ArrowTSS f) = f++appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g+appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x
+ Type/Yoko/Sum.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, EmptyDataDecls,+ QuasiQuotes, UndecidableInstances, ScopedTypeVariables,+ MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances,+ FlexibleContexts #-}++{-# LANGUAGE TemplateHaskell #-}++{- |++Module : Type.Yoko.Sum+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Finite sums of types.++-}++module Type.Yoko.Sum ((:+), All(..), TSum, Exists(..), Elem) where++import Type.Yoko.Type+import Type.Yoko.Universe+import Data.Yoko.CoreTypes++++infixr 5 :++-- | Type-sum union. We re-use 'N' as type-sum singleton and 'V' as the empty+-- type-sum.+data t :+ s++++-- | The higher-order universe @All@. @c@ inhabits @All u@ if @c@ is a type-sum+-- and all types in it inhabit @u@.+data All u c where+ SumV :: All u V+ SumN :: (t ::: u) => u t -> All u (N t)+ SumS :: All u c -> All u d -> All u (c :+ d)++instance V ::: All u where inhabits = SumV+instance (t ::: u) => N t ::: All u where inhabits = SumN inhabits+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++++++-- | The higher-order universe @Exists@. @c@ inhabits @Exists p@ if there+-- exists a type @t@ in the type-sum @c@ for which @'True' ~ 'Pred' p t@. NB+-- that @c@ is not necessarily a type-sum; i.e. there is no well-typed total+-- function from @Exists p c@ to @TSum c@.+data Exists p c where+ Here :: p t -> Exists p (N t)+ OnLeft :: Exists p c -> Exists p (c :+ d)+ OnRight :: Exists p d -> Exists p (c :+ d)++++data Nothing; data Just path++type family IsJust a+type instance IsJust Nothing = False+type instance IsJust (Just path) = True++type family Combine l r+type instance Combine Nothing Nothing = Nothing+type instance Combine Nothing (Just x) = Just (OnRight x)+type instance Combine (Just x) r = Just (OnLeft x)++++data Here+data OnLeft x+data OnRight x++-- | @Elem t ts@ is 'True' if @t@ occurs in the type sum @ts@.+type Elem t ts = IsJust (Find ((:=:) t) ts)++type family Find (pred :: * -> *) c+type instance Find p (N t) = If (Pred p t) (Just Here) Nothing+type instance Find p (c :+ d) = Combine (Find p c) (Find p d)+type instance Find p V = Nothing++++instance (Just path ~ Find p c, c ::: Exists p :? path) => c ::: Exists p where+ inhabits = inhabits_ [qP|path|]++instance (t ::: p) => N t ::: Exists p :? Here where+ inhabits = Anno $ Here inhabits+instance (c ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnLeft path where+ inhabits = Anno $ OnLeft (inhabits_ [qP|path|])+instance (d ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnRight path where+ inhabits = Anno $ OnRight (inhabits_ [qP|path|])
+ Type/Yoko/TFunA.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses,+ FlexibleInstances, UndecidableInstances, QuasiQuotes, ScopedTypeVariables,+ Rank2Types #-}++{- |++Module : Type.Yoko.TFunA+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++The type-level functionality of "Type.Yoko.FunA" functions.++-}++module Type.Yoko.TFunA (TApp, CMap(..), CApp) where++import Type.Yoko.TSTSS++import Type.Yoko.Fun+import Type.Yoko.FunA++import Type.Yoko.Type+import Type.Yoko.Universe++import Data.Yoko.CoreTypes+import Data.Yoko.Generic++import Control.Applicative (Applicative(pure))+import Data.Traversable (Traversable(traverse))+++++-- | The @TApp@ type family encodes the type-level functionality of+-- "Type.Yoko.Fun" functions.+type family TApp (fn :: * -> *) t+++++-- | @CMap fn m c@ applies @fn@ to all recursive occurrences (i.e. 'R') in a+-- "Data.Yoko.Core" type @c@ that's mediated by @m@. The domain ('Dom') is @RM+-- m c@ and the range ('Rng') is @RM m (CApp (fn m) c)@. The 'Idiom' is @Idiom+-- (fn m)@.+newtype CMap fn m c = CMap (forall t. fn m t)++type instance Dom (CMap fn m) c = RM m c+type instance Rng (CMap fn m) c = RM m (CApp (fn m) c)+type instance Idiom (CMap fn m) = Idiom (fn m)++-- | @CApp fn c@ applies the type-function @fn@ to all recursive occurrences+-- (i.e. 'R') in the "Data.Yoko.Core" type @c@.+type family CApp (fn :: * -> *) c+type instance CApp fn (D a) = D a+type instance CApp fn (F f c) = F f (CApp fn c)+type instance CApp fn (FF ff c d) = FF ff (CApp fn c) (CApp fn d)+type instance CApp fn (M i c) = M i (CApp fn c)+type instance CApp fn (R t) = R (TApp fn t)+type instance CApp fn U = U+type instance CApp fn V = V++pureDomain :: (Dom fn t ~ Rng fn t) => Domain fn t+pureDomain = AppBy $ \_ -> id++instance D a ::: Domain (CMap fn m) where inhabits = pureDomain+instance (c ::: Domain (CMap fn m), Traversable f+ ) => F f c ::: Domain (CMap fn m) where+ inhabits = AppBy $ \(CMap fn) -> F . fmap (apply (CMap fn)) . unF+instance (c ::: Domain (CMap fn m), d ::: Domain (CMap fn m),+ FunctorTSTSS ff+ ) => FF ff c d ::: Domain (CMap fn m) where+ inhabits = AppBy $ \(CMap fn) -> FF .+ fmapTSTSS (apply (CMap fn)) (apply (CMap fn)) . unFF+instance (c ::: Domain (CMap fn m)) => M i c ::: Domain (CMap fn m) where+ inhabits = AppBy $ \(CMap fn) -> M . apply (CMap fn) . unM+instance (t ::: Domain (fn m), Wrapper (fn m),+ Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)+ ) => R t ::: Domain (CMap fn m) where+ inhabits = AppBy $ \(CMap fn) -> R . apply (fn :: fn m t) . unR+instance U ::: Domain (CMap fn m) where inhabits = pureDomain+instance V ::: Domain (CMap fn m) where inhabits = pureDomain++pureDomainA :: (Dom fn t ~ Rng fn t, Applicative (Idiom fn)) => DomainA fn t+pureDomainA = AppABy $ \_ -> pure++instance Applicative (Idiom (fn m)) => D a ::: DomainA (CMap fn m) where+ inhabits = pureDomainA+instance (c ::: DomainA (CMap fn m), Applicative (Idiom (fn m)),+ Traversable f) => F f c ::: DomainA (CMap fn m) where+ inhabits = AppABy $ \(CMap fn) -> fmap F . traverse (applyA (CMap fn)) . unF+instance (c ::: DomainA (CMap fn m), d ::: DomainA (CMap fn m),+ Applicative (Idiom (fn m)), TraversableTSTSS ff+ ) => FF ff c d ::: DomainA (CMap fn m) where+ inhabits = AppABy $ \(CMap fn) -> fmap FF .+ traverseTSTSS (applyA (CMap fn)) (applyA (CMap fn)) . unFF+instance (c ::: DomainA (CMap fn m), Functor (Idiom (fn m))+ ) => M i c ::: DomainA (CMap fn m) where+ inhabits = AppABy $ \(CMap fn) -> fmap M . applyA (CMap fn) . unM+instance (t ::: DomainA (fn m), Functor (Idiom (fn m)), Wrapper (fn m),+ Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)+ ) => R t ::: DomainA (CMap fn m) where+ inhabits = AppABy $ \(CMap fn) -> fmap R . applyA (fn :: fn m t) . unR+instance Applicative (Idiom (fn m)) => U ::: DomainA (CMap fn m) where+ inhabits = pureDomainA+instance Applicative (Idiom (fn m)) => V ::: DomainA (CMap fn m) where+ inhabits = pureDomainA
+ Type/Yoko/TSTSS.hs view
@@ -0,0 +1,29 @@+{- |++Module : Type.Yoko.TSTSS+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Classes for @* -> * -> *@ types.++-}++module Type.Yoko.TSTSS where++import Control.Applicative++++class FunctorTSTSS ff where+ fmapTSTSS :: (a -> c) -> (b -> d) -> ff a b -> ff c d+instance FunctorTSTSS Either where fmapTSTSS f g = (Left . f) `either` (Right . g)+instance FunctorTSTSS (,) where fmapTSTSS f g ~(x, y) = (f x, g y)++class TraversableTSTSS ff where+ traverseTSTSS :: Applicative i => (a -> i c) -> (b -> i d) -> ff a b -> i (ff c d)+instance TraversableTSTSS Either where traverseTSTSS f g = either (fmap Left . f) (fmap Right . g)+instance TraversableTSTSS (,) where traverseTSTSS f g ~(x, y) = (,) <$> f x <*> g y
+ Type/Yoko/Type.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE TypeFamilies, FlexibleContexts, TypeOperators,+ ScopedTypeVariables, UndecidableInstances, FlexibleInstances #-}++{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, GADTs #-}++{- |++Module : Type.Yoko.Type+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Some fundamental types central to @yoko@.++-}++module Type.Yoko.Type+ (qK, Proxy(Proxy), module Type.Yoko.Type, module Type.Spine.Stage0,+ module Type.Booleans, IsEQ, Compare, EqT(..), (:=:)(..)) where++import Data.Proxy (Proxy(..))++import Type.Spine+import Type.Spine.Stage0 (KS, KTSS)+import Type.Serialize++import Data.Proxy.TH (qProxy)+import Type.Booleans+--import Polarity+import Type.Ord.SpineSerialize (IsEQ, Compare)++import Data.Type.Equality++++qP = qProxy++++-- | The @Med@ type family encodes the behavior of recursion mediators.+type family Med m a+-- | @type instance Med IdM a = a@.+data IdM = IdM; type instance Med IdM a = a+++++-- | The @Wrapper@ class is used to make term-level programming newtypes a+-- little more lightweight from the user perspective.+class Wrapper f where wrap :: Unwrap f a -> f a; unwrap :: f a -> Unwrap f a+type family Unwrap (f :: * -> *) a++++-- | The @Pred@ type family realizes type-level predicates (over types) that+-- yield a type-level Boolean: either 'True' or 'False'. Predicates are often+-- universes.+type family Pred (p :: * -> *) a++type instance Pred ((:=:) a) b = IsEQ (Compare a b)++++++derive n = do+ d <- spineType n+ (d ++) `fmap` serializeTypeAsHash n++++++-- | Composition of @* -> *@ types.+newtype (f :. g) a = Compose (f (g a))+type instance Unwrap (f :. g) a = f (g a)+instance Wrapper (f :. g) where wrap = Compose; unwrap (Compose x) = x++-- | Explicitly takes the inner type as a proxy.+composeWith :: [qProxy|g :: *->*|] -> f (g a) -> (f :. g) a+composeWith _ = Compose
+ Type/Yoko/Universe.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,+ FlexibleContexts, ScopedTypeVariables, FlexibleInstances,+ UndecidableInstances, GADTs, Rank2Types #-}++{- |++Module : Type.Yoko.Universe+Copyright : (c) The University of Kansas 2011+License : BSD3++Maintainer : nicolas.frisby@gmail.com+Stability : experimental+Portability : see LANGUAGE pragmas (... GHC)++Type universes.++-}++module Type.Yoko.Universe where++import Type.Yoko.Type++infix 0 :::+-- | A /universe/ determines a set of types; /open/ or /closed/. @(:::)@ is+-- comparable to the @Sat@ class (e.g. from @SYB3@).+class a ::: u where inhabits :: u a++++-- | @(:?)@ helps us write /guarded/ @(:::)@ instances (see+-- <http://hackage.haskell.org/trac/ghc/ticket/5590>)+infix 1 :?+data (u :? anno) a = Anno (u a)+++-- | For use with @(:::)@ instances that use @(:?)@.+inhabits_ :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a+inhabits_ _ = i where Anno i = inhabits :: (u :? anno) a++-- | Sometimes it's helpful to specify which @t@ must be in the universe.+inhabitsFor :: (t ::: u) => [qP|t|] -> u t+inhabitsFor _ = inhabits++++-- | The universe of all types; it has /no/ contraints.+data NoneD a = NoneD+instance a ::: NoneD where inhabits = NoneD++type Both = (:&&)+infixr 3 :&&+-- | Universe product.+data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstD :: u a, sndD :: v a} -> (u :&& v) a+instance (a ::: u, a ::: v) => a ::: u :&& v where+ inhabits = inhabits :&& inhabits++type instance Pred (p :&& q) a = And (Pred p a) (Pred q a)++++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++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+instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where+ inhabits = Anno $ RightD inhabits+++type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)++++-- | The empty universe.+data VoidU t = VoidU -- the empty universe++++instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits
+ yoko.cabal view
@@ -0,0 +1,107 @@+name: yoko+version: 0.1+synopsis: generic programming with disbanded constructors ++description: @yoko@ views a nominal datatype as a /band/ of constructors, each+ a nominal type in its own right. Such datatypes can be disbanded via the+ @disband@ function into an anonymous sum of nominal constructors, and vice+ versa via the @band@ function. This library uses extensive type-level+ programming to enrich its @instant-generics@ foundation with capabilities+ derived from the constructor-centric perspective.+ .+ For example, consider the following /nominal datatype/.+ .+ @+ data Beatles = John ... | Paul ... | George ... | Ringo ...+ @+ .+ This type can of course be understood as a sum of the individual+ /constructor types/.+ .+ @+ data John = John ...+ data Paul = Paul ...+ data George = George ...+ data Ringo = Ringo ...+ @+ .+ @yoko@'s conceptual foundations start there. In particular, this allows a+ 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+ 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,+ and @Prog@, which has top-level function declarations instead.+ .+ @+ data Inner = Lam Type Inner | Var Int | App Inner Inner+ .+ data Term = Var Int | App Term Term | DVar Int+ data Prog = Prog ([Type], Type, Term) Term+ @+ .+ These types are defined in separate modules, since they have constructors+ with the same name. Indeed, the fact that they having matching constructors+ named @App@ is crucial for @yoko@'s automatic conversion from @Inner@'s @App@+ to @Term@'s @App@. As written, the generic lambda-lifter would continue to+ work for any new @Inner@ constructors (e.g. syntax for tuples or mutable+ references) as long as constructors with the same names and analogous fields+ were added to @Term@ and the semantics of those constructors doesn't involve+ binding. This default behavior of the lambda-lifter is specified in about ten+ lines of user code.+ .+ Existing generic libraries don't use constructor names to the degree that+ @yoko@ does, and so cannot accomodate generic /conversions/ nearly as well.++category: Generics, Reflection++license: BSD3+license-file: LICENSE+author: Nicolas Frisby <nicolas.frisby@gmail.com>+maintainer: Nicolas Frisby <nicolas.frisby@gmail.com>+stability: experimental++build-type: Simple+cabal-version: >= 1.6++extra-source-files: README, Examples/*.hs++++library+ build-depends: base >= 4 && < 5+ build-depends: type-equality < 0.2, tagged >= 0.2 && < 0.3++ build-depends: type-booleans < 0.2, type-spine < 0.2, tagged-th < 0.2,+ type-digits < 0.2, type-cereal < 0.2, type-ord < 0.2, type-ord-spine-cereal+ < 0.2++ exposed-modules: Type.Yoko,+ Type.Yoko.Type,+ Type.Yoko.Universe,+ Type.Yoko.Natural,+ Type.Yoko.Sum,+ Type.Yoko.BTree,+ Type.Yoko.TSTSS,+ Type.Yoko.Fun,+ Type.Yoko.FunA,+ Type.Yoko.MFun,+ Type.Yoko.TFunA,++ Data.Yoko,+ Data.Yoko.Core,+ Data.Yoko.CoreTypes,+ Data.Yoko.Generic,+ Data.Yoko.ReflectBase,+ Data.Yoko.Reflect,+ Data.Yoko.InDT,+ Data.Yoko.Reduce,+ Data.Yoko.Algebra++-- Examples.TermBase,+-- Examples.TermGeneric,+-- Examples.InnerBase,+-- Examples.InnerGeneric,+-- Examples.TermInner