Jeremy Siek: Closure Conversion with Polymorphism

[guevara]

Jeremy Siek: Closure Conversion, with Polymorphism



https://ift.tt/2BpGZzU

In the last post, we discussed closure conversion applied to the Simply-Typed Lambda Calculus (STLC), perhaps the simplest language with lexical scoping and first-class functions. Now we turn to closure conversion applied to a richer language, one that includes generics.

The Polymorphic Lambda Calculus (aka. System F)

System F extends the STLC with first-class generics: the ΛΛ expression and an expression for instantiating a generic. typesT::=…∣α∣∀α.Texpressionse::=…∣Λα.e∣e[T]valuesv::=…∣Λα.eframesF::=…∣◻[T]

typesexpressionsvaluesframesTevF::=::=::=::=…∣α∣∀α.T…∣Λα.e∣e[T]…∣Λα.e…∣◻[T]

The expression Λα.eΛα.e creates a generic expression parametrized by the type variable αα. The type of such a generic expression is ∀α.T∀α.T, where T is the type of the inner expression e. The expression e[T]e[T] instantiates the generic e, replacing its type parameter with type T.

The typing rules for System F are those of the STLC plus the following: Γ,α⊢e:TΓ⊢Λα.e:∀α.TΓ⊢e:∀α.T2Γ⊢e[T1]:[α:=T1]T2

Γ,α⊢e:TΓ⊢Λα.e:∀α.TΓ⊢e:∀α.T2Γ⊢e[T1]:[α:=T1]T2

Also, there is one new reduction rule: (Λα.e)[T]⟶[α:=T]e

(Λα.e)[T]⟶[α:=T]e

Updating the Intermediate Language: IL2

With the introduction of generics, we not only worry about lexically scoped term variables but we are also concerned with lexically scoped type variables. So the δδ and γγ functions must be updated to include type variables and their bindings. Furthermore, the closure operator must be extended with type arguments to bind the new type variables. expressionse::=…∣δ¯y:T,¯α,x:T.e∣γx:T,¯y=v,α=T.e∣e{¯e,¯T}

expressionse::=…∣δy:T⎯⎯⎯⎯⎯⎯⎯⎯,α⎯⎯⎯,x:T.e∣γx:T,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e∣e{e⎯⎯⎯,T⎯⎯⎯⎯}

The following are the reduction rules for the functions of IL2. (δ¯y:T,¯α,x:T.e){¯e,¯T}⟶γx:T,¯y=v,α=T.e(γx:T,¯y=v,α=T.e)v⟶[¯α:=T]{¯y:=v}{x:=v}e

(δy:T⎯⎯⎯⎯⎯⎯⎯⎯,α⎯⎯⎯,x:T.e){e⎯⎯⎯,T⎯⎯⎯⎯}(γx:T,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e)v⟶γx:T,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e⟶[α:=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯]{y:=v⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯}{x:=v}e

Next we turn to the ΛΛ. We'll need to translate ΛΛ to something in IL2, and in the spirit of closure conversion, it should be something that does not support lexical scoping. Inspired by the δδ and γγ functions, we create analogous things for generics. expressionse::=…∣Φ¯y:T,¯α,α.e∣Υα,¯y=v,α=T.e

expressionse::=…∣Φy:T⎯⎯⎯⎯⎯⎯⎯⎯,α⎯⎯⎯,α.e∣Υα,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e

The following are the reduction rules for the generics of IL2. (Φ¯y:T,¯α,α.e){¯e,¯T}⟶Υα,¯y=v,α=T.e(Υα,¯y=v,α=T.e)[T]⟶[¯α:=T]{¯y:=v}[α:=T]e

(Φy:T⎯⎯⎯⎯⎯⎯⎯⎯,α⎯⎯⎯,α.e){e⎯⎯⎯,T⎯⎯⎯⎯}(Υα,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e)[T]⟶Υα,y=v,α=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯.e⟶[α:=T⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯]{y:=v⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯}[α:=T]e

Closure conversion for System F

With IL2 in place, the definition of closure conversion for System F is relatively straightforward. The case for λλ computes the free type variables (FTV) and includes them in the δδ function. The new case for ΛΛ is analogous to the case for λλ.

ClosureConversion(e)=let(e′,¯f)=C(e)in(globals¯fine′)

ClosureConversion(e)=let(e′,f⎯⎯⎯)=C(e)in(globalsf⎯⎯⎯ine′)

C(x)=(x,ϵ)C(c)=(c,ϵ)C(op(¯e))=let(¯e′,¯f)=¯C(¯e)in(op(¯e′),¯f)C(λx:T.e)=let(e′,¯f)=C(e)¯y:T=FV(e)−{x}¯α=FTV(e)g=freshname()in(g{¯y,¯α},(g=(δ¯y:T,α,x:T.e′),¯f))C(e1e2)=let(e′1,¯f1)=C(e1)(e′2,¯f2)=C(e2)in(e′1e′2,(¯f1,¯f2))C(Λα.e)=let(e′,¯f)=C(e)¯y:T=FV(e)¯α=FTV(e)−{α}g=freshname()in(g{¯y,¯α},(g=(Φ¯y:T,α,α.e′),¯f))C(e[T])=let(e′,¯f)=C(e)in(e′[T],¯f)

Guru

via siek.blogspot.com https://ift.tt/1GndmOw

December 18, 2018 at 05:02PM