From c59c0f3e5b7288917e19a557b0d6d6a72757b0c1 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 1 May 2024 17:07:47 +0200 Subject: [PATCH] readme: add syntax description and roadmap --- README.md | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/README.md b/README.md index d4dc395..b5e8644 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,8 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc) ## Ladder Types +### Motivation + In order to implement complex datastructures and algorithms, usually many layers of abstraction are built ontop of each other. Consequently higher-level data types are encoded into lower-level data @@ -57,6 +59,50 @@ this: 1696093021:1696093039:1528324679:1539892301:1638141920:1688010253 ``` +### Syntax + +In their core form, type-terms can be one of the following: +- (**Atomic Type**) | `SomeTypeName` +- (**Literal Integer**) | `0` | `1` | `2` | ... +- (**Literal Character**) | `'a'` | `'b'` | `'c'` | ... +- (**Literal String**) | `"abc"` +- (**Parameter Application**) | `` given `T1` and `T2` are type-terms +- (**Ladder**) | `T1 ~ T2` given `T1` and `T2` are type-terms + +Ontop of that, the following syntax-sugar is defined: + +#### Complex Types +- `[ T ]` <===> `` +- `{ a:A b:B }` <===> ` <"b" B>>` +- `a:A | b:B` <===> ` <"b" B>>` + +#### Function Types +- `A -> B` <===> `` + +#### Reference Types +- `*A` <===> `` +- `&A` <===> `` +- `&!A` <===> `` + + +### Equivalences + +#### Currying +`< C>` <===> `` + +#### Ladder-Normal-Form +exhaustively apply `` => `~` + +e.g. +- `[~Char~Ascii]` ===> `[]~[Char]~[Ascii]` + +#### Parameter-Normal-Form +exhaustively apply `~` => `` + +e.g. +`[~Char~Ascii]` ===> `[]~[Char]~[Ascii]` + + ## How to use this crate ```rust @@ -73,6 +119,19 @@ fn main() { } ``` +## Roadmap + +- [x] (Un-)Parsing +- [x] (De-)Currying +- [x] Unification +- [x] Ladder-Normal-Form +- [x] Parameter-Normal-Form +- [ ] (De)-Sugaring + - [ ] Seq + - [ ] Enum + - [ ] Struct + - [ ] References + - [ ] Function ## License [GPLv3](COPYING)