Typechecking & parametric polymorphism in cartesian closed categories

Lets examine cartesian closed categories a bit.

Define them first

A cartesian closed category has a terminal object, usually named 1. There is an unique morphism from every object A to terminal object. Lets call these morphisms const. Unit has the rule:

const ∘ f = const

The category also comes with a product A*B, for every object A and B. It's a right adjoint to the diagonal functor, giving the unit dup and counit (fst, snd).

Recall that the counit and unit needs to interact in certain way. It yields these elimination rules:

fst∘dup = a
snd∘dup = a
(fst*snd)∘dup = a

The units and counits are natural transformations means that we have the following rules:

dup∘f = (f*f)∘dup
fst∘(f*g) = f∘fst
snd∘(f*g) = g∘snd

Since the (*) is a functor, we get the composition rule:

(f∘k)*(g∘h) = (f*g)∘(k*h)

To form a closed category there still must be an exponential A^B for every A and B. It's a right adjoint to the (*b) -functor. Call the unit curry and counit apply.

apply ∘ (curry*b) = a
(apply^b) ∘ curry = a

Likewise units/counits being natural transformations yields the rules:

curry ∘ f = ((f*b)^b) ∘ curry
apply ∘ (f^b)*b = f ∘ apply

And the ^ requiring to be a functor yields the composition rule:

(f∘g)^b = f^b ∘ g^b

These are the rules that every cartesian closed category have.

Extra structure

There's some additional structure to this, also likely present in every CCC. I'm just not sure how it's defined exactly.

There's also a contravariant functor (a^). This means that we have the composition rule for right side as well, but it goes in weird direction.

a^(f∘g) = a^g ∘ a^f

The unit and counit have transforms that resemble natural transformations but they are a bit quirky in that they are one-sided.

(a*(c∘f)^b) ∘ curry = (a*c^(f∘b)) ∘ curry
apply ∘ (a^(c∘f))*b = apply ∘ (a^c)*(f∘b)

These rules work but at first sight they are a bit confusing. To illustrate lets examine the following program:

apply ∘ (a^c)*(f∘b) ∘ (a^g ∘ curry)*b

At first sight it'd seem that you'd end up to wrong result where the order of f and g flip around when you apply composition before applying the new rule, but this is not the case.

Recall the result of the composition is reversed and yields:

a^f ∘ a^g = a^(g∘f)

So the transformation must move things sidewise.

It's a bit easier if we recognize that a contravariant functor represents a functor from a dual category.

(a^) : ~C → C

If we treat it this way, then composition is restored:

a^(~g ∘ ~f) = a^(~g) ∘ a^(~f)

And the rules become:

(a*(c∘f)^~b) ∘ curry = (a*c^(~b∘~f)) ∘ curry
apply ∘ (a^(~f∘~c))*b = apply ∘ (a^~c)*(f∘b)

Visually we could think that the letters are flipped around on the right side of the exponential.

This was some detour but it becomes more interesting later on.

Correct application of natural transformations

Now we have bunch of computation rules but if we apply them directly it turns out to behave like untyped lambda calculus. You can construct a fixed point and then unfold it.

apply ∘ pair ∘ (apply ∘ pair ∘ snd)^id ∘ cur ∘ const
= apply ∘   ((apply ∘ pair ∘ snd)^id ∘ cur ∘ const)
          * ((apply ∘ pair ∘ snd)^id ∘ cur ∘ const) ∘ pair
= apply ∘ pair ∘ snd ∘   const
                       * ((apply ∘ pair ∘ snd)^id ∘ cur ∘ const) ∘ pair
= apply ∘ pair ∘ (apply ∘ pair ∘ snd)^id ∘ cur ∘ const

Though fixed point is not a valid composition in the CCC because it relies on an object that can contain itself. Recall the rules for product A*B claim that given A and B, we have A*B. You get the A*B only after you identify A and B.

This also means that cartesian closed category is non-polymorphic. If you say there's a morphism, you must also describe it's domain and codomain -objects.

It also seems that well-reducing programs do not ever need to reduce their parametric parts. This property could be used to partially normalize any untyped program.

All the units and counits are clearly polymorphic. We can say that for every a, the dup is defined as:

dup : a → a*a

Recall that dup is a natural transformation and it's defined as a transformation between functors. Take some object in category C, then the dup states there's a morphism between a and a*a. Take morphism f in category C, then dup reveals that there's a natural transformation that makes these morphisms equal.

dup∘f = (f*f)∘dup

Every natural transformation relates two functors together, so in this way every functors corresponds to a polymorphic type as long as the type forms a functor.

Composition of natural transformations is a valid operation, it yields an another natural transformation. Examine what happens when you duplicate twice.

dup∘dup

The rules still work.

dup∘dup∘f = dup∘(f*f)∘dup = ((f*f)*(f*f))∘dup∘dup

So we start to form a polymorphic language, but it's polymorphic only in an one way.

Functors forming a category

Functors themselves form a category where they participate as morphisms, that category is cartesian closed as well. If you apply the rules directly, the expression to produce pair (a*a) would be.

(*) ∘ dup

But that quite doesn't work with (^) because the other side must be a dual category. Well...

(^) (a*dual) ∘ dup

Of course there's still a question, what's the "dual" here? The conversion into a contravariant is there, but it's not a functor. For now lets imagine that every input come in pairs that contain a category and it's dual. The "dual" flips the pairs. This way we're only handling functors here.

There are some tricky outcomes of these ideas. We can think of natural transformations themselves as structures that behave like functors.

Consider apply and how it transforms morphisms.

apply ∘ (a^(~f∘~c))*b = apply ∘ (a^~c)*(f∘b)
apply ∘ (f^b)*b = f ∘ apply

You can think that apply would break down to structure:

apply(a,b)

Now if you place functions in here:

  f : a → b
  g : x → y

  apply(f,g)
= f∘apply∘(a^~y)*g
= f∘apply∘(a^~g)*x
= apply∘(f^~y)*g
= apply∘(f^~g)*x

In this way you could treat natural transformations as functor-like structures. Though note that composition of natural transformations produce different "pipelines".

dup_apply(h∘f, g) = dup(h) ∘ apply(f,g)

cur_dup(f∘k,g,h∘k) = cur(f,g)*h ∘ dup(k)

Perhaps this is an one way to define valid compositions of natural transformations.

Bidirectional typing with adjoints

Recall that adjoint functors are functor pairs that have unit/counit natural transformations with some constraints.

unit : Id → G.F
counit : F.G → Id

Since the structure is trivial on another side, it's obvious that we can infer towards the domain of unit whereas it's possible to infer towards the codomain of counit.

Counits are structures such as 'fst', 'snd', 'apply', whereas Units are 'dup', 'cur', etc..

This matches the bidirectional typing schemes, except to one case. On products it's possible to infer into both directions. It is needed to capture the split of the context during typechecking.

Limitations of polymorphism in CCC

It seems that functors provide simple forms of polymorphism. Take any bunch of functions, you can plug them into this expression. It's also possible to evaluate these polymorphic programs without filling parameters into them.

CCC are unable to express polymorphic functions though. Consider:

∀a. a → a

But in some crazy sense we have a way to describe this type as a functor:

(∀) ∘ ((^) ∘ (C*dual) ∘ dup ∘ snd)^~C ∘ cur

However this is where cartesian closed categories limit in polymorphism. We can't assume there's more structure that allows to select an one function from a bundle.

Well you can pass natural transformations through functors probably. But CCC sets a certain sort of a floor there.

That's enough for now

Whole lot of ideas in an one post.