Merge pull request #25 from at15/j/feature/variable

[j] Init Variable and Type checker

doc/dev-notes/at15/antlr.md

@@ -15,8 +15,78 @@ Language Implementation Patterns
   - group character into tokens, so parser rules can be more generic `x > 1` vs. `ID > NUM`
   - lexer takes in characters and generate tokens
   - parser takes in tokens and generate parse tree
+- [ ] symbol table
+- [ ] enforce static typing
 
 ## Grammar file
 
 - Ucfirst is token (lexer), lower case is rule (parser)
-  - [ ] this is mentioned in book or doc
+  - [ ] this is mentioned in book or doc
+
+## ANTLR3 Chap 5 Walking and Rewriting Trees
+
+P113 External Tree Visitor
+
+- rely on node types themselves
+- rely on node's token type
+
+double-dispatch, one `visit` on node, one `visit` on visitor
+
+````
+public class AddNode extends Node {
+  public Node l;
+  public Node r;
+  // dispatcher, in ANTLR4 generated parse tree context, it is called accept
+  public void visit(MathVisitor visitor) {
+    visitor.visit(this);
+  }
+}
+
+public interface MathVisitor {
+  void visit(AddNode n);
+  void visit(IntNode n);
+}
+
+public class PrintVisitor implements MathVisitor {
+  // NOTE: in ANTLR4, we are using visit(n.l), because the visit method is 
+  // public T visit(ParseTree tree) {}
+  //    return tree.accept(this);
+  // }
+  public void visit(AddNode n) {
+    n.l.visit(this);
+    System.out.println('+')
+    n.r.visit(this);
+    System.out.println();
+  }
+}
+````
+
+the example is pretty similar to the visitor we use in ANTLR4, except
+
+- in visitor
+  - no overload on `visit` method, the generated interface has name like `visitInt`
+  - `visit` method would call `node.accept(this)`, so write `visit(n.child)` instead of `n.child.accept(this)`
+- in node (parse tree context)
+  - `visit` is called `accept`
+  - does not call `visitor.visit(this)`, but call its own named method, like `IntNode` would call `visitInt`
+
+## ANTLR3 Chap 8 Enforcing Static Typing Rules
+
+Three pass
+
+- parser builds an AST (not parse tree?)
+- builds scope tree and populates a symbol table
+- compute type of each expression
+  - type promotion
+  - typing checking
+
+In practice, second and third can be put into single pass, it's even possible to put all three into one (lua?). 
+Unless run-time speed is critical, it's better to break into different parts
+
+- [ ] P113 External Tree Visitor
+- [ ] P159 Symbol Table
+- hmm, the logic is hard coded in grammar file
+
+Automatic Type Promotion
+
+- we can do our syntax sugar for method operation in similar way, but how to combine it with compute type of each expression

doc/dev-notes/at15/log.md

@@ -1,7 +1,12 @@
 # Log
 
+## 2017-11-26
+
+- read ANLTR3 Chapter 8 Enforcing static typing rules
+
 ## 2017-11-25
 
+- finish syntax, use immutable variable
 - introducing variable [#23](https://github.com/at15/reika/issues/23)
 
 ## 2017-11-24

doc/dev-notes/at15/type-inference.md

@@ -0,0 +1,197 @@
+# Type Inference
+
+- [#26](https://github.com/at15/reika/issues/26)
+
+## Progamming Languages: Application and Interpretation 15
+
+Using Racket
+
+### 15.1 Types as Static Disciplines
+
+- static type checking: checking (declared) types before the program even executes
+- it can be useful to think of parsing as being simply the very simplest kind of type-checking:
+determining (typically) whether the program obeys a context-free syntax
+- type checking then asks whether it obeys a context-sensitive (or richer) syntax
+- type checking is a generalization of parsing, in that both are concerned with syntactic methods for enforcing disciplines on programs
+
+### 15.2 A Classical View of Types
+
+#### 15.2.1 A Simple Type Checker
+
+- typing environment, maps names to types
+- tc, tells what type an expression is
+  - no difference between handling `plus` and `mult` expression
+  - application
+    - compute value of function
+    - compute value of argument
+    - ensure function expression is function type
+    - check argument expression is compatible type
+  - abstraction
+    - extend typing environment with formal name bound to its type, and in that extended environment type-check the body
+
+**The difference between interpreter and type-checker**
+
+- in the interpreter, application was responsible for evaluating the argument expression, extending the environment, and evaluating the body
+- in type-checker, application does check the argument expression but leaves the environment alone, and simply returns the type of the body without traversing it. Instead, the body is actually traversed by the checker when checking a function definition, so this is the point at which the environment actually extends
+
+#### 15.2.3 Recursion in Code
+
+- previous done via desugaring
+
+````
+((lambda (x) (x x)
+  (lambda (x) (x x)))
+````
+
+becomes a infinite type, why?
+
+- we cannot type Omega at all
+- the typed language we have so far has a property called strong normalization: every expression that has type will terminate computation after a finite number of steps
+
+What's the use of a language in which all programs terminate
+
+- none, for general purpose programming language
+- linker in Standard ML
+- scheduler, packet-filter, real-time event processor
+
+- [ ] TODO: the real code
+
+#### 15.2.4 Recursion in Data
+
+- [ ] TODO: skipped for now
+
+#### 15.2.5 Types, Time, and Space
+
+- save time, no longer need to check at runtime
+- save space, type tags are no longer necessary
+
+#### 15.2.6 Types and Mutation
+
+- traditional type checkers: types must be invariant across mutation
+
+#### 15.2.7 The Central Theorem: Type Soundness
+
+Difference between type checker and evaluator
+
+- type checker only sees program text, evaluator runs over actual stores
+- type environment binds identifier to types, evaluator environment binds identifiers to values or locations
+- type checker compresses (even infinite) sets of values into types, whereas the evaluator treats these distinctly
+- type checker always terminates, whereas the evaluator might not
+- type checker passes over they body of each expression only once, whereas the evaluator might pass over each body anywhere from zero to infinite times
+
+Progress and Preservation (hi, TAPL ...)
+
+### 15.3 Extension to the Core
+
+#### 15.3.1 Explicit Parametric Polymorphism
+
+- [ ] TODO: skipped
+
+#### 15.3.2 Type Inference
+
+- even in languages with inference, programmers are free (and for documentation purposes, often encouraged - as you have been) to declare types)
+- inference can be think as a user convenience of writing less type annotation, but the language underneath is explicitly typed
+
+````
+(lambda ([x : number]) : string x)
+(* after erasure, the ill-typed one could actually become typeable *)
+(lambda (x) x)
+````
+
+- previous simple recursive descent type-checking algorithm will no longer work
+
+Two steps
+
+- generate constraints, based on program terms, on what the types must be
+- solve constraints to identify inconsistencies and join together constraints spread across the function body
+
+##### Constraint Generation
+
+- constraint generation walks the program source, emitting appropriate constraints on each expression
+
+What can we say about the type of an expression
+
+- it is related to the type of some identifier
+- it is related to the type of some other expression
+- it is a number
+- it is a function, whose domain and range types are presumably further constrained
+
+````
+(define-type Constraints
+    [eqCon (lhs : Term) (rhs : Term)])
+
+(define-type Term
+    [tExp (e : ExprC)
+    [tVar (s : symbol)]
+    [tNum]
+    [tArrow (dom : Term) (rng : Term)])
+````
+
+Now we can define the process of generating constraints
+
+````
+(define (cg [e : ExprC]) : (listof Constraints))
+  (type-case ExprC e)
+    - numC
+    - idC
+    - plus/mul
+    - appC
+    - lamC))
+````
+
+- case numC, `[numC (_) (list (eqCon (tExp e) (tNum)))]`
+- case idC, `[idC (_) (list (eqCon (tExp e) (tVar s)))]`
+- case plus/mul, constraints in each sub expression, each sub should be numeric, entire exp is numeric
+
+````
+[plusC (l r) (append3 (cg l)
+                      (cg r)
+                      (list (eqCon (tExp l) (tNum))
+                            (eqCon (tExp r) (tNum))
+                            (eqCon (tExp e) (tNum))))]
+````
+
+function definition lamC
+
+````
+[lamC (a b) (append (cg b)
+                    (list (eqCon (tExp e) (tArrow (tVar a) (tExp b)))))]
+````
+
+function application appC
+
+````
+[appC (f a) (append3 (cg f)
+                     (cg a)
+                     (list (eqCon (tExp f) (tArrow (tExp a) (tExp e)))))]
+````
+
+##### Constraint Solving Using Unification
+
+- the goal of unification is generate a substitution, or mapping from variables to terms that do not contain any variables
+- solved using gaussian elimination
+  - [ ] can have under and over constrained
+- iterate over the set of constraints, total 4^2 = 16 cases, can use less cases to cover in actual code
+- begins with all constraints and empty substitution
+- when all constraints have been disposed, unification returns the final substitution set.
+
+Unification process
+
+- if left side is variable (?), add right side to substitution to truly eliminate it
+  - include a occurs check, a check for whether the same variable occurs on both sides, if it does, decline to unify
+
+- if left side is var, lookup in substitution
+  - if present, replace current constraint with a new one, otherwise, extend the substitution
+  - else, extend substitution
+- expression designator is same as var (??)
+- number, check right hand side
+  - number, do nothing
+  - function, type error
+  - var and expr can't be there
+- function, extend constraints instead of shrink it
+
+- if above process success, the success of the above process implies that the program would have typed-checked, so we need not explicitly run the type-checker over this program
+- error messages are harder to understand
+- over-constrained, type error
+- under-constrained, don't have enough information to make definitive statement about all expressions `(lambda (x) x)` becomes `('a -> 'a)`
+- automatically computes the most general types for an expression, also known as principle types

doc/spec/0.1/02-primitive-type.md

@@ -45,5 +45,21 @@ Overloading
     - Python has always provided a variety of built-in and standard-library generic functions, such as len(), iter()
     - does not have a simple or straightforward way for developers to create new generic function
     - In addition, it is currently a common anti-pattern for Python code to inspect the types of received arguments, in order to decide what to do with the objects
-
-## Example
+
+## Variable
+
+- start with smaller case
+- no mutable variable, for now, it depends on how the interpreter/compiler implement stuff
+- as long as the data size is small, it should work ....
+
+````
+x = 1
+y = x + 1
+let z:Double = x + 1
+````
+
+## Type
+
+- start with upper case
+
+## Example

impl/reika-j/doc/0.1.md

@@ -4,6 +4,6 @@
 
 - Parse Tree from ANTLR generated Parser `parser.ReikaParser`
 - Untyped AST from `ast.UntypedVisitor`
-- Typed AST from `type.Reconstructor`
+- Typed AST from `varType.Reconstructor`
 - Evaluation using `interpreter.TreeInterpreter`
 - ? Translate into other language

impl/reika-j/src/main/java/me/at15/reika/ast/ASTVisitor.java

@@ -0,0 +1,25 @@
+package me.at15.reika.ast;
+
+import me.at15.reika.common.ReikaException;
+
+public interface ASTVisitor<T> {
+    T visit(Node n) throws ReikaException;
+
+    T visit(Program n) throws ReikaException;
+
+    T visit(Val.Bool n) throws ReikaException;
+
+    T visit(Val.Int n) throws ReikaException;
+
+    T visit(Val.Double n) throws ReikaException;
+
+    // TODO: do we still need to visit type node?
+
+    T visit(Var n) throws ReikaException;
+
+    T visit(OpUnary n) throws ReikaException;
+
+    T visit(OpBinary n) throws ReikaException;
+
+    T visit(Let n) throws ReikaException;
+}

impl/reika-j/src/main/java/me/at15/reika/ast/Let.java

@@ -0,0 +1,20 @@
+package me.at15.reika.ast;
+
+import me.at15.reika.common.ReikaException;
+
+public class Let extends Node {
+    public final Var var;
+    public final Type varType;
+    public final Node term;
+
+    public Let(Var var, Type varType, Node term) {
+        this.var = var;
+        this.varType = varType;
+        this.term = term;
+    }
+
+    @Override
+    public <T> T accept(ASTVisitor<? extends T> visitor) throws ReikaException {
+        return visitor.visit(this);
+    }
+}

impl/reika-j/src/main/java/me/at15/reika/ast/Node.java

@@ -1,9 +1,11 @@
 package me.at15.reika.ast;
 
+import me.at15.reika.common.ReikaException;
 import me.at15.reika.type.Ty;
 
 public abstract class Node {
-//    public abstract Ty Type();
+    public Ty type;
 
-//    public abstract void NodeType();
+    public abstract <T> T accept(ASTVisitor<? extends T> visitor) throws ReikaException;
+    //    public abstract void NodeType();
 }