diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-04-05 12:25:57 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-04-05 12:25:57 +0200 |
commit | 5912b63a89fd2db11aa0e767189856769e23f6ce (patch) | |
tree | 1730b4efb7801c9141a98af8c42485b4b9feaf78 /doc/guide.pandoc | |
parent | 4e802fead6bbfbbe47ade30d5c792210e39c7b5d (diff) |
document the idea of rich context
Diffstat (limited to 'doc/guide.pandoc')
-rw-r--r-- | doc/guide.pandoc | 69 |
1 files changed, 55 insertions, 14 deletions
diff --git a/doc/guide.pandoc b/doc/guide.pandoc index b4ba61bd..8d106ad8 100644 --- a/doc/guide.pandoc +++ b/doc/guide.pandoc | |||
@@ -28,7 +28,7 @@ Main design decisions | |||
28 | - code completion is done by type classes | 28 | - code completion is done by type classes |
29 | - abstractions are eliminated by reduction | 29 | - abstractions are eliminated by reduction |
30 | - Code generation is not part of the compiler; it is done during the reduction of the main expression. | 30 | - Code generation is not part of the compiler; it is done during the reduction of the main expression. |
31 | This helps to keep the compiler smaller and separate domain specific code. | 31 | This helps to keep the compiler smaller, and separate domain specific code from the compiler. |
32 | - The compiler has just two phases: | 32 | - The compiler has just two phases: |
33 | 1. lexing + parsing + scope checking + desugaring | 33 | 1. lexing + parsing + scope checking + desugaring |
34 | 2. type checking + type inference + normalization | 34 | 2. type checking + type inference + normalization |
@@ -69,7 +69,7 @@ Additinional design decisions: | |||
69 | 69 | ||
70 | - include pattern synonyms which can match different normal forms of `Expression` | 70 | - include pattern synonyms which can match different normal forms of `Expression` |
71 | This eases the description of code generation. | 71 | This eases the description of code generation. |
72 | - Ideally no error handling is needed during code generation; all misues should ruled out during the type checking of application code. | 72 | - Ideally no error handling is needed during code generation; all misues should be found during the type checking of application code. |
73 | - track compilation stages by the type system [(reference)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.4374) | 73 | - track compilation stages by the type system [(reference)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.4374) |
74 | - prevents even more misuses | 74 | - prevents even more misuses |
75 | - helps to speed up compilation (?) | 75 | - helps to speed up compilation (?) |
@@ -98,7 +98,7 @@ DSL compiler code: | |||
98 | -- (this is a custom DSL IO type) | 98 | -- (this is a custom DSL IO type) |
99 | data IO a = ... | 99 | data IO a = ... |
100 | 100 | ||
101 | -- definition of target code (e.g. ByteString) | 101 | -- definition of target code type (e.g. ByteString) |
102 | data Target = ... | 102 | data Target = ... |
103 | 103 | ||
104 | -- DSL compiler, including optimizations | 104 | -- DSL compiler, including optimizations |
@@ -126,7 +126,7 @@ Compilation flowchart: | |||
126 | lexing + parsing + scope checking + desugaring | 126 | lexing + parsing + scope checking + desugaring |
127 | & inference + normalization ------> halt with error message (phase #1) | 127 | & inference + normalization ------> halt with error message (phase #1) |
128 | | | 128 | | |
129 | | `compile` ready to be applied | 129 | | 'compile' ready to be applied |
130 | | | 130 | | |
131 | /---/ | 131 | /---/ |
132 | | | 132 | | |
@@ -136,16 +136,16 @@ Compilation flowchart: | |||
136 | | lexing + parsing + scope checking + desugaring | 136 | | lexing + parsing + scope checking + desugaring |
137 | | & inference + normalization ------> halt with error message (phase #2) | 137 | | & inference + normalization ------> halt with error message (phase #2) |
138 | | | | 138 | | | |
139 | | | normalized `dslMain` | 139 | | | normalized 'dslMain' |
140 | | v | 140 | | v |
141 | | reflection | 141 | | reflection |
142 | | | | 142 | | | |
143 | | | normalized `reflect dslMain` | 143 | | | normalized 'reflect dslMain' |
144 | | | (value of type `Expr (IO ())`) | 144 | | | (value of type 'Expr (IO ())') |
145 | v v | 145 | v v |
146 | function application & normalization | 146 | function application & normalization |
147 | | | 147 | | |
148 | | normalized `compile (reflect dslMain)` | 148 | | normalized 'compile (reflect dslMain)' |
149 | | (target code) | 149 | | (target code) |
150 | v | 150 | v |
151 | 151 | ||
@@ -443,18 +443,59 @@ Design decisions | |||
443 | - use a dependently typed core language (treat types as values) | 443 | - use a dependently typed core language (treat types as values) |
444 | This gives more expressive power to static typing and somewhat simplifies the compiler at the same time. | 444 | This gives more expressive power to static typing and somewhat simplifies the compiler at the same time. |
445 | - all code completion task is done by inferring values of hidden variables in the following two intermangled phases: | 445 | - all code completion task is done by inferring values of hidden variables in the following two intermangled phases: |
446 | 1. make every hidden argument application explicit by inserting metavariables | 446 | 1. make hidden arguments (type applications, type class witnesses) explicit by inserting metavariables |
447 | 2. gradually eliminate metavariables during type checking | 447 | 2. eliminate metavariables |
448 | - use a rich environment | 448 | - use bidirection type checking |
449 | - use a zipper to move around in the environment | 449 | - use a rich context |
450 | 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. | ||
451 | - use the context as a zipper | ||
452 | 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. | ||
450 | - do type inference and reduction in one step | 453 | - do type inference and reduction in one step |
454 | - keep the unreduced form of expressions too | ||
451 | - use labels to remember the beginning of right hand side instead of arity information | 455 | - use labels to remember the beginning of right hand side instead of arity information |
452 | - separate types and expressions | 456 | - separate types and expressions |
453 | - erease types when possible | 457 | - erease types when possible |
454 | 458 | ||
455 | 459 | ||
456 | Rich environment | 460 | Rich context |
457 | ---------------- | 461 | ------------ |
462 | |||
463 | Type inference algorithms process expressions by processing their subexpressions (in various orders). | ||
464 | When processing a subexpression, the type of variables bounded outside the expression is the minimal information through which the | ||
465 | subexpression and the whole expression is connected (from the type inference's point of view). | ||
466 | This information is usually called **context**. | ||
467 | |||
468 | For example, consider the following expression: | ||
469 | |||
470 | \f -> \x -> \y -> f y x | ||
471 | |||
472 | The subexpressions and their contexts (for simplicity, the types in the contexts are some variables): | ||
473 | |||
474 | subexpression context | ||
475 | -------------------------- ------------------------------ | ||
476 | `\f -> \x -> \y -> f y x` [] | ||
477 | `\x -> \y -> f y x` (`f` :: a) : [] | ||
478 | `\y -> f y x` (`x` :: a) : (`f` :: a) : [] | ||
479 | `f y x` (`y` :: a) : (`x` :: a) : (`f` :: a) : [] | ||
480 | `f y` (`y` :: a) : (`x` :: a) : (`f` :: a) : [] | ||
481 | `x` (`y` :: a) : (`x` :: a) : (`f` :: a) : [] | ||
482 | `f` (`y` :: a) : (`x` :: a) : (`f` :: a) : [] | ||
483 | `y` (`y` :: a) : (`x` :: a) : (`f` :: a) : [] | ||
484 | -------------------------- ------------------------------ | ||
485 | |||
486 | We can store more information in context: | ||
487 | |||
488 | subexpression rich context | ||
489 | -------------------------- ------------------------------ | ||
490 | `\f -> \x -> \y -> f y x` [] | ||
491 | `\x -> \y -> f y x` Lam (`f` :: a) : [] | ||
492 | `\y -> f y x` Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
493 | `f y x` Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
494 | `f y` App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
495 | `x` App2 (`f y`) : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
496 | `f` App1 `y` : App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
497 | `y` App2 `f` : App1 `x` : Lam (`y` :: c) : Lam (`x` :: b) : Lam (`f` :: a) : [] | ||
498 | -------------------------- ------------------------------ | ||
458 | 499 | ||
459 | 500 | ||
460 | 501 | ||