redex's People
Forkers
sznurekredex's Issues
make hashing alpha-equivalence-respecting
Robby says: "One thing to also look into for Redex: in addition to an
alpha-sensitive equality, we also need an alpha-sensitive hashing. I
think it's straightforward: just normalize and then call the
equal-based hash function that's built into Redex.
We'll need this for traces (the way it collapses different paths to
the same term is based on hashing)."
make alpha-equivalence the internal notion of equivalence for Redex matching
make name generation more user-friendly
enforce `rib`
Currently, rib
and shadow
have no functional difference.
eliminate O(n^2) cost of alpha-equivalence
use alpha-equivalence as `default-equiv`, when possible
proposed design: if default-equiv
accepts three arguments, also give it the language as an argument
document #:binding-forms (and other visible changes)
deal with metafunction caching
Freshening is (and should be!) nondeterministic. But metafunction caching assumes that metafunctions are deterministic. I think that we need to disable caching for any metafunctions that destructure any binding forms (or, at least, any binding forms that bind names). It sounds pretty costly, unfortunately.
benchmark a metafunction-heavy model
provide substitution and alpha-equivalence to the user directly
extended/union languages don't work with binding
when no binding specification is applicable, a list ought to treat all free names in its subterms as free
Essentially, the "default" binding form that applies to everything will have special behavior: even though it #:exports nothing
; any binders free in its subterms should be free in it (this is already inherently true of references).
By accident, this is already mostly the case, and indeed needs to be the case for the Right Thing to happen in certain situations.
This proposal will make non-binding-specified lists less like binding forms. Suppose that one is passing multiple arguments to a metafunction, one of which is (define x 1)
(which exports x
), and one passes those arguments as a plain list (in fact, this is exactly how metafunctions normally operate). The list must then be destructured, and therefore freshened. If x
is treated as free, it must not be renamed, but normally, if (define x 1)
is neither imported nor exported, then x
is treated as bound, and therefore in need of renaming.
collapse alpha-equivalent results from reduction relations
fix commit structure
allow `...` to create binding forms
This would make it possible to express let*
in its natural syntax.
eliminate O(n^2) cost of freshening
I think that this can be done Dybvig-style, but I worry that it might only be possible if we were willing to put non-plain-old-data into terms, and break term-destructuring-with-anything-other-than-redex-match.
we don't know how binding forms perform
make generation/enumeration respect alpha-equivalence
The basic approach is simple: the enumeration for a binder is a single (fresh) atom, since it doesn't matter what you choose. Inside a scope, the finite enumeration of the names that are bound in that scope comes before the infinite enumeration of free names (on the theory that choosing different free names is not as interesting as choosing different bound names).
However, this probably won't work: (a) Whether a name is a binder or not is not defined until the term is complete, and can be matched against a pattern. (b) This requires that all bound names be selected before all free names.
For (a), we might be able to use an approximation: traverse each nt's pattern, intersecting it against the binding patterns. If a variable is always used as a binder, treat it as such. If a variable is never used as a binder, treat it as a reference. Otherwise, enumerate both possibilities, maybe?
For (b), dependent cons might do the trick, as long as forward- and self- references don't exist. They're rare, but they are perfectly legal. The only thing that I can think of to deal with them, though, is to first generate the entire shape of the Redex value ("shape" here means everything but the particular variable names), and only then enumerate over the variable name possibilities.
The shape-first trick would also solve problem (a), I suppose: just match against the shape. And, as long as there exists at least one reference position, there is always an infinite enumeration of possible namings, which I think helps matters?
improve `substitute`'s interface
...make it a metafunction! (but one that uses default-language
, instead of setting it)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.