Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
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.
Re #1, the first of many I hope, Sam!
I have never heard of “defunctionalizing”, do you have any more references?
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 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 by giving the code pointer a sort of “global” or “external” function type:
This seems even closer to using an adjoint functor theorem!
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 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.
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 . The function-space is the presheaf defined by . Is that at all related to defunctionalization? Is it saying something about some kind of embedding being fully faithful?
Yes, I think so. For is a colimit of representables, and working through the usual formulation of that, we get is a quotient of . This looks quite like defunctionalization to me.
This is close to the adjoint functor theorem formation of 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.)
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.
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 . 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: . So in factcps, we do an existential elim to get some , and the type of g is , 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.
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)).
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.
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.
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.
Coming back to #9. atmacen, you said (roughly) “” 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 ) 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 as a coend we can use Max New’s co-Yoneda argument, but that seems difficult to get right.
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.
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 as the terminal object of the category whose objects are types together with morphisms , 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 of all objects of the category and then quotient it by an appropriate relation (in an -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 -types with arbitrary domain, and it “has” -types with arbitrary domain but is not closed under such -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 — it’s a sort of “universe-relative” -type, somewhat analogous to how the (-1)-truncated existential is a “-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 -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.
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 -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.
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).
Matt, your comment in #8 about AFTs seemed rather informal, so I was only going for an intuitive understanding of a relationship to AFTs.
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.
1 to 26 of 26