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)   = 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 a la carte, by Wouter Swierstra, in 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)

ConsType' (Full a)

(NAryDom b ~ dom, Typeable a, NAry b, Typeable (NAryEval b)) => NAry (AST dom (Full a) -> b)

NAry (AST dom (Full a))

Typeable a => Syntactic (ASTF dom a) dom

newtype a :-> b

The type of a partially applied (or unapplied) constructor

Constructors

Partial (a -> b)

Instances

Typeable2 :->

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

class ConsType' a => ConsType a

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)

Instances

ConsType' a => ConsType a

type ConsEval a = ConsEval' a

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

type EvalResult a = EvalResult' a

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

consEval :: ConsType a => ConsEval a -> a

Make a constructor evaluation from a ConsEval representation

($:) :: (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 (ConsType a).

Note that the hidden class ConsType' mentioned in the type of Symbol is interchangeable with ConsType.

Constructors

Symbol :: ConsType' a => dom a -> AST dom a

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

Instances

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

ExprEq expr => ExprEq (AST expr)

ToTree dom => ToTree (AST dom)

Render expr => Render (AST expr)

Eval expr => Eval (AST expr)

ExprHash expr => ExprHash (AST expr)

ExprEq expr => Eq (AST expr a)

Render expr => Show (AST expr a)

(NAryDom b ~ dom, Typeable a, NAry b, Typeable (NAryEval b)) => NAry (AST dom (Full a) -> b)

NAry (AST dom (Full a))

Typeable a => Syntactic (ASTF dom a) 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

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

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

Instances

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)

(ExprHash expr1, ExprHash expr2) => ExprHash (:+: expr1 expr2)

(ExprEq expr1, ExprEq expr2) => Eq (:+: expr1 expr2 a)

(Render expr1, Render expr2) => Show (:+: expr1 expr2 a)

Subsumption

class sub :<: sup where

Methods

inject :: ConsType a => sub a -> sup a

Injection from sub to sup

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

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 Language.Syntactic.Analysis.Evaluation.eval)

Associated Types

type Internal a

Methods

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

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

Instances

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

Typeable a => Syntactic (ASTF dom a) dom

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

(Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d) expr

(Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e) expr

(Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Syntactic f expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e, f) expr

(Syntactic a expr, Syntactic b expr, Syntactic c expr, Syntactic d expr, Syntactic e expr, Syntactic f expr, Syntactic g expr, Tuple :<: expr, Select :<: expr) => Syntactic (a, b, c, d, e, f, g) expr

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

Syntactic type casting

AST processing

data family SubTrees dom a

Data family for collecting the children of a constructor, for example:

 subTrees :: forall dom . SubTrees dom (Int :-> Bool :-> Full [Int])
 subTrees = a :*: b :*: Nil
   where
     a = undefined :: ASTF dom Int
     b = undefined :: ASTF dom Bool

(SubTrees a) is meaningful iff. (ConsType a)

processNode :: forall dom a b. (forall a. ConsType a => dom a -> SubTrees dom a -> b) -> ASTF dom a -> b

Process 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 -> SubTrees 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 = processNode count'

Here, count represents some static analysis on an AST. Each constructor in the tree will be processed 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