Wednesday, April 29, 2009

Typed closure conversion

Typed closure conversion is a really lovely explanation of the structure of a closure-converted function. Every closure has its own particular environment structure that binds the particular set of free variables that occur in its body. But this means that if you represent a closure directly as a pair of an environment record and a closed procedure (which is explicitly parameterized over the environment record), then the representations of functions that are supposed to have the same type can end up with incompatible environment types. For example, the program
let val y = 1
in
if true then
λx.x+y
else
λz.z
end
converts naively to the transparent representation
let val y = 1
in
if true then
(λ(env, x).x+#y(env), {y=y})
else
(λ(env,z).z, {})
end
The problem here is the type of the environment has leaked information about the internals of the procedure into the external interface. So Minamide et al use existential types as a nice, lightweight type abstraction for hiding the environment layout as an abstract type. So you instead get the opaque representation
let val y = 1
in
if true then
pack {y:int} with (λ(env,x).x+#y(env), {y=y})
as ∃t.((t × int) → int) × t
else
pack {} with (λ(env,z).z, {})
as ∃t.((t × int) → int) × t
end
Update: fixed the types in the existentials-- since I'm using an uncurried representation the argument type is a pair, not an arrow type.

6 comments:

Paul Steckler said...

That's very nice, but are you guaranteed type-safety? Both closures have the same external type; are they mutually substitutable in the same type context?

I have done some programming with existential types, but in a situation where type constraints forced the witness type to be just what was needed.

In other words, if you messed up your closure conversion algorithm, could you mis-pack the environment, and the type inferencer wouldn't warn you?

-- Paul

Dave Herman said...

Both closures have the same external type; are they mutually substitutable in the same type context?I'm not sure, but I suspect this paper may answer that question.

sjj said...

Dave - whats your feedback on the google proposals re modules on the ecmascript mailing list. You had some good input in this area.

deepika kapoor said...
This comment has been removed by the author.
deepika kapoor said...
This comment has been removed by the author.
deepika kapoor said...

geometry dash apk
netflix mod apk