| Copyright | (c) 2020 James Koppel |
|---|---|
| License | BSD3 |
| Safe Haskell | None |
| Language | Haskell2010 |
Cubix.Essentials
Description
This is a beginner-friendly package containing the most common functions and types needed by Cubix programs. It is built as a companion to the Cubix tutorial, though we explain many things in both places.
Guide to using this file
- Strongly recommend: In the top-right corner, click Instances and then collapse all instances.
- This file is excellent for Cubix beginners, as it re-exports the most important functions, often with a simplified type. As you progress, you will want to increasingly use the original versions, rather than the versions from this file.
- Because some definitions are re-exported with simplified types, those definitions conflict with the original Cubix definitions.
Synopsis
- deriveAll :: [Name] -> Q [Dec]
- data Sum (fs :: Signature) (h :: Family) e
- class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature)
- type Term (fs :: Signature) = HFix (Sum fs)
- inject :: forall g (fs :: Signature) l. g :-<: fs => g (Term fs) l -> Term fs l
- class All (c :: k -> Constraint) (fs :: [k])
- caseCxt :: forall cxt (fs :: [Fragment]) (a :: Family) e b. All cxt fs => (forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
- class All HFunctor fs => InjF (fs :: [(Type -> Type) -> Type -> Type]) l l' where
- data Label
- type TermLab (f :: Signature) = AnnTerm Label f
- class HFunctor (h :: (Type -> Type) -> Type -> Type)
- class HFunctor h => HFoldable (h :: (Type -> Type) -> Type -> Type)
- class HFoldable t => HTraversable (t :: (Type -> Type) -> Type -> Type)
- class EqHF (f :: (Type -> Type) -> Type -> Type)
- class EqHF f => OrdHF (f :: (Type -> Type) -> Type -> Type)
- class ShowHF (f :: (Type -> Type) -> Type -> Type)
- project :: forall g (f :: Fragment) h (a :: Type -> Type) l. g :<: f => Cxt h f a l -> Maybe (g (Cxt h f a) l)
- class Monad m => MonadAnnotater a (m :: Type -> Type)
- annotateLabel :: forall (f :: (Type -> Type) -> Type -> Type) (m :: Type -> Type). (HTraversable f, MonadAnnotater Label m) => CxtFunM m f (f :&: Label)
- runConcurrentSupplyLabeler :: MonadIO m => StateT LabelGen m a -> m a
- project' :: forall (f :: Node) (f' :: Family -> Type -> Type) s i. (RemA f f', s :<: f') => HFix f i -> Maybe (s (HFix f) i)
- stripA :: forall (f :: Node) (f' :: Family -> Type -> Type) i. (RemA f f', HFunctor f) => HFix f i -> HFix f' i
- class Functor f => InsertF (f :: Type -> Type) (e :: Type -> Type) where
- class ExtractF (f :: Type -> Type) (e :: Type -> Type) where
- extractF :: e (f l) -> f (e l)
- query :: forall (fs :: [(Type -> Type) -> Type -> Type]) r l. (All HFoldable fs, All HFunctor fs) => (forall i. Term fs i -> r) -> (r -> r -> r) -> Term fs l -> r
- transform :: forall (fs :: [(Type -> Type) -> Type -> Type]) l. All HFunctor fs => (forall i. Term fs i -> Term fs i) -> Term fs l -> Term fs l
- type RewriteM (m :: Type -> Type) (f :: Type -> Type) l = f l -> m (f l)
- (>+>) :: forall (m :: Type -> Type) (f :: Type -> Type). MonadPlus m => GRewriteM m f -> GRewriteM m f -> GRewriteM m f
- alltdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM m (Cxt h f a) -> GRewriteM m (Cxt h f a)
- prunetdR :: forall (m :: Type -> Type) (f :: (Type -> Type) -> Type -> Type) h (a :: Type -> Type). (Monad m, HTraversable f) => GRewriteM (MaybeT m) (Cxt h f a) -> GRewriteM m (Cxt h f a)
- class DynCase (f :: Type -> Type) a
- addFail :: Monad m => TranslateM m f l t -> TranslateM (MaybeT m) f l t
- promoteRF :: forall f l (m :: Type -> Type). (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
- promoteR :: forall f l (m :: Type -> Type). (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM m f
- type MCSig = MCSig
- type MJavaSig = MJavaSig
- type MJSSig = MJSSig
- type MLuaSig = MLuaSig
- type MPythonSig = MPythonSig
- type MCTerm = Term MCSig
- type MJavaTerm = Term MJavaSig
- type MJSTerm = Term MJSSig
- type MLuaTerm = Term MLuaSig
- type MPythonTerm = Term MPythonSig
- type MCTermLab = TermLab MCSig
- type MJavaTermLab = TermLab MJavaSig
- type MJSTermLab = TermLab MJSSig
- type MLuaTermLab = TermLab MLuaSig
- type MPythonTermLab = TermLab MPythonSig
- class ParseFile (fs :: Signature) where
- class Pretty (fs :: Signature) where
- data Cfg (fs :: Signature)
- data CfgNode (fs :: Signature)
- safeLookupCfg :: forall (fs :: Signature). Cfg fs -> Label -> Maybe (CfgNode fs)
- lookupCfg :: forall (fs :: Signature). Cfg fs -> Label -> CfgNode fs
- cfgNodeForTerm :: forall (fs :: Signature) l. Cfg fs -> CfgNodeType -> TermLab fs l -> Maybe (CfgNode fs)
- class (CfgComponent fs (CfgState fs), ConstructCfg fs (CfgState fs) (Sum fs), CfgInitState fs) => CfgBuilder (fs :: Signature)
- makeCfg :: forall (fs :: Signature) l. CfgBuilder fs => TermLab fs l -> Cfg fs
- data ProgInfo (fs :: Signature)
- makeProgInfo :: forall (fs :: Signature) l. (CfgBuilder fs, All HFoldable fs) => TermLab fs l -> ProgInfo fs
- containingCfgNode :: forall (fs :: [(Type -> Type) -> Type -> Type]) l. (All HTraversable fs, All HFoldable fs, All HFunctor fs) => ProgInfo fs -> TermLab fs l -> Maybe (E (TermLab fs))
- withContainingCfgNode :: forall (fs :: [(Type -> Type) -> Type -> Type]) m l. (All HTraversable fs, All HFoldable fs, All HFunctor fs, Applicative m) => ProgInfo fs -> TermLab fs l -> (forall i. TermLab fs i -> m ()) -> m ()
- class InsertAt (gs :: Signature) l
- class Monad m => MonadCfgInsertion (m :: Type -> Type) (fs :: Signature) l where
- dominatingPrependFirst :: TermLab fs i -> TermLab fs l -> m ()
- type CfgInserterT (fs :: Signature) l (m :: Type -> Type) = WriterT [Action fs l] m
- performCfgInsertions :: forall l (fs :: Signature) m i. (MonadAnnotater Label m, InsertAt fs l, All HTraversable fs, All HFunctor fs, All HFoldable fs) => ProgInfo fs -> RewriteM (CfgInserterT fs l m) (TermLab fs) i -> RewriteM m (TermLab fs) i
Core representation
Language fragments
The first concept is that of a language fragment and signature. Language fragments in Cubix look like this:
data ExpL data StatementL data Statement e l where Assign :: String -> e ExpL -> Statement e StatementL Seq :: e StatementL -> e StatementL -> Statement e StatementL
This definition of Statement is called a *language fragment*. It defines
the nodes Assign and Seq without any reference to the larger language
they are embedded in. The *labels* StatementL and ExpL are *sorts*, categories of terms.
Popular languages commonly have a sort for top-level definitions, a sort for lvalues, a sort for
import statements, etc. Specifying the sort separately from the language fragment makes it possible
to modularly add new statements and expressions to a language definition, which we will demonstrate shortly.
Expect to see the kind (* -> *) -> * -> * a lot, the kind of language fragments.
When you define a normal datatype (kind *) in Haskell, you might suffix it with
deriving (Eq, Ord, Show). The equivalent for these higher-kinded language fragments is
to derive their higher-kinded equivalents using the deriveAll Template Haskell function, e.g.:
deriveAll [''Statement]
deriveAll :: [Name] -> Q [Dec] Source #
Derives instances of the following for each type in the list:
HFunctor,HTraversable,HFoldable,EqHF,ShowHF,OrdHF,DynCase
Additonally, it will create smart constructors for the data type
Signatures: Combining fragments
Language fragments let one define nodes independent of a larger language. We shall soon
show how to combine them into a **signature**. But first, let us define two more
language fragments, Conditional and Exp.
data Conditional e l where If :: e ExpL -> e StatementL -> e StatementL -> Conditional e StatementL data Exp e l where VarExp :: String -> Exp e ExpL Add :: e ExpL -> e ExpL -> Exp e ExpL -- other cases omitted
As a preview, note how Conditional defines a new node If of sort Statement. When these fragments are
combined into a language, the If node will be able to be included under a Seq node, just as easily
as if was defined in the Statement fragment.
A *signature* is a collection of language fragments. They take the form of a type-level list.
Here is a signature for a language containing all the nodes in the Statement, Conditional, and Exp
fragments.
type LangSig = '[Statement, Conditional, Exp]
Signatures have the kind [(* -> *) -> * -> *], another kind you'll encounter frequently.
Signatures are used by passing them to the Sum constructor, e.g.:
Sum LangSig
Sum LangSig has kind (* -> *) -> * -> *, the same kind as language fragments. It is
conceptually a single language fragment consisting of the combined nodes of Statement, Conditional,
and Exp. It could even be placed in another language signature, and nested within another Sum,
although this use case is not supported.
The Sum constructor is important to Cubix, but you may not use it directly.
More often, you'll use something like Term LangSig --- but note that Term is defined using
Sum.
Signatures also appear with the (:-<:) "signature membership" constraint
For the LangSig definition above, the constraints (Statement :-<: LangSig),
(Conditional :-<: LangSig), and (Exp :-<: LangSig) all hold. In some type signatures,
you'll also see the sibling constraint f :-<: fs(:<:): If , then f :<: (Sum fs). This
makes it possible to write functions that run on any language that have a certain kind of node.
E.g.: (Statement :-fs) = Term fs l -> Term fs l is a rewrite on terms of any
language that has the Statement language fragment.
data Sum (fs :: Signature) (h :: Family) e Source #
Data type defining a sum of signatures.
It is inspired by modular reifiable matching, as described in
- Oliveira, Bruno C. D. S., Shin-Cheng Mu, and Shu-Hung You. "Modular reifiable matching: a list-of-functors approach to two-level types." In Haskell Symposium, 2015.
except that this definition uses value-level integers (in the Elem datatype) in place
of type-level naturals. It hence uses unsafeCoerce under the hood, but is type-safe if used
through the public API. The result is that values of this type take constant memory with respect to the number
of summands (unlike vanilla datatypes à la carte), and constant time to dereference
(unlike modular reifiable matching). The representation is the bare minimum: an int representing the alternative,
and pointer to the value.
Instances
class f :<: Sum fs => (f :: Fragment) :-<: (fs :: Signature) Source #
Instances
| f :<: Sum fs => f :-<: fs | |
Defined in Data.Comp.Multi.Ops | |
Terms
Signatures define nodes of a language, but are agnostic to what the children of those nodes can be. Terms are what "tye the recursive knot" and turn a signature into the final type for a language. They do this by taking a signature, and specifying what the children of each node may be: other nodes from the same signature.
In the slides for the accompanying tutorial, we give a decent pictoral explanation of this topic. Here's a textual version:
It is easier to first present the type-level fixpoint for single-sorted terms. This is the classic example
data ListF e a = ConsF a e | NilF data Fix f = Fix (f (Fix f)) type List = Fix ListF
The ListF type was constructed by taking the normal recursive list type,
and replacing the sublist in Cons with a type parameter, e. This
is called "unfixing" the type. Taking Fix ListF undoes this;
the result is isomorphic to the built-in list type ([]).
Since Cubix terms have different sorts, Cubix uses a generalization
of the Fix constructor. Cubix's definition is equivalent to the following:
data Term fs l = Term (Sum fs (Term fs) l)
This recursively defines Term fs to be
terms of signature fs. It can be thought of as a product
of the types for terms of each sort, so that, for each sort l,
Term fs l is the type of terms of signature fs of sort l.
For example, since MJavaSig is Cubix's signature for Java,
Term MJavaSig denotes all terms in Java, and Term MJavaSig StmtL
denotes Java statements.
Breaking down the definition: Sum fs e l denotes nodes drawn from
any of the language fragments in signature fs, where the children of those
nodes are given by e, and the top node has sort l. Here, e is set to Term fs,
meaning the children are other terms of this signature. These children have their
own sorts. l is then the sort of the root node.
cubix-compdata has a generalization of Term for terms-with-holes, called contexts.
That is outside the scope of this document (see the original "Compositional Data Types"
paper), but, know that, if you see the type Cxt h f a l, it specializes to Term fs l.
Smart constructors
Consider the following language definition:
data ExpL
data StatementL
data Statement e l where
Assign :: String -> e ExpL -> Statement e StatementL
Seq :: e StatementL -> e StatementL -> Statement e StatementL
data Exp e l where
VarExp :: String -> Exp e ExpL
Add :: e ExpL -> e ExpL -> Exp e ExpL
deriveAll [''Statement, ''Exp]
type LangSig = '[Statement, Exp]
type Lang = Term LangSig
Using the raw constructors, here is how one would construct the tem
y = x+x . (n.b.: inj creates values of a Sum type.)
Term $ inj $ Assign "y" $ Term (inj (Add (Term (inj (VarExp "x"))) (Term (inj (VarExp "x")))))
This is obviously quite cumbersome. Towards that end, deriveAll creates smart constructors.
Smart constructors look like this:
iAssign :: (Statement :-fs) = String -> Term fs ExpL -> Term fs StatementL
(Simplified here. The tutorial explains their real types.)
With smart constructors, that term would be constructed like this:
iAssign "y" (iAdd (iVarExp "x) (iVarExp "x"))
Dealing with sums
class All (c :: k -> Constraint) (fs :: [k]) Source #
An instance of All c fs holds if c f holds for all f in fs.
Example: All holds if there are HFunctor '[Add, Mul]HFunctor instances for signatures
Add and Mul.
The primary way to consume an All instance is with the caseCxt function. E.g.:
class Pretty f where pretty :: f e l -> String instance (All Pretty fs) => Pretty (Sum fs) where pretty x = caseCxt @Pretty pretty x
Minimal complete definition
dicts
Instances
| All (c :: k -> Constraint) ('[] :: [k]) | |
Defined in Data.Comp.Dict | |
| (All c fs, c f) => All (c :: a -> Constraint) (f ': fs :: [a]) | |
Defined in Data.Comp.Dict | |
caseCxt :: forall cxt (fs :: [Fragment]) (a :: Family) e b. All cxt fs => (forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b Source #
For full documentaton, see original declaration: caseCxt
Higher topics involving sums/tems
Sort injections
class All HFunctor fs => InjF (fs :: [(Type -> Type) -> Type -> Type]) l l' where Source #
InjF allows us to create "sort injections," stating that one sort can be considered a coercive subsort of another..
For example, if we wanted to parameterize whether a given syntax allows arbitrary expressions to be used as function arguments, we could have the function terms have arguments of sort FunArg and create an ExpressionIsFunArg . Defining an instance
instance (ExpressionIsFunArg :-<: f) => InjF fs ExpL FunArgL
would then allow us to use expression as function arguments freely.
Methods
injF :: forall h (a :: Type -> Type). CxtS h fs a l -> CxtS h fs a l' Source #
projF :: forall h (a :: Type -> Type). CxtS h fs a l' -> Maybe (CxtS h fs a l) Source #
Instances
Labeled nodes
Provides unique labels for AST nodes
Instances
| Data Label Source # | |||||
Defined in Cubix.Language.Info Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Label -> c Label # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Label # dataTypeOf :: Label -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Label) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Label) # gmapT :: (forall b. Data b => b -> b) -> Label -> Label # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Label -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Label -> r # gmapQ :: (forall d. Data d => d -> u) -> Label -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Label -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Label -> m Label # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Label -> m Label # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Label -> m Label # | |||||
| Generic Label Source # | |||||
Defined in Cubix.Language.Info Associated Types
| |||||
| Read Label Source # | |||||
| Show Label Source # | |||||
| HasLabel Label Source # | |||||
| NFData Label Source # | |||||
Defined in Cubix.Language.Info | |||||
| Eq Label Source # | |||||
| Ord Label Source # | |||||
| ToJSON Label Source # | |||||
Defined in Cubix.Language.Info Methods toEncoding :: Label -> Encoding toJSONList :: [Label] -> Value toEncodingList :: [Label] -> Encoding | |||||
| (Monad m, HasLabelGen s) => MonadAnnotater Label (StateT s m) Source # | |||||
| type Rep Label Source # | |||||
Defined in Cubix.Language.Info | |||||
Common typeclassess
These are analogues of standard typeclasses, but for sorted unfixed datatypes.
You are unlikely to use methods in these classes directly, but
you may frequently invoke functions that require them. You may
wind up writing many constraints that use these, likely combined with the All
constructor.
class HFunctor (h :: (Type -> Type) -> Type -> Type) Source #
This class represents higher-order functors (Johann, Ghani, POPL '08) which are endofunctors on the category of endofunctors.
Minimal complete definition
Instances
class HFunctor h => HFoldable (h :: (Type -> Type) -> Type -> Type) Source #
Instances
class HFoldable t => HTraversable (t :: (Type -> Type) -> Type -> Type) Source #