From 02ff39d0ab6488fa8cedb31030130b352e10b3e2 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Wed, 27 Nov 2024 16:18:16 +0100
Subject: Initial typing

---
 readme.md | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

(limited to 'readme.md')

diff --git a/readme.md b/readme.md
index 7d0378d..c49f396 100644
--- a/readme.md
+++ b/readme.md
@@ -1,44 +1,49 @@
 # mili
 
 > Minimal linear lambda calculus with linear types, de Bruijn indices
-> and unbounded iteration/minimization
+> and unbounded iteration
 
 Linear lambda calculus is a restricted version of the lambda calculus in
 which every variable occurs exactly once. This typically implies ptime
 normalization and therefore Turing incompleteness.
 
-We extend the linear lambda calculus with unbounded
-iteration/minimization such that it barely becomes Turing complete,
-while still benefitting from the advantages of syntactic linearity.
+We extend the linear lambda calculus with unbounded iteration such that
+it barely becomes Turing complete, while still benefitting from the
+advantages of syntactic linearity.
 
 ## core
 
 Mili's core syntactic representation consists of only five constructs:
 
 ``` haskell
-data Term = Abs Int Term                    -- | Abstraction at level
-          | App Term Term                   -- | Application
-          | Lvl Int                         -- | de Bruijn level
-          | Num Nat                         -- | Peano numeral
-          | Rec (Term, Term) Term Term Term -- | Unbounded iteration
+data Term = Abs Int Term                 -- | Abstraction at level
+          | App Term Term                -- | Application
+          | Lvl Int                      -- | de Bruijn level
+          | Num Nat                      -- | Peano numeral
+          | Rec Term Term Term Term Term -- | Unbounded iteration
 ```
 
-Lets and Pairs are only used in the higher-level syntax. This allows us
-to use a minimal abstract reduction machine.
+Lets and Pairs are only used in the higher-level syntax. There are no
+erasers or duplicators. This allows us to use a minimal abstract
+reduction machine as well as a linear type system.
+
+In general, a more elegant encoding would be *tagless*, as can be seen
+in an implementation by [by Oleg
+Kiselyov](https://okmij.org/ftp/tagless-final/course/LinearLC.hs).
+However, tagless encodings are hard to work with and can't be compiled.
 
 ## roadmap
 
 -   [x] basic syntax
 -   [x] linearity check
 -   [x] basic reduction
--   [ ] type syntax
 -   [ ] type checking
--   [ ] reduction shortcut
+-   [ ] syntax that embeds linearity (levels?)
+-   [ ] compile to LLVM stack machine + reduction shortcut
 -   [ ] preprocessor
     -   [ ] `:test`
     -   [ ] `:import`
 -   [ ] more examples
--   [ ] compile to LLVM stack machine
 
 ## references
 
-- 
cgit v1.2.3