Lambda polymorphism as a natural transformation

In my last post I proposed seeing lambda polymorphism as a bifunctor, but this notion seems tio weak. Lambda polymorfism really needs three inputs, but one of them doesn't seem to involve any data in the set sense, only type data, connecting the types. I've tried making this into a category that defined every possible input as an arrow to the right output, but it didn't turn out nicely. 

Instead I'm thinking of turning lambda polymorphism into a natural transformation. This seems promising, because as we all know, a parametrically polymorphic function is always a natural transformation. I will only scetch an example. The Church numeral 4 is applied to the Church numeral 3. Without polymorphism, this would not be possible, because 4 expects a signature * -> * in its first argument, but 3 has signature (* -> *) -> * -> *. We solve this by going by a * -> * functor before we apply the 3. 

The * -> * functor is super simple. It takes every signature S to a signature T where T is exactly what you get if you replace every * in S with (* -> *) and remove any extraneous parentheses that would be implied by the right associativity of ->. Arrows are equally easy. Just pick the arrow indicated by the original function. 


Now, in order to be applied to 3, 4 goes by the * -> * functor from its original signature (* -> *) -> * -> * to ((* -> *) -> * -> *) (* -> *) -> * -> *. Since 3 has the same signature as the first argument, the application is valid, returning the remaining (* -> *) -> * -> *. As expected, this is a Church numeral, incidentally 3^4 = 81. I'll explain why later, but there is a half hearted explanation on Wikipedia.

Remains to see if this definition proves fruitful.

The natural transformation I am talking about goes from the identity functor to the polymorphism functor (* -> * in this case). The arrow of the identity functor "remembers" that this the element 4 in the set of Church numerals. 3 will have to be pointed out somehow in the domain pointed out by the natural transformation. This way, the natural transformation can "store" both it's function and it's input in the point of its output. I think I might have to redefine the arrows of the category for this to work, though. I will get back to that.

Kommentarer

Skicka en kommentar

Populära inlägg i den här bloggen

The category of lambda calculus with products and coproducts

Normal Forms and Cut-Free Proofs as Natural Transformations by Girard, Scedrov and Scott seems to have what I have been looking for. My interpretation: (simply typed) Lambda calculus with products can be expressed as natural deductions (with parcels and products) via the Curry-Howard isomorphism. Natural deductions can in turn be expressed by left sequent logic (with products). Sequent logic can always be rewritten in a way that is cut free. The main result of the paper is that all rules in left sequent logic (with products), except the cut rule, can be interpreted in any Cartesian closed category. Further, these interpretations can be inductively proven to be dinatural.  I think cut free left sequent logic corresponds to simply typed lambda calculus in normal form where all free variables in all subexpressions have been bound and uncurried, so the passive context of the sequent represents a tuple with the needed unbound variables in the subexpression. Notably, they have been kind ...
Läs mer

The Lambda Polymorphism (bi?) functor

So, I’m trying to think about how to define a category for lambda calculus. I’m thinking of a category that has as objects all the lambda function signatures and as arrows “the set of all lambda functions” somehow related by the domain and codomain signature. I am not sure exactly how to define the arrows, but currently it is much like Set, so all objects (except * and possibly some initial and terminal objects) are exponential objects. To create the exponentials, products are needed, but they are merely cartesian products, and exponentials are defined using the curry-uncurry isomorphism, as in Set. Let S be a non product signature with n inputs of signatures  s1, s2, … , sn,  so that  S = s1 -> s2 -> … - > sn -> *.  and T another non-product signature. Then the homset Hom(T, S) is the set of all lambda functions of signature T -> s1 -> s2 -> … - > sn -> *. If S is a product UxV, the arrows are pairs of arrows  from Hom(T, U) and Hom(T...
Läs mer

The universal arrow of the exponential object for combining function and input

I have no idea how this should be done, but I am pretty certain (right now) that it is the way forward. As described in my first post, (almost) all objects in the lambda category are exponential objects of each other. The (possibly Cartesian product) contravariant part denotes the input, and the covariant part denotes the (probably curried) output. In Set, the universal arrow of the exponential object denotes how a pair of function and input is related to the output. The trick is to do the same thing in the lambda category. Next we have to consider that the function object is lifted by a (possibly identity) natural transformation before it is applied to the input, as described in the previous post. I don't know how yet. It will probably make sense to define a category were objects are exponentials, points of the objects denote the current function of the application chain and arrows are a pairs of a natural transformation and an input object of the right signature fed to the evalua...
Läs mer