Language.Syntactic.Syntax

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.

Syntax trees

newtype Full a

The type of a fully applied constructor

Constructors

Full

Fields

result :: a

Instances

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

newtype a :-> b

The type of a partially applied (or unapplied) constructor

Constructors

Partial (a -> b)

Instances

Typeable2 :->

Signature' b => Signature' (:-> a b)

(Typeable a, ApplySym b f' dom) => ApplySym (:-> a b) (ASTF dom a -> f') dom

data family Args c a

Heterogeneous list, indexed by a container type and a Signature

data WrapFull c a where

Can be used to turn a type constructor indexed by a to a type constructor indexed by (Full a). This is useful together with Args, which assumes its constructor to be indexed by (Full a). That is, use

 Args (WrapFull c) ...

instead of

 Args c ...

if c is not indexed by (Full a).

Constructors

WrapFull :: c a -> WrapFull c (Full a)

Fields

unwrapFull :: c a

class Signature' a => Signature a

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)

Instances

Signature' a => Signature a

type Denotation a = Denotation' a

Maps a Signature to a simpler form where :-> has been replaced by ->, and Full has been removed. This is a public alias for the hidden type Denotation'.

type DenResult a = DenResult' a

Returns the result type (Full removed) of a Signature. This is a public alias for the hidden type DenResult'.

data ConsWit a where

A witness of (Signature a)

Constructors

ConsWit :: Signature a => ConsWit a

class WitnessCons expr where

Expressions in syntactic are supposed to have the form (Signature a => expr a). This class lets us witness the Signature constraint of an expression without examining the expression.

Methods

witnessCons :: expr a -> ConsWit a

Instances

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 -> a

Make a constructor evaluation from a Denotation representation

toEval :: Signature a => a -> Denotation a

listArgs :: Signature a => (forall a. c (Full a) -> b) -> Args c a -> [b]

Convert a heterogeneous list to a normal list

mapArgs :: Signature a => (forall a. c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a

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)

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)

Apply the syntax tree to the listed arguments

appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult a

Apply the evaluation function to the listed arguments

($:) :: (a :-> b) -> a -> b

Semantic constructor application

data AST dom a where

Generic abstract syntax tree, parameterized by a symbol domain

In general, (AST dom (a :-> b)) represents a partially applied (or unapplied) constructor, missing at least one argument, while (AST dom (Full a)) represents a fully applied constructor, i.e. a complete syntax tree. It is not possible to construct a total value of type (AST dom a) that does not fulfill the constraint (Signature a).

Note that the hidden class Signature' mentioned in the type of Sym is interchangeable with Signature.

Constructors

Sym :: Signature' a => dom a -> AST dom a

:$ :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b

Instances

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

type ASTF dom a = AST dom (Full a)

Fully applied abstract syntax tree

data dom1 :+: dom2 where

Co-product of two symbol domains

Constructors

InjL :: dom1 a -> (dom1 :+: dom2) a

InjR :: dom2 a -> (dom1 :+: dom2) a

Instances

(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 dom

Class that performs the type-level recursion needed by appSym

Instances

ApplySym (Full a) (ASTF dom a) dom

(Typeable a, ApplySym b f' dom) => ApplySym (:-> a b) (ASTF dom a -> f') dom

appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> f

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 -> f

Generic symbol application with explicit context

Subsumption

class sub :<: sup where

Methods

inj :: Signature a => sub a -> sup a

Injection from sub to sup

prj :: sup a -> Maybe (sub a)

Partial projection from sup to sub

Instances

expr :<: expr

:<: sub sup => sub :<: (AST sup)

:<: expr1 expr3 => expr1 :<: (:+: expr2 expr3)

expr1 :<: (:+: expr1 expr2)

injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup a

inj with explicit context

prjCtx :: sub ctx :<: sup => Proxy ctx -> sup a -> Maybe (sub ctx a)

prj with explicit context

Syntactic sugar

class Typeable (Internal a) => Syntactic a dom | a -> dom where

It is assumed that for all types A fulfilling (Syntactic A dom):

 eval a == eval (desugar $ (id :: A -> A) $ sugar a)

(using eval)

Associated Types

type Internal a

Methods

desugar :: a -> ASTF dom (Internal a)

sugar :: ASTF dom (Internal a) -> a

Instances

(Syntactic a dom, Syntactic b dom, :<: (Tuple Poly) dom, :<: (Select Poly) dom) => Syntactic (a, b) dom

(Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) dom) => Syntactic (a, b) dom

Typeable a => Syntactic (ASTF dom a) dom

(Syntactic a (HODomain ctx dom), Syntactic b (HODomain ctx dom), Sat ctx (Internal a)) => Syntactic (a -> b) (HODomain ctx dom)

(Syntactic a dom, Syntactic b dom, Syntactic c dom, :<: (Tuple Poly) dom, :<: (Select Poly) dom) => Syntactic (a, b, c) dom

(Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) 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, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) dom) => Syntactic (a, b, c, d) dom

(:<: (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)

(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, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) 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, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), Syntactic f dom, Eq (Internal f), Show (Internal f), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) 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

(Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), Syntactic f dom, Eq (Internal f), Show (Internal f), Syntactic g dom, Eq (Internal g), Show (Internal g), :<: (Tuple SimpleCtx) dom, :<: (Select SimpleCtx) dom) => Syntactic (a, b, c, d, e, f, g) dom

resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b

Syntactic type casting

class SyntacticN a internal | a -> internal where

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.

Methods

desugarN :: a -> internal

sugarN :: internal -> a

Instances

(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 -> c

"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 -> c

"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)

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 AST dom', we get the following type, which shows that 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 -> c

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)

A version of queryNode where the result is a transformed syntax tree, wrapped in a type constructor c

Restricted syntax trees

class Sat ctx a where

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 (Sat MyContext a) instead of (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 (Sat MyContext a), we can always construct the context (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).

Associated Types

data Witness ctx a

Methods

witness :: Witness ctx a

Instances

(Eq a, Show a, Typeable a) => Sat SimpleCtx a

Sat Poly a

witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a

data SatWit ctx a where

Witness of a (Sat ctx a) constraint. This is different from (Witness ctx a), which witnesses the class encoded by ctx. Witness' has a single constructor for all contexts, while Witness has different constructors for different contexts.

Constructors

SatWit :: Sat ctx a => SatWit ctx a

fromSatWit :: SatWit ctx a -> Witness ctx a

class WitnessSat expr where

Expressions that act as witnesses of their result type

Associated Types

type SatContext expr

Methods

witnessSat :: expr a -> SatWit (SatContext expr) (DenResult a)

Instances

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 where

Expressions that act as witnesses of their result type

Methods

maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (DenResult a))

Instances

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))

Convenient default implementation of maybeWitnessSat

withContext :: sym ctx a -> Proxy ctx -> sym ctx a

Type application for constraining the ctx type of a parameterized symbol

data Poly

Representation of a fully polymorphic constraint -- i.e. (Sat Poly a) is satisfied by all types a.

Instances

Sat Poly a

poly :: Proxy Poly

data SimpleCtx

Representation of "simple" types: types satisfying (Eq a, Show a, Typeable a)

Instances

(Eq a, Show a, Typeable a) => Sat SimpleCtx a

simpleCtx :: Proxy SimpleCtx