sml-typed-abts
sml-typed-abts copied to clipboard
RedPRL
second-order abstract syntax
Right now, constructing and deconstructing ABTs is very expensive; there is basically no way to really optimize the ABT interface (this was the conclusion of Tom 7 many years ago),...
The error messages that are emitted from this library are simply impossible to debug. James has made progress by adding a `BadMetasubst` exception, which is good; we should go even...
The rust-style issue triage labels are really nice and helpful, and I've liked how they turned out in Yggdrasil and RedPRL. We should use those here too.
let's add a new constructor for explicit substitutions! And we can also add some operations to wring out the substitutions. @freebroccolo
Currently, `SYMBOL.named` is used; we need to use `SYMBOL.fresh ctx` instead.
When we begin to tune performance and try out things like hash-consing, we'll need to have a benchmark in place.
Sadly, the `SORT` signature is part of `cmlib`, so it's kind of inconvenient if we use it here. ~~I think a better option would be to just collapse the whole...