diff options
Diffstat (limited to 'readme.md')
| -rw-r--r-- | readme.md | 33 |
1 files changed, 19 insertions, 14 deletions
@@ -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 |