Represent independent lambdas explicitly in the language

[robrix]

Independent lambdas are ones where some ordering is imposed but it doesn’t actually matter (yet). For example, the pairing function:

pair = λ A : Type . λ B : Type . λ a : A . λ b : B . (a, b)

This tree representation is unambiguous, but awkward; it’s difficult to extract the dependencies. Far from being completely serial, the actual data flow is something like a zip:

pair = zip((λ A : Type . λ a : A .), (λ B : Type . λ b : B .)) {
    (a, b)
}

In particular, if we want to curry the original representation, we can curry A directly, curry another parameter by wrapping in a (nested) closure which applies it at the correct position, or rewrite the function to put the parameter we want at the front, and then curry directly.

Capturing the dependency graph explicitly in the representation would make it easier for us to e.g. erase types/terms for much the same reason: we won’t have to rewrite in order to erase.

[robrix]

@andymatuschak: This occurred to me as kind of a weird example of how ill-prepared we are in general for dealing with graphs: there is no direct representation in λ a . x of whether a occurs free in x or not, let alone where. It’s one vertex of an edge in a directed multi_hyper_graph, but you have to crawl it to recover the other vertices.

Curiously, higher-order abstract syntax actually makes this worse on its own, because although you do away with variables in the AST, you do this by replacing them with functions in the host language which you can no longer inspect at all.