(http://www.nuprl.org/documents/Constable/Automath-35years.pd...)
RECENT RESULTS IN TYPE THEORY AND THEIR RELATIONSHIP TO AUTOMATH, ROBERT L. CONSTABLE
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...
Som help from type/name inference might help in wiring things togetger.
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?