52 lines
2.5 KiB
Markdown
52 lines
2.5 KiB
Markdown
|
|
# Newt
|
|
|
|
Newt is a dependently typed programming language that compiles to javascript. It is
|
|
my first attempt to write a dependent typed language. It is inspired by Idris,
|
|
Elaboration Zoo, pi-forall, and various tutorials.
|
|
|
|
The goal is to have inductive types, pattern matching, compile to javascript, and be self hosted. At the very least though, I'd like to be able to build a little browser "playground" to compile and run code.
|
|
|
|
## Building
|
|
|
|
There is a `Makefile` that builds both chez and javascript versions. They end up in
|
|
`build/exec` as usual. I've also added a `pack.toml`, so `pack build`
|
|
|
|
There is a vscode extension in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace.
|
|
|
|
## Overview
|
|
|
|
I'm doing Type in Type for now.
|
|
|
|
The type checking and implicits are based on elaboration zoo. I'm using normalization
|
|
by evaluation with closure objects rather than HOAS. When going under binders in the
|
|
typechecking, I follow Kovács example and place a `VVar` into the environment instead of
|
|
doing `subst`.
|
|
|
|
The raw syntax is `Raw`. This is elaborated to `Tm`. There is a top level context and a
|
|
context during checking. The top level context uses names, and type checking uses deBruijn
|
|
indices for `Tm` and levels for `Val`. For compilation, this is converted to `CExp`, which works out how arity and closures will work, and then `JSExp` which is javascript AST.
|
|
|
|
I have `Let` in the core language. Partly because I'd like this to make it into javascript (only compute once), but also because it's being leveraged by the casetree stuff.
|
|
|
|
## Case Tree
|
|
|
|
I've got no idea what I'm doing here. I worked off of Jesper Cockx "Elaborating Dependent (Co)pattern Matching", leaving out codata for now.
|
|
|
|
## Issues
|
|
|
|
- I need to do some erasure of values unused at runtime
|
|
- I'm a little fuzzy on the "right way" to deal with constraints from unification
|
|
- I'm a little fuzzy on how much to evaluate and when
|
|
- I'm not postponing anything, and I suspect I will need to
|
|
|
|
## References
|
|
|
|
"Unifiers as Equivalences" has unification with types. Look into adapting some of that (or at least read/understand it). Indexed types are mentioned here.
|
|
|
|
"Elaborating Dependent (Co)pattern Matching" describes building case trees. Section 5.2 has the algorithm.
|
|
|
|
"A prettier printer" was the basis of the pretty printer.
|
|
|
|
"Elaboration Zoo" was a resource for typechecking and elaboration. In particular pattern unification and handling of implicits is based on that.
|