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) = inject (Num2 n) conv12 (Add1 a b) = inject Add2 :$: conv12 a :$: conv12 b conv21 :: Expr2 a -> Expr1 a conv21 (project -> Just (Num2 n)) = Num1 n conv21 ((project -> 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 (Symbol _) = 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 HList c a
- class ConsType' a => ConsType a
- type ConsEval a = ConsEval' a
- type EvalResult a = EvalResult' a
- data ConsWit a where
- class WitnessCons expr where
- witnessCons :: expr a -> ConsWit a
- fromEval :: ConsType a => ConsEval a -> a
- toEval :: ConsType a => a -> ConsEval a
- listHList :: ConsType a => (forall a. c (Full a) -> b) -> HList c a -> [b]
- listHListM :: (Monad m, ConsType a) => (forall a. c (Full a) -> m b) -> HList c a -> m [b]
- mapHList :: ConsType a => (forall a. c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a
- appHList :: ConsType a => AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)
- ($:) :: (a :-> b) -> a -> b
- data AST dom a where
- type ASTF dom a = AST dom (Full a)
- data dom1 :+: dom2 where
- class sub :<: sup where
- 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
- queryNodeI :: forall dom a b. (forall a. ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a)) -> ASTF dom a -> b a
- queryNode :: forall dom a b. (forall a. ConsType a => dom a -> HList (AST dom) a -> b) -> ASTF dom a -> b
- transformNode :: forall dom dom' a. (forall a. ConsType a => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)) -> ASTF dom a -> ASTF dom' a
- class Sat ctx a where
- data Witness' ctx a where
- witness' :: Witness' ctx a -> Witness ctx a
- class WitnessSat sym where
- type Context sym
- witnessSat :: sym a -> Witness' (Context sym) (EvalResult a)
- withContext :: sym ctx a -> Proxy ctx -> sym ctx a
- data Poly
- poly :: Proxy Poly
Syntax trees
The type of a fully applied constructor
Typeable1 Full | |
(Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => NAry ctx (ASTF dom a -> b) dom | |
Sat ctx a => NAry ctx (ASTF dom a) dom | |
Eq a => Eq (Full a) | |
Show a => Show (Full a) | |
ConsType' (Full a) | |
Typeable a => Syntactic (ASTF dom a) dom | |
(ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) |
The type of a partially applied (or unapplied) constructor
Partial (a -> b) |
class ConsType' a => ConsType a Source
Fully or partially applied constructor
This is a public alias for the hidden class ConsType'
. The only instances
are:
instance ConsType' (Full a) instance ConsType' b => ConsType' (a :-> b)
ConsType' a => ConsType a |
type EvalResult a = EvalResult' aSource
class WitnessCons expr whereSource
Expressions in syntactic are supposed to have the form
(
. This class lets us witness the ConsType
a => expr a)ConsType
constraint of an expression without examining the expression.
witnessCons :: expr a -> ConsWit aSource
WitnessCons Sym | |
WitnessCons (Literal ctx) | |
WitnessCons (Condition ctx) | |
WitnessCons (Select ctx) | |
WitnessCons (Tuple ctx) | |
WitnessCons (Lambda ctx) | |
WitnessCons (Variable ctx) | |
WitnessCons (Node ctx) | |
WitnessCons (Let ctxa ctxb) | |
WitnessCons (HOLambda ctx dom) |
fromEval :: ConsType a => ConsEval a -> aSource
Make a constructor evaluation from a ConsEval
representation
listHList :: ConsType a => (forall a. c (Full a) -> b) -> HList c a -> [b]Source
Convert a heterogeneous list to a normal list
listHListM :: (Monad m, ConsType a) => (forall a. c (Full a) -> m b) -> HList c a -> m [b]Source
Convert a heterogeneous list to a normal list
mapHList :: ConsType a => (forall a. c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 aSource
Change the container of each element in a heterogeneous list
appHList :: ConsType a => AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)Source
Apply the syntax tree to 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)(
.
ConsType
a)
Note that the hidden class ConsType'
mentioned in the type of Symbol
is
interchangeable with ConsType
.
Symbol :: ConsType' a => dom a -> AST dom a | |
:$: :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b |
sub :<: sup => sub :<: (AST sup) | |
(Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => NAry ctx (ASTF dom a -> b) dom | |
Sat ctx a => NAry ctx (ASTF dom a) dom | |
ExprEq dom => ExprEq (AST dom) | |
ToTree dom => ToTree (AST dom) | |
Render dom => Render (AST dom) | |
Eval dom => Eval (AST dom) | |
ExprEq dom => Eq (AST dom a) | |
Render dom => Show (AST dom a) | |
Typeable a => Syntactic (ASTF dom a) dom | |
(ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) |
data dom1 :+: dom2 whereSource
Co-product of two symbol domains
expr1 :<: expr3 => expr1 :<: (:+: expr2 expr3) | |
expr1 :<: (:+: expr1 expr2) | |
(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) | |
(ExprEq expr1, ExprEq expr2) => Eq (:+: expr1 expr2 a) | |
(Render expr1, Render expr2) => Show (:+: expr1 expr2 a) |
Subsumption
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 Language.Syntactic.Analysis.Evaluation.eval
)
(Syntactic a dom, Syntactic b dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b) dom | |
Typeable a => Syntactic (ASTF dom a) dom | |
(Syntactic a dom, Syntactic b dom, Syntactic c dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b, c) dom | |
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b, c, d) dom | |
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b, c, d, e) dom | |
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b, c, d, e, f) dom | |
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, (Tuple Poly) :<: dom, (Select Poly) :<: dom) => Syntactic (a, b, c, d, e, f, g) dom |
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
.
(ia ~ AST dom (Full (Internal a)), Syntactic a dom) => SyntacticN a ia | |
(ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) |
AST processing
queryNodeI :: forall dom a b. (forall a. ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a)) -> ASTF dom a -> b aSource
Like queryNode
but with the result indexed by the constructor's result
type
queryNode :: forall dom a b. (forall a. ConsType a => dom a -> HList (AST dom) a -> b) -> ASTF dom a -> bSource
Query an AST
using a function that gets direct access to the top-most
constructor and its sub-trees
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 -> HList (AST domain) a -> Int instance (Count sub1, Count sub2) => Count (sub1 :+: sub2) where count' (InjectL a) args = count' a args count' (InjectR a) args = count' a args count :: Count dom => ASTF dom a -> Int count = queryNode 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' a. (forall a. ConsType a => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)) -> ASTF dom a -> ASTF dom' aSource
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).
class WitnessSat sym whereSource
Symbols that act as witnesses of their result type
witnessSat :: sym a -> Witness' (Context sym) (EvalResult a)Source
WitnessSat (Literal ctx) | |
WitnessSat (Condition ctx) | |
WitnessSat (Select ctx) | |
WitnessSat (Tuple ctx) | |
WitnessSat (Variable ctx) | |
WitnessSat (Let ctxa ctxb) |
withContext :: sym ctx a -> Proxy ctx -> sym ctx aSource
Type application for constraining the ctx
type of a parameterized symbol