syntactic-0.2: Generic abstract syntax, and utilities for embedded languages

Language.Syntactic.Syntax

Contents

Description

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.

Synopsis

Syntax trees

newtype Full a Source

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) 
Typeable a => Syntactic (ASTF dom a) dom 
(Typeable a, NAry b dom, Typeable (NAryEval b)) => NAry (ASTF dom a -> b) dom 
NAry (ASTF dom a) dom 
(ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) 

newtype a :-> b Source

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

Instances

ConsType' a => ConsType a 

type ConsEval a = ConsEval' aSource

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' aSource

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

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

Make a constructor evaluation from a ConsEval representation

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

Semantic constructor application

data AST dom a whereSource

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 dom => ExprEq (AST dom) 
ToTree dom => ToTree (AST dom) 
Render dom => Render (AST dom) 
Eval dom => Eval (AST dom) 
ExprHash dom => ExprHash (AST dom) 
ExprEq dom => Eq (AST dom a) 
Render dom => Show (AST dom a) 
Typeable a => Syntactic (ASTF dom a) dom 
(Typeable a, NAry b dom, Typeable (NAryEval b)) => NAry (ASTF dom a -> b) dom 
NAry (ASTF dom a) dom 
(ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) 

type ASTF dom a = AST dom (Full a)Source

Fully applied abstract syntax tree

data dom1 :+: dom2 whereSource

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 whereSource

Methods

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

Injection from sub to sup

project :: sup a -> Maybe (sub a)Source

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

Associated Types

type Internal a Source

Methods

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

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

Instances

(Syntactic a dom, Syntactic b dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b) dom 
Typeable a => Syntactic (ASTF dom a) dom 
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c) dom 
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c, d) dom 
(Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Tuple :<: dom, Select :<: 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 :<: dom, Select :<: 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 :<: dom, Select :<: 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.

Methods

desugarN :: a -> internalSource

sugarN :: internal -> aSource

Instances

(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

data family SubTrees dom a Source

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

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