% LambdaCube 3D compiler developer's documentation and ideas

Introduction
============

The documentation is written on demand.
If you are interested in an undocumented feature, please open an issue with a short message like
"Documentation on ... is missing."


Compiler structure overview
==================

Main tasks of the compiler:

-   find errors in source code
-   code completion to avoid superfluous parts of source code
-   eliminate abstractions

Additional tasks of the compiler:

-   support modular development
    -   modules support
-   support livecoding
    -   highlight errors
    -   show inferred types in tooltips
    -   code completion during editing
-   additional feedback for programmers
    -   show desugared source
    -   show optimizations

Main design decisions

-   reuse Haskell syntax & semantics
    -   semantics errors are ruled out by strong static typing
    -   code completion is done by type classes
    -   abstractions are eliminated by reduction
-   Code generation is not part of the compiler; it is done during the reduction of the main expression.  
    This helps to keep the compiler smaller, and separate domain specific code from the compiler.
-   The compiler has just two phases:
    1.  lexing + parsing + scope checking + desugaring
    2.  type checking + type inference + normalization


Example: Compilation and reduction of a simple value
----------------------------------------------------

      |
      | source code
      | (e.g. description of the 100th prime number)
      v
    lexing + parsing + scope checking + desugaring
      |                             |
      | desugared source code       \--> halt with error message
      v
    inference + normalization   -------> halt with error message
      ||
      ||  infos (e.g. inferred types)
      |\------------------------------->
      |
      | normalized value
      | (e.g. 547, the 100th prime number)
      |
      v


Code generation by reduction
----------------------------

The interface between the compiler and the code generator is the builtin `Expression` type.  
The compilation is done in multiple phases:

1.  The code generator is in a library; it is parsed and normalized by the compiler.
2.  The application code is normalized by the compiler and it is given to the code generator as an `Expression` value.

Additinional design decisions:

-   include pattern synonyms which can match different normal forms of `Expression`  
    This eases the description of code generation.
-   Ideally no error handling is needed during code generation; all misues should be found during the type checking of application code.
-   track compilation stages by the type system [(reference)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.4374)
    -   prevents even more misuses
    -   helps to speed up compilation (?)
-   include optimizing transformations of `Expression` in the libraries


### Example: Compilation of domain specific code in two phases

Builtin library:

~~~~~ {.haskell}
-- definition of elaborated expressions
data Expr a = ...

-- primitive function for reflection
reflect :: a -> Expr a  -- TODO: encode phase info in type

-- pattern synonyms for matching different normal forms of `Expr`
...
~~~~~

DSL compiler code:

~~~~~ {.haskell}
-- definition of main type of the DSL
-- (this is a custom DSL IO type)
data IO a = ...

-- definition of target code type (e.g. ByteString)
data Target = ...

-- DSL compiler, including optimizations
compile :: Expr (IO ()) -> Target
...
~~~~~

Application code:

~~~~~ {.haskell}
-- DSL main entry point
dslMain :: IO ()
dslMain = ...

-- compiled main
main :: Target
main = compile (reflect dslMain)
~~~~~

Compilation flowchart:

          |
          | DSL compiler code
          v
        lexing + parsing + scope checking + desugaring
        & inference + normalization ------> halt with error message (phase #1)
          |
          | 'compile' ready to be applied
          |
      /---/
      |
      |   |
      |   | application code
      |   v
      | lexing + parsing + scope checking + desugaring
      | & inference + normalization ------> halt with error message (phase #2)
      |   |
      |   | normalized 'dslMain'
      |   v
      | reflection
      |   |
      |   | normalized 'reflect dslMain'
      |   | (value of type 'Expr (IO ())')
      v   v
    function application & normalization
      |
      | normalized 'compile (reflect dslMain)'
      | (target code)
      v

Remarks:

-   only phase #2 should be run again if the application code changes
-   application of `compile` can be faster if `compile` is compiled to machine code in an additional phase between phase #1 and phase #2


Use case: Live coding system overview
----------------------------------


           editor frame    WebGL frame
               | ^             ^
    source code| |errors       |
               | | & infos     |pipeline description
               v |             |
             compiler----------/

Try online at [http://lambdacube3d.com/editor.html](http://lambdacube3d.com/editor.html)




Modules support
---------------

[Source code of the driver which handles modules](https://github.com/lambdacube3d/lambdacube-compiler/blob/master/src/LambdaCube/Compiler.hs)

Design decisions

-   modules can be loaded by filename or by module name
-   module header and body are parsed in two phases  
    This makes possible to process the import list even if there is a syntax error in the body.
-   modules' status and availabe information are cached in a map
-   builtin modules are always accessible by the last path element which is added by default

The module header contains

-   module name
-   export list
-   import list

The driver state contains

-   path list (in a ReaderT monad transformer)
-   map of cached modules: status + available information (in a StateT monad transformer)
-   fatal error message (in an ExceptT monad transformer)

Possible module status

status                                  available information
--------------------------------------- ---------------------------------
file cannot be found                    filename or module name (the paths are available in the driver state) 
header cannot be parsed                 module name, filename, source code
error with loading imported modules     module name, filename, source code, import and export lists (the successfully loaded modules and the error messages are available in the driver state)
body cannot be parsed                   module name, filename, source code, import and export lists, parse error
body cannot be elaborated               module name, filename, source code, import and export lists, desugared body, error message
loaded                                  module name, filename, source code, import and export lists, desugared body, elaborated definitions
--------------------------------------- ---------------------------------


Lexer
=====

[Source code of the lexer](https://github.com/lambdacube3d/lambdacube-compiler/blob/master/src/LambdaCube/Compiler/Lexer.hs)

Tasks

-   pruning white space and comments
-   recognise literals, reserved words and identifiers
-   recognise indentation (case & let expressions, where blocks, ...)
-   calculate ranges (start + end position) of tokens

Design decisions

-   Lexing and parsing is done in the same phase, sharing the same state  
    how it works: Whitespace is consumed immediately after each "lexeme".
-   use the `megaparsec` parser combinator library (a better parsec)
-   do custom indentation sensitive parsing
-   use custom lexer for literals

Indentation sensitive parsing
-----------------------------

State used for indentation sensitive parsing:

-   current position (line + column)
-   current active indentation, in a reader monad

Range calculation
-----------------

State used for calculating ranges:

-   position at the end of the last lexeme


Parsing & desugaring
====================

[Source code of the parser and desugarer](https://github.com/lambdacube3d/lambdacube-compiler/blob/master/src/LambdaCube/Compiler/Parser.hs)

Parser tasks

-   recognise syntactic structures
-   apply precedences
-   compute ranges of syntactic structures
-   handle namespaces: expression + type namespace

Parser design decisions

-   precedence application is done during parsing  
    This is possible with tying-the-knot technique: precedence information is part of parse result and it is used during parsing at the same time.

Scope checker tasks

-   disambiguate names

Scope checker design decisions

-   scope checking is done by calculating De Bruijn indices

Desugarer tasks

-   handle operator precendences
-   compile patterns and guards into function calls
-   desugar local functions
-   desugar node definitions
-   desugar case expressions
-   desugar let expressions
-   desugar if expressions
-   desugar list comprehensions
-   add missing foralls in type annotations
-   insert wildcards
-   desugar type synonym declarations
-   desugar type family declarations
-   desugar type classes and instances


Pattern match compilation
-------------------------

Main task:

-   transform pattern matching and guards to simple case expressions

Other tasks:

-   exhaustiveness check (is pattern matching total?)
-   reachability check (are there superfluous expressions involved?)
-   [pattern guards](https://wiki.haskell.org/Pattern_guard) desugaring
-   [view patterns](https://ocharles.org.uk/blog/posts/2014-12-02-view-patterns.html) desugaring

Design decisions:

-   The same algorithm is used to compile all language structures which contain pattern matching:
    -   function alternatives
    -   case expressions
    -   lambda expressions
    -   closed type family alternatives
    -   open type family instances
    -   type class instances, type class instance heads (look at type class desugaring)
-   A new data structure, *pattern guard trees* are used as intermediate representation.  
    Pattern match compilation is done in three steps:  

    1.  language structures are transformed into pattern guard trees
    1.  pattern guard trees are normalized
    1.  normalized pattern guard trees are compiled to case expressions

-   Exhaustiveness and reachability checks are done also in step 3.  
    This approach is less error-prone and more cheap than doing them in a separate phase.


### Pattern guard trees

Pattern guard trees is an intermediate representation to which all pattern match related syntactic structures are transformed.

Syntax of pattern guards trees (used only in this documentation):

----------- -- ---------------------------------------------------------- -----------------------
*guardtree* := *expression*                                               **success**
            |  `MatchFailure`                                             **failure**
            |  *guardtree* `|` *guardtree*                                **alternatives**
            |  *pattern* `<-` *expression* `,` *guardtree*                **pattern guard**
            |  `let` *bindings* `in` *guardtree*                          **let binding**
----------- -- ---------------------------------------------------------- -----------------------

Pattern guard trees are generalizations of [pattern guards](https://wiki.haskell.org/Pattern_guard):

-   pattern guard trees are expressions (may appear whereever an expression may appear)
-   pattern guard trees may have alternatives not only on the top level  
    For example, in  `[] <- x, (Nothing <- y, ... | True <- z, ...)`  both alternatives will match only if `x` is an empty list.
-   pattern guard trees may have let bindings not only on the top level

Examples:

1.  Definition of `not` with pattern guard trees:  

    ~~~~~ {.haskell}
    not x = (True  <- x,  False) | (False <- x,  True)
    ~~~~~


#### Semantics

The semantics of pattern guard trees is given by the `value` function:  
(This is pseudo code, it could be turned into a valid function producing a template Haskell splice):

~~~~~ {.haskell}
value :: GuardTree a -> Maybe a
value (Leaf e)   = Just e
value (Alt x y)  = value x <|> value y
value MatchFailure = Nothing
value (Let bs x) = value (let $bs in x)
value (PatternGuard p e x) = case matchPattern p e of
    Just bs -> value (let $bs in x)
    _       -> Nothing

matchPattern :: Pattern a -> Expression a -> Maybe Bindings
...

data GuardTree a where
    Leaf :: Expression a -> GuardTree a
    Alt  :: GuardTree a -> GuardTree a -> GuardTree a
    MatchFailure :: GuardTree a
    -- bindings are not strongly typed here for simplicity
    Let  :: Bindings -> GuardTree a -> GuardTree a
    PatternGuard :: Pattern b -> Expression b -> GuardTree a -> GuardTree a
~~~~~

#### Basic properties of pattern guard trees

------------------------------------- -------------------------- ------------------------------- 
t `|` (t' `|` t'')                    = (t `|` t') `|` t''       (`|`) is associative            
`MatchFailure` `|` t                  = t                        `MatchFailure` is left unit     
t `|` `MatchFailure`                  = t                        `MatchFailure` is right unit    
t `|` t                               = t                        (`|`) is idempotent
e `|` t                               = e                        success ignores alternative    
C1 p1 ... pn `<-` C2 e1 ... em`,` t   = `MatchFailure`           constructor match failure       
------------------------------------- -------------------------- ------------------------------- 

These are not true because of different strictness properties:

-   (p `<-` e, `MatchFailure`) = `MatchFailure`


### Desugaring to pattern guard trees

#### Function alternatives

1.  make n fresh variables v1, ..., vn where n is the arity of the function
2.  the new left hand side is `f` v1 ... vn
3.  translate each function alternative to a pattern guard tree with the help of v1, ..., vn
4.  compose the pattern guard trees with alternative patterns to get the new right hand side

Example:

Definition of `zip`:

~~~~~ {.haskell}
zip []     _      = []
zip x      []     = []
zip (a:as) (b:bs) = (a,b) : zip as bs
~~~~~

Translation to pattern guard trees:

~~~~~ {.haskell}
zip v0 v1
    = ([]   <- v0, _    <- v1,  [])
    | (x    <- v0, []   <- v1,  [])
    | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

### Normalization of pattern guard trees

The normal form of pattern guard trees contains only simple constructor patterns:

------------- -- ---------------------------------------------------------- -----------------------
*conpattern*  := *conname* (*variable*)*
------------- -- ---------------------------------------------------------- -----------------------

The following equations turn all patterns into simple constructor patterns:

---------------------------- -------------------------------------------------------------- ------------------- 
`_` `<-` e`,`  t             =  t                                                           wildcard elim       
v `<-` e`,`  t               =  `let` v = e `in` t                                          variable elim       
v`@`p `<-` e`,`  t           =  `let` v = e `in` p `<-` v`,` t                              at-pattern elim     
C p1 ... pn `<-` e`,`  t     =  C w1 ... wn `<-` e`,` p1 `<-` w1`,` ...`,` pn `<-` wn`,` t  nested pattern elim 
(f `->` p) `<-` e`,`  t      =  p `<-` f e`,` t                                             view pattern elim   
---------------------------- -------------------------------------------------------------- ------------------- 


### Compilation of pattern guard trees


Compilation is driven by the following equations:

1.  C ... `<-` e`,` t | t'  
    =  `seq` e (C ... `<-` e`,` t | t')

1.  `seq` e t  
    =  `case` e `of` p1 `->` t; ...; pn `->` t  
    if p1, ..., pn is complete and p1 evaluates e

1.  `case` e `of` ...; C e1 ... en `->` ... (C v1 ... vn `<-` e`,` t | t') ...; ...  
    = `case` e `of` ...; C e1 ... en `->` ... (`let` v1 = e1; ...; vn = en `in` t) ...; ...

1.  `case` e `of` ...; C1 e1 ... en `->` ... (C2 v1 ... vn `<-` e`,` t | t') ...; ...  
    =  `case` e `of` ...; C1 e1 ... en `->` ... t' ...; ...



# Complete example

Source code:

~~~~~ {.haskell}
zip []     _      = []
zip x      []     = []
zip (a:as) (b:bs) = (a,b) : zip as bs
~~~~~

Transformed to pattern guard trees:

~~~~~ {.haskell}
zip v0 v1
    = ([] <- v0, _ <- v1,  [])
    | (x <- v0, [] <- v1,  [])
    | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Simplified pattern guard trees:

~~~~~ {.haskell}
zip v0 v1
    = ([] <- v0,  [])
    | (let x = v0 in [] <- v1,  [])
    | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (1):

~~~~~ {.haskell}
zip v0 v1 = v0 `seq`
      ([] <- v0,  [])
    | (let x = v0 in [] <- v1,  [])
    | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (2) with patterns `[]` and `x:xs`:

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] ->
          ([] <- v0,  [])
        | (let x = v0 in [] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
    x: xs ->
          ([] <- v0,  [])
        | (let x = v0 in [] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (3); empty let is eliminated:

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs ->
          ([] <- v0,  [])
        | (let x = v0 in [] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (4):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs ->
          (let x = v0 in [] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Let floating:

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in
          ([] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (1):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in v1 `seq`
          ([] <- v1,  [])
        | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (2) with patterns `[]` and `y: ys`:

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in case v1 of
        [] ->
              ([] <- v1,  [])
            | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
        y: ys ->
              ([] <- v1,  [])
            | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (3):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in case v1 of
        [] -> []
        y: ys ->
              ([] <- v1,  [])
            | (a:as <- v0, b:bs <- v1,  (a,b) : zip as bs)
~~~~~

Apply (4):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in case v1 of
        [] -> []
        y: ys ->
              a:as <- v0, b:bs <- v1,  (a,b) : zip as bs
~~~~~

Apply (3):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in case v1 of
        [] -> []
        y: ys -> let a = x; as = xs in b:bs <- v1,  (a,b) : zip as bs
~~~~~

Apply (3):

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> let x = v0 in case v1 of
        [] -> []
        y: ys -> let a = x; as = xs in let b = y; bs = ys in  (a,b) : zip as bs
~~~~~

Simplification:

~~~~~ {.haskell}
zip v0 v1 = case v0 of
    [] -> []
    x: xs -> case v1 of
        [] -> []
        y: ys -> (x, y) : zip xs ys
~~~~~



#### Concrete algorithm

Filtering is a transformation on pattern guard trees, given an expession and a constructor name:

~~~~~ {.haskell}
filterTree :: Expression b -> Expression b -> GuardTree a -> GuardTree a
filterTree _ _ (Leaf e)   = Leaf e
filterTree e a (Alt x y)  = filterTree e a x <> filterTree e a y
filterTree e a MatchFailure = MatchFailure
filterTree e a (Let bs t) = Let bs (filterTree e a t)
filterTree e a@(Con c es) (PatternGuard (PCon c' vs) e' t)
    | e /= e' = PatternGuard (PCon c' vs) e' (filterTree e a t)
    | c /= c' = Nothing
    | otherwise = filterTree e a (let $(bind vs es) t)
~~~~~

...


#### Checks

Exhaustiveness check is just finding `MatchFailure` values in the result.

Reachability check is just finding parts of source code not present in result.


#### Extensions

Step (2) is very general:

-   For pattern matching just on a single constructor C, the patterns {C v1 ... vn, _} can be used.  
    This can prevent quadratic code blowup in case of ADTs with many constructors.
-   Pattern matching on types is possible in a similar way.
-   In case of GADTs, for better warnings, type information can be taken into account to restrict the set of matching constructor patterns,
    similar to [GADTs Meet Their Match](https://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf), implemented in GHC 8.

### Discussion

-   Extension with dependent pattern matching seems possible but has to be explored.
-   The algorithm produce fast code, but in some cases the size of produced code may blow up.  
    Compilation driven by more than 4 equations might prevent this.
-   [A prototype was implemented.](https://github.com/lambdacube3d/lambdacube-compiler/blob/master/prototypes/PatCompile.hs)

#### Related work

Have not seen this approach before; help to compare it with others.


Desugared source code
---------------------

~~~~~ {.haskell}
data SExp
    = SGlobal SIName
    | SVar SIName Int
    | SBind SI Binder SIName SExp SExp
    | SApp SI Visibility SExp SExp
    | SLet SI SIName SExp SExp
    | SLit SI Lit

data Binder
    = BPi  Visibility
    | BLam Visibility
    | BMeta      -- a metavariable is like a floating hidden lambda

data Stmt
    = Let SIName (Maybe SExp) SExp
    | Data SIName               -- name
           [(Visibility, SExp)] -- parameters
           SExp                 -- type
           [(SIName, SExp)]     -- constructor names and types
    | PrecDef SIName Fixity
~~~~~


Type inference
==============

Tasks

-   find semantic errors
-   complete code
    -   infer types
    -   construct witnesses for type class method invocation
    -   possibly find out inferrable values
-   normalize code
    -   reduce expressions (beta-reduction)
-   avoid infinite recursion (termination checking)  
    (this is not a priority at the moment)

Design decisions

-   use a dependently typed core language (treat types as values)  
    This gives more expressive power to static typing and somewhat simplifies the compiler at the same time.
-   type checking is based on [LambdaPi](https://www.andres-loeh.de/LambdaPi/) 
    -   use bidirection type checking
    -   do type inference and reduction in one step
    -   separate types and expressions
-   all code completion task is done by inferring values of hidden variables in the following two intermangled phases:
    1.  make hidden arguments (type applications, type class witnesses) explicit by inserting metavariables
    2.  eliminate metavariables
-   use a rich context  
    With this, the inference algorithm can take into account not just the types of bounded variables but also the fact that the expression is part of an application and more.
-   use the context as a zipper  
    The context is literally the context of the expression, so it can be used as a zipper. As a bonus, the type inference algorithm will be tail recursive.
-   keep the unreduced form of expressions too  
-   use labels to remember the beginning of right hand side instead of arity information
-   erease types when possible


Rich context
------------

Type inference algorithms process expressions by processing their subexpressions (in various orders).
When processing a subexpression, the type of variables bounded outside the expression is the minimal information through which the
subexpression and the whole expression is connected (from the type inference's point of view).
This information is usually called **context**.

For example, consider the following expression:

    \f -> \x -> \y -> f y x

The subexpressions and their contexts (for simplicity, the types in the contexts are some variables):

subexpression              context
-------------------------- ------------------------------
`\f -> \x -> \y -> f y x`  []
`\x -> \y -> f y x`        (`f` :: a) : []
`\y -> f y x`              (`x` :: b) : (`f` :: a) : []
`f y x`                    (`y` :: c) : (`x` :: b) : (`f` :: a) : []
`f y`                      (`y` :: c) : (`x` :: b) : (`f` :: a) : []
`x`                        (`y` :: c) : (`x` :: b) : (`f` :: a) : []
`f`                        (`y` :: c) : (`x` :: b) : (`f` :: a) : []
`y`                        (`y` :: c) : (`x` :: b) : (`f` :: a) : []
-------------------------- ------------------------------

We can store more information in context:

subexpression              rich context
-------------------------- ------------------------------
`\f -> \x -> \y -> f y x`  []
`\x -> \y -> f y x`        Lam (`f` :: a) : []
`\y -> f y x`              Lam (`x` :: b) : Lam (`f` :: a) : []
`f y x`                    Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : []
`f y`                      App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : []
`x`                        App2 (`f y`) : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : []
`f`                        App1 `y` : App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : []
`y`                        App2 `f` : App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : []
-------------------------- ------------------------------


Rich context as a zipper
------------------------

The rich context contains the real context of the subexpression, together with the path to the subexpression.
In fact, the rich context is very close to the zipper of expressions.

The type inference algorithm becomes tails recursive if its arguments are the rich context and the subexpression.


Bidirectional type checking
---------------------------



~~~~~ {.haskell}
infer :: Context -> SourceExp -> Maybe TypedExp
~~~~~

~~~~~ {.haskell}
check :: Context -> SourceExp -> Type -> Maybe TypedExp
~~~~~




Insertion of metavariables
--------------------------





Solving metavariables
---------------------






Code generation
===============

Currently there is only one code generator, which is wired in the compiler and generates intermediate representation
(called IR or graphics pipeline description)

Tasks

-   generate graphics pipeline descriptions

Design decisions

-   use a custom data type which encapsulates expessions with types and De Bruijn environment