diff options
author | JJ | 2023-07-19 19:25:30 +0000 |
---|---|---|
committer | JJ | 2023-07-20 02:08:36 +0000 |
commit | f5e61572b217c5445c3cd593d1cc94697fa7ec48 (patch) | |
tree | 5ae7c5a95cac5c2a23c27ae10f48ebf4c0e4e684 /README.md | |
parent | 99769e9ebb94d1dcc12f2d1f6a6d899f7a229676 (diff) |
major cleanups: switch to dynamic Errors, impl Context, rename enums/records to unions/structs
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 33 |
1 files changed, 25 insertions, 8 deletions
@@ -1,4 +1,10 @@ -# chrysanthemum: a simple type system +# chrysanthemum + +chrysanthemum is a simple language with a type system, initially written as a term project for CPSC 539. +It implements a number of features from the excellent *Types and Programming Languages*, including: +- The simply typed lambda calculus +- Bidirectional type checking and subtyping support +- A somewhat complex type system: including support for `unit`, `bool`, `nat`, `int`, `float`, `str`, `union`, `struct`, `empty`, and `err` types ## todo @@ -8,19 +14,30 @@ - [x] bidirectional typechecking: implement `infer` and `check` - [x] extend to additional basic types: refactor `Term` - [ ] extend to complex types: implement `access` -- [ ] simple effects: extend `ast` - [ ] type classes: implement `monomorphize` +- [ ] simple effects: extend `ast` - [x] testtesttest ## architecture ```bash src/ -src/main.rs # the user facing program -src/parser.rs # parses user programs into proper data structures -src/ast.rs # the fundamental representation of the program -src/simple.rs # the core of the lambda calculus: checking, inference, evaluation -src/effects.rs # code for effects idk -src/classes.rs # a monomorphization pass for type classes +src/main.rs # the user facing program +src/simple.rs # the simple lambda calculus: execution +src/ast.rs # the fundamental representation of types and terms +src/bidirectional.rs # the core of the language: checking, inference +src/unification.rs # an alternate core: checking and inference by unification +src/parser.rs # parses user programs into proper data structures +src/monomorphize.rs # a monomorphization pass for type classes +src/effects.rs # code for effects idk test/ # various tests ``` + +## bibliography + +- [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/) +- [Bidirectional Typing Rules: A Tutorial](https://www.davidchristiansen.dk/tutorials/bidirectional.pdf) +- [Bidirectional Typechecking](https://research.cs.queensu.ca/home/jana/bitype.pdf) +- [Typechecking for Higher-Rank Polymorphism](https://arxiv.org/pdf/1306.6032.pdf) +- [Bidirectional Type Class Instances](https://arxiv.org/pdf/1906.12242.pdf) +- [How to make ad-hoc polymorphism less ad-hoc](https://dl.acm.org/doi/pdf/10.1145/75277.75283) |