[pilgrim0]

I find this super interesting! The first thing that comes to mind reading the demo code is, perhaps against the purpose, to canonicalize the lookup examples, which in turns evokes that the examples could be expressed by type expressions alone. Which makes me think of a type system that embeds a generalized set of algebraic operations, so that the adder function is one that simply returns the type Number + Number. Those could be semantic operations, beyond the basic mathematical ones, of course. Anyways, just thinking out loud.