# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorSam Staton
• CommentTimeDec 2nd 2018

Attempt at making a page about defunctionalization. My first new page on nlab, I hope there are no faux pas’s. I noticed the resemblance to the adjoint functor theorem a while back, and several people seemed to find it interesting, so I thought I’d make a page.

• CommentRowNumber2.
• CommentAuthorAlizter
• CommentTimeDec 2nd 2018

Can we have some more context where we are working? I am guessing this is just simply typed lambda calculus? What is a functional program? What is a program? Can you give some examples?

• CommentRowNumber3.
• CommentAuthorSam Staton
• CommentTimeDec 2nd 2018

Good point. Linked to functional programming, and included an example, which I think I learnt from Mike Spivey.

• CommentRowNumber4.
• CommentAuthorSam Staton
• CommentTimeDec 2nd 2018
And I know no reason why this wouldn't work in more complicated type theories than simple type theory, with dependent products etc., but I am not an expert on the compilers literature.
• CommentRowNumber5.
• CommentAuthorAlizter
• CommentTimeDec 2nd 2018

OK so I see what this is doing. You basically look at each abstraction and replace it with a constructor for some inductive type Defun. Then you redefine the original “program” to consider values from the inductive type rather than higher order functions?

I’m not completely convinced this has actually gotten rid of any abstractions, morerather it has hidden them in the inductive type. If you expand out the inductive type you will get the abstractions back.

• CommentRowNumber6.
• CommentAuthorSam Staton
• CommentTimeDec 2nd 2018
Thanks! First paragraph: yes, that's right. Second paragraph, I don't fully understand. The result program can be typed in a first order language with no true function type, that's the main point as I understand it.

I used to think it was a syntactic hack, which may be where you are leaning. But several people persuaded me to take it seriously (including Noam Zeilberger, who may have his own take). Now I think it is profound.

For example, recently we addressed the problem that measurable spaces are not cartesian closed, by embedding them in a quasitopos and using adjoint functor theorems. Some programming people said, "why is the lack of function spaces a problem, when we can just defunctionalize". Now my response is, "that is kind-of the same thing as embedding in a bigger category and using AFT".
• CommentRowNumber7.
• CommentAuthorDavid_Corfield
• CommentTimeDec 2nd 2018

Re #1, the first of many I hope, Sam!

• CommentRowNumber8.
• CommentAuthorAlizter
• CommentTimeDec 2nd 2018

I have never heard of “defunctionalizing”, do you have any more references?

• CommentRowNumber9.
• CommentAuthoratmacen
• CommentTimeDec 3rd 2018

Thanks, Sam; this is cool!

Could you write something comparing and contrasting with closure conversion? They’re both implementation techniques for first-class functions, so it’d be nice to see right away the important difference(s). Here are some thoughts about it:

At first glance, it looks like defunctionalization is very inefficient, because of that huge coproduct. But what if you “round up to infinity”? How would you implement an open-ended coproduct of that form? Like a tagged union: elements are tuples that have a tag identifying the lambda, and then all those elements that make up the environment. What should the tag be? It needs to tell $eval$ what code to use, so make it a code pointer. But wait: a code pointer along with an environment is a closure! So from an implementation perspective they’re basically the same, but closure conversion is a more low-level view.

But to handle the type of closures, it does seem like you need to close off the coproduct, or else the type gets more complicated, not simpler. But what if you’re OK with complicated types? In typed closure conversion, they tend to use an (impredicative) existential type to encode a type of closures. The existential is used to sum up over all types, which includes all types of environments, then they narrow it back down to things you can $eval$ by giving the code pointer a sort of “global” or “external” function type:

$\exists \Gamma : type, [\Gamma,A \vdash B] \times \Gamma$

This seems even closer to using an adjoint functor theorem!

• CommentRowNumber10.
• CommentAuthorSam Staton
• CommentTimeDec 5th 2018
• (edited Dec 5th 2018)

Sorry not to reply. I wanted to think about it but didn’t get very far. I suspect that closure conversion means different things to different people, but it is quite close to defunctionalization.

My understanding (and I’m not a compiler hacker) is that traditional closure conversion + lambda lifting would provide, in the factorial example

multiply :: Integer -> (Integer -> Integer) -> Integer -> Integer

multiply x k y = k (x * y)

identity :: Integer -> Integer

identity x = x

But typed closure conversion that you mentioned is a different kettle of fish. People do seem to use the existential type that you wrote, where $[\Gamma, A \vdash B]$ is something very intensional, and so the proper function types disappear (as in defunctionalization).

Blurring that intensional side of it, Max New wrote a blog post about this a short while ago: blog.

So I’m not really sure what to put in the nlab page.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeDec 5th 2018

So what does defunctionalization say at a categorical level? The obvious/naive way to “get function spaces” in a category where you don’t have them already is to apply the Yoneda embedding $y:C\to [C^{op},Set]$. The function-space $(y B)^{y A}$ is the presheaf defined by $(y B)^{y A}(X) = C(A\times X,B)$. Is that at all related to defunctionalization? Is it saying something about some kind of embedding being fully faithful?

• CommentRowNumber12.
• CommentAuthorSam Staton
• CommentTimeDec 5th 2018
• (edited Dec 5th 2018)

Yes, I think so. For $(y B)^{y A}$ is a colimit of representables, and working through the usual formulation of that, we get $(y B)^{y A}$ is a quotient of $\sum_{X,C(A\times X,B)} y X$. This looks quite like defunctionalization to me.

This is close to the adjoint functor theorem formation of $(y B)^{y A}$ as a right adjoint, to my mind at least.

It is maybe another angle on the surprise, which many have pointed out: when we take a cocompletion we get function spaces, even though we didn’t ask for them.

(Of course it may be that you already had some colimits, in which case you might not need to embed in the free cocompletion.)

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeDec 5th 2018

Thanks. Maybe now I understand #6: it’s related to the dichotomy between nice objects and nice categories. If you want a category of “concrete types” without first-class functions (“nice objects”), then to deal with functions you have to encode them up kind of kludgily by defunctionalizing. But by expanding your category to include first-class function types (“nice category”) you don’t have to deal with this, although the types in question become more abstract. And the point is that the resulting “notion of function” is not very different: defunctionalization is just a sort of intensional beta-reduction of the Yoneda embedding of a not-so-nice category of nice objects into a nice category of less-nice objects.

• CommentRowNumber14.
• CommentAuthoratmacen
• CommentTimeDec 5th 2018

Re #10, no, that doesn’t work. You need to be able to get the same type of closure from both identity and multiply, since they’re both used as a continuation for factcps.

Try this:

multiply (x,k,g) y = k g (x * y)
identity _ x = x

factcps x (k,g) = if x == 0 then k g 1 else factcps (x-1) (multiply,(x,k,g))

fact :: int -> int
fact x = factcps x (identity,0)

(This is not valid Haskell; it’s pseudocode. I don’t know the Haskell for existential types.)

The type of factcps’ continuation argument is $\exists \Gamma:type, [\Gamma,int \vdash int] \times \Gamma$. For identity, we use a dummy environment of type int. See that (identity,0) then has the right type, using an implicit existential intro.

The environment type for multiply is more complicated, since it includes another continuation: $\exists \Gamma':type, int \times [\Gamma',int \vdash int] \times \Gamma'$. So in factcps, we do an existential elim to get some $\Gamma'$, and the type of g is $\Gamma'$, and so (multiply,(x,k,g)) is the right type of closure (using two existential intros).

I cheat slightly: actual closure-converted code unpacks closures at the last moment, but I had factcps unpack its closure right away, since it’s notationally convenient.

But typed closure conversion that you mentioned is a different kettle of fish.

I wouldn’t say that typed closure conversion is a whole ’nother story. They just figured out a way to assign types to the implementation technique they were already using.

• CommentRowNumber15.
• CommentAuthoratmacen
• CommentTimeDec 5th 2018

I tested it in Coq with -impredicative-set. I’m a little surprised it passed the termination checker. Here’s the code:

Set Implicit Arguments.
Unset Elimination Schemes.

(* Impredicative existential quantifier *)
Inductive Ex (F:Set->Set) : Set := exI T (x:F T).

Definition exE F (C:Set) (p:Ex F) (k:forall T,F T->C) :=
match p with exI T x => k T x end.

(* Coq didn't like it when I destructured the nested pair in one step. *)
Definition multiply (g:Ex (fun G'=>nat * (G'->nat->nat) * G')%type) y :=
exE g (fun G' g=>let (p,g) := g in let (x,k) := p in k g (x * y)).

Definition identity (g x:nat) := x.

Fixpoint factcps x (g:Ex (fun G=>(G->nat->nat) * G)%type) := exE g (fun G' g=>
let (k,g) := g in match x with
O => k g 1 |
S x' => factcps x' (exI _ _ (multiply,exI _ G' (x,k,g)))
end).

Definition fact x := factcps x (exI _ _ (identity,O)).
• CommentRowNumber16.
• CommentAuthorSam Staton
• CommentTimeDec 6th 2018
• (edited Dec 6th 2018)

Re #13 (Mike). Thanks, nicely put. I agree. I’d even say Set and wCpo are on the “nice categories” side of the fence, whereas categories of games, and free ccc’s are on the nice objects side.

Re #15. Thanks! It can be done in Haskell too — the examples at haskell wiki are similar.

Re #14. In #10 I didn’t write out factcps and fact; what I had in mind was simply

factcps x k = if x == 0 then k 1 else factcps (x-1) (multiply x k)

fact x = factcps x identity

which do typecheck. This is what some people seem to call closure conversion + lambda lifting. The existentially-typed closure conversion of Minamide, Morrisett and Harper is quite a bit more than this, and seems close to defunctionalization — that’s all I meant.

• CommentRowNumber17.
• CommentAuthorDavid_Corfield
• CommentTimeDec 6th 2018

Re #13, it would be good to have a word for the process of shifting from nice objects to nice categories, something like enhancement to a stronger doctrine. Mike’s ideas on n-theories seem very much to the point here.

• CommentRowNumber18.
• CommentAuthoratmacen
• CommentTimeDec 6th 2018

Re #16, your factcps partially applies multiply, so I don’t see that it’s successfully eliminating first-class functions. So I don’t think that it’s closure conversion.

• CommentRowNumber19.
• CommentAuthorSam Staton
• CommentTimeDec 6th 2018
Oops, you're right. Perhaps some people would call it "lambda lifting" but I now agree it's not closure conversion.
• CommentRowNumber20.
• CommentAuthorSam Staton
• CommentTime7 days ago
• (edited 7 days ago)

Coming back to #9. atmacen, you said (roughly) “$B^A \cong \exists \Gamma. [\Gamma,A \vdash B] \times \Gamma$” looks like an adjoint functor theorem. I have been trying to understand what you meant.

Maybe I should understand your sentence as saying that a small complete full subcategory of Set (roughly, one where we can interpret impredicative $\exists$) is necessarily cartesian closed, by a AFT-like argument? Just as every frame is a Heyting algebra? Is that what you had in mind?

If we can interpret $\exists$ as a coend we can use Max New’s co-Yoneda argument, but that seems difficult to get right.

• CommentRowNumber21.
• CommentAuthoratmacen
• CommentTime7 days ago

It could be that I was being too sloppy. Impredicative encodings had seemed similar to the adjoint functor theorem to me, and then I saw Mike Shulman and Steve Awodey talking about a “dream adjoint functor theorem” using impredicative encodings, so I felt bold enough to say that the existential encoding of function types was similar to an instance of some adjoint functor theorem. I don’t know how to work out the details. (Maybe Mike does.)

Maybe I should understand your sentence as saying…

I didn’t mean that much. It seems plausible though, if you additionally require that the subcategory has enough Hom sets (global function types). Oh wait, if it’s a full subcategory of Set, then the Hom sets would already be function types. So that’s probably not a good way to think about typed closure conversion.

There’s a difference, in programming languages, between the global function types of e.g. C, and the fully-featured function types of e.g. ML. But I don’t know how to explain the difference categorically. The difference in typing rules is basically that global function types have an intro form that works only in the empty context. In any case, it seems like the cartesian closedness of ML implemented using closures is not the result of being a full subcategory of anything that’s already cartesian closed. Typed intermediate languages where you’d use typed closure conversion should not be cartesian closed by assumption. But they have impredicative quantifiers, and global function types by assumption.

• CommentRowNumber22.
• CommentAuthorMike Shulman
• CommentTime6 days ago

Let’s see. If cartesian products preserve colimits in each variable (which they do in type theory, because the universal property of colimits applies in any context), then any adjoint functor theorem that applies (in particular, including the ’dream’ one in an impredicative world) implies that the category is cartesian closed. The construction (in the dream world — the ordinary one requires some smallness futzing) is dual to the construction of inductive types as initial objects of categories of algebras: we regard $B^A$ as the terminal object of the category whose objects are types $X$ together with morphisms $X\times A\to B$, and construct such a terminal object as the colimit of the identity functor. To construct such a colimit by coproducts and coequalizers, we would start with the coproduct $\coprod_{X:\mathcal{U}} (X\times A\to B) \times X$ of all objects of the category and then quotient it by an appropriate relation (in an $\infty$-world that “quotient” would be more complex).

The main caveat is that while an impredicative category of modest types has all limits, and hence also all colimits, unlike the limits, the colimits will not in general coincide with those in the ambient universe of types. That is, the impredicative universe is closed under $\Pi$-types with arbitrary domain, and it “has$\Sigma$-types with arbitrary domain but is not closed under such $\Sigma$-types in the ambient universe. So I think your intuition is correct, Matt, as long as we are careful about what we mean by that $\exists$ — it’s a sort of “universe-relative” $\Sigma$-type, somewhat analogous to how the (-1)-truncated existential $\Vert \Sigma_{x:X} Y\Vert$ is a “$\Sigma$-type relative to the universe of propositions”, except that in this case the universe is defined by impredicativity rather than by h-level restrictions. Defunctionalization is sort of “approximating” that by an actual $\Sigma$-type in the ambient universe but over a restricted domain (kind of like the way the non-dream AFT restricts to a small generating family!). Of course in either case one is still missing the quotient to make the coproduct into a colimit.

Comparing these two paragraphs I’m a little worried about whether these universe-relative colimits are also preserved by products in each variable so that we can use the adjoint functor theorem on them, but probably they are since “everything” in type theory can happen in an arbitrary context.

• CommentRowNumber23.
• CommentAuthoratmacen
• CommentTime6 days ago

These typed intermediate languages are usually like intensional type theory in that they don’t have equalizers or coequalizers, and universal mapping properties may not be unique. Function extensionality is too much to hope for. If the coproduct is a weak exponential, you’re done. At least from an implementation perspective; extensionality could be handled setoid style. (And you can’t express the setoids in these languages, so you’d be adding a refinement type system.)

The main caveat is that while an impredicative category of modest types has all limits, and hence also all colimits, unlike the limits, the colimits will not in general coincide with those in the ambient universe of types.

You and Sam seem to be thinking of modest sets in a realizability topos, but that’s probably not how typed intermediate languages were intended to be interpreted. The impredicative quantifiers can be interpreted as meets and joins in the subtyping order. It’s fine if they’re completely different from any $\Sigma$-types you may or may not have from some ambient universe.

I’m a little worried about whether these universe-relative colimits are also preserved by products in each variable so that we can use the adjoint functor theorem on them, but probably they are since “everything” in type theory can happen in an arbitrary context.

The rules for existential types work in an arbitrary context, if that helps.

• CommentRowNumber24.
• CommentAuthorSam Staton
• CommentTime5 days ago

Thanks Mike and atmacen. Some very interesting points. I wanted to add something about typed closure conversion to the article, but I can’t quite see how to do it.

Although the intermediate languages don’t have much structure, presumably one would still like to somehow show that closure conversion is correct, which may amount to giving an AFT-like argument. But I can’t see it immediately in the correctness proof of Minamide, Morrisett and Harper (p 14).

• CommentRowNumber25.
• CommentAuthorMike Shulman
• CommentTime5 days ago

Matt, your comment in #8 about AFTs seemed rather informal, so I was only going for an intuitive understanding of a relationship to AFTs.

• CommentRowNumber26.
• CommentAuthoratmacen
• CommentTime4 days ago

OK, Mike. I was happy to hear that they seem related to you too.

Sam, I was originally just thinking you’d compare defunctionalization to “usual”, untyped (or unsoundly-typed) closure conversion. But I guess we can leave that to Wikipedia. I don’t know what you could add to the page, about typed closure conversion either.

I haven’t read the proofs in that paper, but the introduction makes it sound like they have proofs that the translated programs simulate the source programs. In particular, the translation of a function application (to closure operations) simulates the original beta reduction. So buried in there somewhere is probably the essence of a proof that the existential encoding gets you weak exponentials, if you think of the languages as categories. But it doesn’t look like they’re taking a very categorical perspective on this at all.