From 26119be8b60a708464e1b5c668de00486c68e498 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 15 Nov 2024 21:16:32 -0800 Subject: [PATCH] update readme --- README.md | 38 +++++++++++++++++++++----------------- TODO.md | 10 +++++----- 2 files changed, 26 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 652e7f6..1407292 100644 --- a/README.md +++ b/README.md @@ -14,12 +14,21 @@ output, and run code. The repository is tagging `.newt` files as Agda to convince github to highlight them. +There is a web playground at https://dunhamsteve.github.io/newt. The top left corner +has a dropdown with some samples. At the moment, it shows generated code, but doesn't +execute it. + ## 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` also works. -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. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output is in flux. +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. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output format is in flux. + +The web playground is in playground. +- `npm install` will pull down dependencies. +- `./build` will build the web workers and install sample files (`make` must be run in root first). +- `npx vite` will run the dev server. ## Overview @@ -36,37 +45,32 @@ indices for `Tm` and levels for `Val`. For compilation, this is converted to `C 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. +I also have `Case` in the core language. + ## 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. +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. I've now added matching primitives, requiring a default case. When splitting on inductive types it will break out all of the remaining cases and doesn't emit a default case. -For the dependent thing, I've change unify to return `VVar` constraints. I think such constraints would be an error while typechecking on RHS (meta solutions are handled separately). On the LHS, I'm rewriting the environment to turn the var from a bind to a define. Unification has been tweaked to look up `VVar` in environment. Bind will hand back the same `VVar`. +I'm essentially putting the constraints into the environment like `let`. This is a problem when stuff is already in `Val` form. Substitution into types in the context is done via quote/eval. I plan to revisit this. -Some of this I could probably do with subst, but the RHS is `Raw`, it takes typechecking to turn it into a clean `Tm`, and I need this information for the typechecking. To substitute into the goal type for the RHS, I am now -doing a quote and eval to get case to expand. This is a bit of a stopgap because case is only eval'd when going -from `Tm` to `Val`. I think I'll need a way to eval a VCase during unification, as we do with function applications. +I intend to add the codata / copatterns from the paper, but haven't gotten to that yet. ## Evaluation -Following kovacs, I'm putting `VVar` into context env when I go under binders. This avoids substitution. +Following kovacs, I'm putting `VVar` into context env when I go under binders in type-checking. This avoids substitution. ## Autos Newt has primitive auto implicits. They are denoted by double braces `{{}}` as in Agda. Newt will search for a function that returns a type in the same family, only has implicit and auto-implicit arguments, and unifies (satisfying any relevant constraints). -## Issues - -- I should 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 +This search can be used to manually create typeclasses. `do` blocks are supported, desugaring to `>>=`, which it expects to be the `bind` of a Monad typeclass. ## References -"Elaborating Dependent (Co)pattern Matching" describes building case trees. Section 5.2 has the algorithm. +"Elaborating Dependent (Co)pattern Matching" by Jesper Cockx and Andreas Abel describes building case trees. Section 5.2 describes the algorithm. -"A prettier printer" was the basis of the pretty printer. +"A prettier printer" by Philip Wadler 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. +"Elaboration Zoo" by András Kovács was my primary resource for typechecking and elaboration. In particular pattern unification and handling of implicits is based on it. -"Unifiers as Equivalences" has unification with types. Look into adapting some of that (or at least read/understand it). Indexed types are mentioned here. +There were many other resources and papers that I used to learn how dependent typed languages are built. diff --git a/TODO.md b/TODO.md index 420141b..c1774d3 100644 --- a/TODO.md +++ b/TODO.md @@ -12,14 +12,13 @@ - [x] Check for shadowing when declaring dcon - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if we have different core terms for TCon/DCon/Function -- [ ] Require infix decl before declaring names (helps find bugs) +- [ ] Require infix decl before declaring names with `_` (helps find bugs) - [ ] sugar for typeclasses - [ ] maybe add implicits in core to help resugar operators? - There is also a bit where kovacs uses the implicit on the type (a value) to decide to insert -- [ ] consider binders in environment, to better mark let and to provide names +- [ ] consider binders in environment, like Idris, to better mark `let` and to provide names - [ ] move some top-level chattiness to `debug` -- [ ] consider optionally compiling to eliminators for a second type-checking pass. This - would help catch bugs. +- [ ] consider optionally compiling to eliminators for a second type-checking pass to help catch bugs. - [x] Allow unicode operators/names - Web playground - [x] editor @@ -38,7 +37,7 @@ - [ ] Get `Combinatory.newt` to work - [x] Remember operators from imports - [ ] Default cases for non-primitives (currently gets expanded to all constructors) - - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from the individual, unnamed cases though. + - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from breaking out the individual, unnamed cases though. - There are cases where we have `_` and then `Foo` on the next line, but they should all get collected into the `Foo` case. I think I sorted all of this out for primitives. - [x] Case for primitives - [ ] aoc2023 translation @@ -104,6 +103,7 @@ - [ ] Read Ulf Norell thesis - [ ] Finish reading dynamic pattern unification paper to see what is missing/wrong with the current implementation +- [ ] Read "Unifiers as Equivalences" has unification with types. Look into adapting some of that (or at least read/understand it). Indexed types are mentioned here. ### Other issues