diff options
Diffstat (limited to 'sec/compiler.ltx')
| -rw-r--r-- | sec/compiler.ltx | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index dde2856..2cfde8e 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -6,12 +6,25 @@ \TODO{ \begin{itemize} - \item QTT basics - \item intrinsically well-scoped AST - \item bidirectional judgement - \item well-typed data types - \item type checking function - \item irrelevant pattern matching + \item describe that I have a type checker and compiler implemented in Idris + \item explain what intentionally well-scoped syntax is + \item justify why I used intentionally well-scoped syntax + \item describe how type checking produces a derivation + \item explain the derivation is runtime erased + \item justify the derivation having no runtime cost + \item describe why knowing there is a derivation is necessary + \item explain why these extra features do not guarantee compiler correctness + \end{itemize} +} + +\TODO{ + \begin{itemize} + \item justify how dynamic types make Scheme a good compilation target + \item describe how products are compiled to assoc-lists + \item describe how sums are compiled to tagged values + \item describe how dynamic typing removes the need for roll + \item explain why fold needs to know the term has a valid type + \item explain why fold must be compiled recursively with map \end{itemize} } |