Lambda the Ultimate

I’m looking at type theory from point of view of the general-purpose programming language evolution, and I’ve found something that does not look nice.

There is stage when function pointers like ones in C were introduced to the languages. Differently from lambdas they are stateless and they could be only evaluated using their explicit arguments and using only constants (or global state) and by calling other stateless functions. Their type will be designated as:

T ⇨ A

Now let’s take usual lambdas, their type will be designated as:

T → A

The relationship between these two types is the following:

A → B = ∃ T (T ⨉ (T ⨉ A ⇨ B))
apply:  (A → B) ⨉ A ⇨ B = ? ((t, f), a), f(t, a) // unpacking existential type here
curry: ((A ⨉ B) → C) ⇨ (A → B → C) = ?(t, f) ((t, f), (?((t1, f1),  a1) ((t1, f1, a1),  (?((t2, f2, a2), b2)  f2(t2, (a2, b2))))))

Such definition is needed to support currying and to capture implicit environment, and it reflects what is actually happens in the code. Every function from T ⇨ A could be trivially converted to T → A, however stateless functions have different set operations supported. Particularly, currying is not supported. So, it is not subclass, but a separate entity type.

This existential type captures difference between structured programming paradigm and object-oriented or functional programming paradigms. So, theoretically, when we would try to study paradigms, we would also need to make this distinction.

I’m interested if there are some research papers that describe this distinction. The discussion in the TaPL book is somewhat unsatisfying because explicit existential types are defined using implicit existential types. Theoretically, the type theory should start from stateless functions to reflect evolution path rather than in reverse direction. Such point of view might be also useful for the compiler transformation reasoning, so there might be papers on such equivalence in that area too.