Expresso: A simple expressions language with polymorphic extensible row types
github.com
github.com
For those interested in more of the beautiful theory on extensible row types, this project seems to be based on an earlier paper I wrote on scoped labels: https://www.microsoft.com/en-us/research/wp-content/uploads/...
E.g. a type like:
foo :: r/x => { x :: int | r } -> int
foo r = r.x
Gets translated at runtime to a function where the lacks constraint r/x becomes an actual offset parameter.
There would be no need to think of currying and partial application of functions as it would naturally follow from partially evaluating incomplete record inputs.
Another (nice?) property would be that a value always comes with a name binding. This no need to encode semantics of values purely as positions in lists and tuples.
So a question then to an implementer, is this something you considered? Is feasible?
Som help from type/name inference might help in wiring things togetger.
For example, one can already introduce all the fields of a record as local bindings, e.g.
let {..} = import "List.x"
or just a subset using, e.g.
let {reverse} = import "List.x"
Similarly for function argument bindings, e.g.
f {x, y} = x - y
The above is just syntactic sugar for:
f r = r.x - r.y
Such named arguments of course prevent arguments with the same type being passed in the wrong order, e.g.
f {x=2, y=1}
There is still some minor work to be done to better support inline type annotations on such patterns to make them more usable.
Your idea of unifying bindings with records is interesting and not something I have considered.
Couldn’t find a syntax that made sense though...
(http://www.nuprl.org/documents/Constable/Automath-35years.pd...)
RECENT RESULTS IN TYPE THEORY AND THEIR RELATIONSHIP TO AUTOMATH, ROBERT L. CONSTABLE