Safe Haskell | None |
---|
Generic representation of typed syntax trees
As a simple demonstration, take the following simple language:
data Expr1 a where Num1 :: Int -> Expr1 Int Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
Using the present library, this can be rewritten as follows:
data Num2 a where Num2 :: Int -> Num2 (Full Int) data Add2 a where Add2 :: Add2 (Int :-> Int :-> Full Int) type Expr2 a = ASTF (Num2 :+: Add2) a
Note that Num2
and Add2
are non-recursive. The only recursive data type
here is AST
, which is provided by the library. Now, the important point is
that Expr1
and Expr2
are completely isomorphic! This is indicated by the
following conversions:
conv12 :: Expr1 a -> Expr2 a conv12 (Num1 n) = inj (Num2 n) conv12 (Add1 a b) = inj Add2 :$ conv12 a :$ conv12 b conv21 :: Expr2 a -> Expr1 a conv21 (prj -> Just (Num2 n)) = Num1 n conv21 ((prj -> Just Add2) :$ a :$ b) = Add1 (conv21 a) (conv21 b)
A key property here is that the patterns in conv21
are actually complete.
So, why should one use Expr2
instead of Expr1
? The answer is that Expr2
can be processed by generic algorithms defined over AST
, for example:
countNodes :: ASTF domain a -> Int countNodes = count where count :: AST domain a -> Int count (Sym _) = 1 count (a :$ b) = count a + count b
Furthermore, although Expr2
was defined to use exactly the constructors
Num2
and Add2
, it is possible to leave the set of constructors open,
leading to more modular and reusable code. This can be seen by relaxing the
types of conv12
and conv21
:
conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a
This way of encoding open data types is taken from Data types à la carte
(Wouter Swierstra, Journal of Functional Programming, 2008). However, we do
not need Swierstra's fixed-point machinery for recursive data types. Instead
we rely on AST
being recursive.
- newtype Full a = Full {
- result :: a
- newtype a :-> b = Partial (a -> b)
- data family Args c a
- data WrapFull c a where
- WrapFull :: {
- unwrapFull :: c a
- WrapFull :: {
- class Signature' a => Signature a
- type Denotation a = Denotation' a
- type DenResult a = DenResult' a
- data ConsWit a where
- class WitnessCons expr where
- witnessCons :: expr a -> ConsWit a
- fromEval :: Signature a => Denotation a -> a
- toEval :: Signature a => a -> Denotation a
- listArgs :: Signature a => (forall a. c (Full a) -> b) -> Args c a -> [b]
- mapArgs :: Signature a => (forall a. c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a
- mapArgsM :: (Monad m, Signature a) => (forall a. c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a)
- appArgs :: Signature a => AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a)
- appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult a
- ($:) :: (a :-> b) -> a -> b
- data AST dom a where
- type ASTF dom a = AST dom (Full a)
- data dom1 :+: dom2 where
- class ApplySym a f dom | a dom -> f, f -> a dom
- appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> f
- appSymCtx :: (ApplySym a f dom, Signature a, sym ctx :<: dom) => Proxy ctx -> sym ctx a -> f
- class sub :<: sup where
- injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup a
- prjCtx :: sub ctx :<: sup => Proxy ctx -> sup a -> Maybe (sub ctx a)
- class Typeable (Internal a) => Syntactic a dom | a -> dom where
- resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b
- class SyntacticN a internal | a -> internal where
- sugarSym :: (Signature a, sym :<: AST dom, ApplySym a b dom, SyntacticN c b) => sym a -> c
- sugarSymCtx :: (Signature a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) => Proxy ctx -> sym ctx a -> c
- queryNode :: forall dom c a. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (Full a)) -> ASTF dom a -> c (Full a)
- queryNodeSimple :: forall dom a c. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c) -> ASTF dom a -> c
- transformNode :: forall dom dom' c a. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (ASTF dom' a)) -> ASTF dom a -> c (ASTF dom' a)
- class Sat ctx a where
- witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a
- data SatWit ctx a where
- fromSatWit :: SatWit ctx a -> Witness ctx a
- class WitnessSat expr where
- type SatContext expr
- witnessSat :: expr a -> SatWit (SatContext expr) (DenResult a)
- class MaybeWitnessSat ctx expr where
- maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (DenResult a))
- maybeWitnessSatDefault :: WitnessSat expr => Proxy (SatContext expr) -> expr a -> Maybe (SatWit (SatContext expr) (DenResult a))
- withContext :: sym ctx a -> Proxy ctx -> sym ctx a
- data Poly
- poly :: Proxy Poly
- data SimpleCtx
- simpleCtx :: Proxy SimpleCtx
Syntax trees
The type of a fully applied constructor
Typeable1 Full | |
Eq a => Eq (Full a) | |
Show a => Show (Full a) | |
Signature' (Full a) | |
ApplySym (Full a) (ASTF dom a) dom | |
Typeable a => Syntactic (ASTF dom a) dom | |
(Syntactic a dom, ~ * ia (Internal a), SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) | |
(Typeable a, ApplySym b f' dom) => ApplySym (:-> a b) (ASTF dom a -> f') dom |
The type of a partially applied (or unapplied) constructor
Partial (a -> b) |
Can be used to turn a type constructor indexed by a
to a type constructor
indexed by (
. This is useful together with Full
a)Args
, which assumes
its constructor to be indexed by (
. That is, use
Full
a)
Args (WrapFull c) ...
instead of
Args c ...
if c
is not indexed by (
.
Full
a)
WrapFull :: c a -> WrapFull c (Full a) | |
|
class Signature' a => Signature a Source
Fully or partially applied constructor
This is a public alias for the hidden class Signature'
. The only instances
are:
instance Signature' (Full a) instance Signature' b => Signature' (a :-> b)
Signature' a => Signature a |
type Denotation a = Denotation' aSource
class WitnessCons expr whereSource
Expressions in syntactic are supposed to have the form
(
. This class lets us witness the Signature
a => expr a)Signature
constraint of an expression without examining the expression.
witnessCons :: expr a -> ConsWit aSource
WitnessCons (Condition ctx) | |
WitnessCons (Construct ctx) | |
WitnessCons (Identity ctx) | |
WitnessCons (Literal ctx) | |
WitnessCons (MONAD m) | |
WitnessCons (Select ctx) | |
WitnessCons (Tuple ctx) | |
WitnessCons (Lambda ctx) | |
WitnessCons (Variable ctx) | |
WitnessCons (Node ctx) | |
(WitnessCons sub1, WitnessCons sub2) => WitnessCons (:+: sub1 sub2) | |
WitnessCons dom => WitnessCons (Decor info dom) | |
WitnessCons (Let ctxa ctxb) | |
WitnessCons (HOLambda ctx dom) |
fromEval :: Signature a => Denotation a -> aSource
Make a constructor evaluation from a Denotation
representation
toEval :: Signature a => a -> Denotation aSource
listArgs :: Signature a => (forall a. c (Full a) -> b) -> Args c a -> [b]Source
Convert a heterogeneous list to a normal list
mapArgs :: Signature a => (forall a. c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 aSource
Change the container of each element in a heterogeneous list
mapArgsM :: (Monad m, Signature a) => (forall a. c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a)Source
Change the container of each element in a heterogeneous list, monadic version
appArgs :: Signature a => AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a)Source
Apply the syntax tree to the listed arguments
appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult aSource
Apply the evaluation function to the listed arguments
Generic abstract syntax tree, parameterized by a symbol domain
In general, (
represents a partially applied (or
unapplied) constructor, missing at least one argument, while
AST
dom (a :->
b))(
represents a fully applied constructor, i.e. a
complete syntax tree.
It is not possible to construct a total value of type AST
dom (Full
a))(
that
does not fulfill the constraint AST
dom a)(
.
Signature
a)
Note that the hidden class Signature'
mentioned in the type of Sym
is
interchangeable with Signature
.
Sym :: Signature' a => dom a -> AST dom a | |
:$ :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b |
MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom) | |
:<: sub sup => sub :<: (AST sup) | |
ExprEq dom => ExprEq (AST dom) | |
ToTree dom => ToTree (AST dom) | |
Render dom => Render (AST dom) | |
Eval dom => Eval (AST dom) | |
ApplySym (Full a) (ASTF dom a) dom | |
ExprEq dom => Eq (AST dom a) | |
Render dom => Show (AST dom a) | |
Typeable a => Syntactic (ASTF dom a) dom | |
(Syntactic a dom, ~ * ia (Internal a), SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) | |
(Typeable a, ApplySym b f' dom) => ApplySym (:-> a b) (ASTF dom a -> f') dom |
data dom1 :+: dom2 whereSource
Co-product of two symbol domains
(MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) => MaybeWitnessSat ctx (:+: sub1 sub2) | |
:<: expr1 expr3 => expr1 :<: (:+: expr2 expr3) | |
expr1 :<: (:+: expr1 expr2) | |
(WitnessCons sub1, WitnessCons sub2) => WitnessCons (:+: sub1 sub2) | |
(ExprEq expr1, ExprEq expr2) => ExprEq (:+: expr1 expr2) | |
(ToTree expr1, ToTree expr2) => ToTree (:+: expr1 expr2) | |
(Render expr1, Render expr2) => Render (:+: expr1 expr2) | |
(Eval expr1, Eval expr2) => Eval (:+: expr1 expr2) | |
(EvalBind sub1, EvalBind sub2) => EvalBind (:+: sub1 sub2) | |
(Optimize sub1 ctx dom, Optimize sub2 ctx dom) => Optimize (:+: sub1 sub2) ctx dom | |
(Syntactic a (HODomain ctx dom), Syntactic b (HODomain ctx dom), Sat ctx (Internal a)) => Syntactic (a -> b) (HODomain ctx dom) | |
(AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq (:+: subA1 subA2) (:+: subB1 subB2) dom env | |
(ExprEq expr1, ExprEq expr2) => Eq (:+: expr1 expr2 a) | |
(Render expr1, Render expr2) => Show (:+: expr1 expr2 a) | |
(:<: (MONAD m) dom, Syntactic a (HODomain ctx dom), Monad m, Typeable1 m, Sat ctx (Internal a)) => Syntactic (Mon ctx dom m a) (HODomain ctx dom) |
class ApplySym a f dom | a dom -> f, f -> a domSource
Class that performs the type-level recursion needed by appSym
appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> fSource
Generic symbol application
appSym
has any type of the form:
appSym :: (expr :<: AST dom, Typeable a, Typeable b, ..., Typeable x) => expr (a :-> b :-> ... :-> Full x) -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)
appSymCtx :: (ApplySym a f dom, Signature a, sym ctx :<: dom) => Proxy ctx -> sym ctx a -> fSource
Generic symbol application with explicit context
Subsumption
injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup aSource
inj
with explicit context
Syntactic sugar
class Typeable (Internal a) => Syntactic a dom | a -> dom whereSource
It is assumed that for all types A
fulfilling (
:
Syntactic
A dom)
eval a == eval (desugar $ (id :: A -> A) $ sugar a)
(using eval
)
resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> bSource
Syntactic type casting
class SyntacticN a internal | a -> internal whereSource
N-ary syntactic functions
desugarN
has any type of the form:
desugarN :: ( Syntactic a dom , Syntactic b dom , ... , Syntactic x dom ) => (a -> b -> ... -> x) -> ( AST dom (Full (Internal a)) -> AST dom (Full (Internal b)) -> ... -> AST dom (Full (Internal x)) )
...and vice versa for sugarN
.
(Syntactic a dom, ~ * ia (AST dom (Full (Internal a)))) => SyntacticN a ia | |
(Syntactic a dom, ~ * ia (Internal a), SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) |
sugarSym :: (Signature a, sym :<: AST dom, ApplySym a b dom, SyntacticN c b) => sym a -> cSource
"Sugared" symbol application
sugarSym
has any type of the form:
sugarSym :: ( expr :<: AST dom , Syntactic a dom , Syntactic b dom , ... , Syntactic x dom ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x)) -> (a -> b -> ... -> x)
sugarSymCtx :: (Signature a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) => Proxy ctx -> sym ctx a -> cSource
"Sugared" symbol application with explicit context
AST processing
queryNode :: forall dom c a. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (Full a)) -> ASTF dom a -> c (Full a)Source
Query an AST
using a function that gets direct access to the top-most
constructor and its sub-trees
Note that, by instantiating the type c
with
, we get the
following type, which shows that AST
dom'queryNode
can be directly used to
transform syntax trees (see also transformNode
):
(forall b . (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> ASTF dom' a) -> ASTF dom a -> ASTF dom' a
queryNodeSimple :: forall dom a c. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c) -> ASTF dom a -> cSource
A simpler version of queryNode
This function can be used to create AST
traversal functions indexed by the
symbol types, for example:
class Count subDomain where count' :: Count domain => subDomain a -> Args (AST domain) a -> Int instance (Count sub1, Count sub2) => Count (sub1 :+: sub2) where count' (InjL a) args = count' a args count' (InjR a) args = count' a args count :: Count dom => ASTF dom a -> Int count = queryNodeSimple count'
Here, count
represents some static analysis on an AST
. Each constructor
in the tree will be queried by count'
indexed by the corresponding symbol
type. That way, count'
can be seen as an open-ended function on an open
data type. The (Count domain)
constraint on count'
is to allow recursion
over sub-trees.
Let's say we have a symbol
data Add a where Add :: Add (Int :-> Int :-> Full Int)
Then the Count
instance for Add
might look as follows:
instance Count Add where count' Add (a :* b :* Nil) = 1 + count a + count b
transformNode :: forall dom dom' c a. (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (ASTF dom' a)) -> ASTF dom a -> c (ASTF dom' a)Source
A version of queryNode
where the result is a transformed syntax tree,
wrapped in a type constructor c
Restricted syntax trees
An abstract representation of a constraint on a
. An instance might look
as follows:
instance MyClass a => Sat MyContext a where data Witness MyContext a = MyClass a => MyWitness witness = MyWitness
This allows us to use (
instead of Sat
MyContext a)(MyClass a)
. The
point with this is that MyContext
can be provided as a parameter, so this
effectively allows us to parameterize on class constraints. Note that the
existential context in the data definition is important. This means that,
given a constraint (
, we can always construct the context
Sat
MyContext a)(MyClass a)
by calling the witness
method (the class instance only
declares the reverse relationship).
This way of parameterizing over type classes was inspired by Restricted Data Types in Haskell (John Hughes, Haskell Workshop, 1999).
fromSatWit :: SatWit ctx a -> Witness ctx aSource
class WitnessSat expr whereSource
Expressions that act as witnesses of their result type
type SatContext expr Source
witnessSat :: expr a -> SatWit (SatContext expr) (DenResult a)Source
WitnessSat (Condition ctx) | |
WitnessSat (Construct ctx) | |
WitnessSat (Identity ctx) | |
WitnessSat (Literal ctx) | |
WitnessSat (Select ctx) | |
WitnessSat (Tuple ctx) | |
WitnessSat (Variable ctx) | |
WitnessSat expr => WitnessSat (Decor info expr) | |
WitnessSat (Let ctxa ctxb) |
class MaybeWitnessSat ctx expr whereSource
Expressions that act as witnesses of their result type
MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom) | |
MaybeWitnessSat ctx1 (Condition ctx2) | |
MaybeWitnessSat ctx (Condition ctx) | |
MaybeWitnessSat ctx1 (Construct ctx2) | |
MaybeWitnessSat ctx (Construct ctx) | |
MaybeWitnessSat ctx1 (Identity ctx2) | |
MaybeWitnessSat ctx (Identity ctx) | |
MaybeWitnessSat ctx1 (Literal ctx2) | |
MaybeWitnessSat ctx (Literal ctx) | |
MaybeWitnessSat ctx (MONAD m) | |
MaybeWitnessSat ctx1 (Select ctx2) | |
MaybeWitnessSat ctx (Select ctx) | |
MaybeWitnessSat ctx1 (Tuple ctx2) | |
MaybeWitnessSat ctx (Tuple ctx) | |
MaybeWitnessSat ctx1 (Lambda ctx2) | |
MaybeWitnessSat ctx1 (Variable ctx2) | |
MaybeWitnessSat ctx (Variable ctx) | |
(MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) => MaybeWitnessSat ctx (:+: sub1 sub2) | |
MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Decor info dom) | |
MaybeWitnessSat ctx (Let ctxa ctxb) | |
MaybeWitnessSat ctxb (Let ctxa ctxb) | |
MaybeWitnessSat ctx1 (HOLambda ctx2 dom) |
maybeWitnessSatDefault :: WitnessSat expr => Proxy (SatContext expr) -> expr a -> Maybe (SatWit (SatContext expr) (DenResult a))Source
Convenient default implementation of maybeWitnessSat
withContext :: sym ctx a -> Proxy ctx -> sym ctx aSource
Type application for constraining the ctx
type of a parameterized symbol