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

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

newtype a :-> b

The type of a partially applied (or unapplied) constructor

Constructors

Partial (a -> b)

Instances

Typeable2 :->

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

data family HList c a

Heterogeneous list, indexed by a container type and a ConsType

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

data ConsWit a where

A witness of (ConsType a)

Constructors

ConsWit :: ConsType a => ConsWit a

class WitnessCons expr where

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

Methods

witnessCons :: expr a -> ConsWit a

Instances

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

Make a constructor evaluation from a ConsEval representation

toEval :: ConsType a => a -> ConsEval a

listHList :: ConsType a => (forall a. c (Full a) -> b) -> HList c a -> [b]

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]

Convert a heterogeneous list to a normal list

mapHList :: ConsType a => (forall a. c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a

Change the container of each element in a heterogeneous list

appHList :: ConsType a => AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)

Apply the syntax tree to 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 (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)

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

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)

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

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

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

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

Transform an AST using a function that gets direct access to the top-most constructor and its sub-trees. This function is similar to queryNode, but returns a transformed AST rather than abstract interpretation.

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

Sat Poly a

data Witness' 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

Witness' :: Sat ctx a => Witness' ctx a

witness' :: Witness' ctx a -> Witness ctx a

class WitnessSat sym where

Symbols that act as witnesses of their result type

Associated Types

type Context sym

Methods

witnessSat :: sym a -> Witness' (Context sym) (EvalResult a)

Instances

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