I just got back from Copenhagen, where I gave a tutorial on gradual typing at the Workshop on Scheme and Functional Programming. I very much enjoyed the workshop and giving the tutorial. Thank you for the invitation Olivier!
For those of you who couldn't be there, this series of blog posts will include the material from my tutorial. For those of you who were there, this series will include some bonus material: an efficient machine for "Eager D" based on recent work by Ronald Garcia and myself.
When I first began working on gradual typing in 2005 and 2006, my focus was on the type system. The main pieces of the type system fell into place that first year, and ever since then I've been thinking about the dynamic semantics. It turns out there are many design choices and implementation challenges regarding the dynamic semantics. In this post I'll restrict my attention to the gradually-typed lambda calculus, as many issues already arise in that setting. I'll quickly review the syntax and type system, then move on to discuss the dynamic semantics.
The following defines the syntax for the gradually-typed lambda calculus. Here I'm writing the dynamic type as ⋆. Also, note that a lambda without a type annotation on its parameter is shorthand for a lambda whose parameter is annotated with ⋆. basic typesB::=Int∣BooltypesT::=B∣T→T∣⋆variablesx,y,zintegersnconstantsk::=n∣true∣falseoperatorsop::=inc∣dec∣zero?expressionse::=k∣op(e)∣x∣λx:T.e∣eeλx.e≡λx:⋆.e
The Gradual Type System and Cast Insertion
The type system of the gradually-typed lambda calculus is quite similar to the simply-typed lambda calculus. The only differences are in the rules for application. Instead of requiring the argument's type to be identical to the function's parameter type, we only require that the types be consistent, written ∼ and defined below. We also allow the application of expressions of type ⋆. typeof(k)=BΓ⊢k:Btypeof(op)=B1→B2Γ⊢e:TB1∼TΓ⊢op(e):B2x:T∈ΓΓ⊢x:TΓ,x:T1⊢e:T2Γ⊢λx:T1.e:T1→T2Γ⊢e1:T1→T3Γ⊢e2:T2T1∼T2Γ⊢e1e2:T3Γ⊢e1:⋆Γ⊢e2:T2Γ⊢e1e2:⋆B∼B⋆∼TT∼⋆T1∼T3T2∼T4T1→T2∼T3→T4
The dynamic semantics of the gradually-typed lambda calculus is not defined in terms of the surface syntax, but instead it is defined on an intermediate language that extends the simply-typed lambda calculus with explicit casts. blame labelsℓexpressionse::=…∣e:T⇒ℓT
Cast insertion is a type-directed translation, so it is the same as the type system with the addition of an output term. typeof(k)=BΓ⊢k⇝k:Btypeof(op)=B1→B2Γ⊢e⇝e′:TB1∼TΓ⊢op(e)⇝op(e′:T⇒ℓB1):B2x:T∈ΓΓ⊢x⇝x:TΓ,x:T1⊢e⇝e′:T2Γ⊢(λx:T1.e)⇝(λx:T1.e′):T1→T2Γ⊢e1⇝e′1:T1→T3Γ⊢e2⇝e′2:T2T1∼T2Γ⊢e1e2⇝e′1(e′2:T2⇒ℓT1):T3Γ⊢e1⇝e′1:⋆Γ⊢e2⇝e′2:T2Γ⊢e1e2⇝(e′1:⋆⇒ℓT2→⋆)e′2:⋆
We often abbreviate a pair of casts (e:T1⇒ℓ1T2):T2⇒ℓ2T3
Design Choices Regarding the Dynamics
Consider the following example in which a function is cast to the dynamic type and then cast to a type that is inconsistent with the type of the function. letf=(λx:Int.incx):Int→Int⇒ℓ0⋆⇒ℓ1Bool→Boolinftrue
- Should a runtime cast error occur during the evaluation of the right-hand side of the let? Or should the runtime error occur later, when f is applied to \textsf{true}?
- When the runtime cast error occurs, which cast should be blamed, ℓ0 or ℓ1? More generally, we want to define a subtyping relation to characterize safe casts (casts that never fail), and the specifics of subtyping relation depend on the blame tracking strategy.
Ron, Walid, and I wrote a paper, Exploring the Design Space of Higher-Order Casts (ESOP 2009), that characterized the different answers to the above questions in terms of Henglein's Coercion Calculus. One can choose to check higher-order casts in either a lazy or eager fashion and one can assign blame to only downcasts (D) or the one can share blame between upcasts and downcasts (UD). The semantics of casts with lazy checking is straightforward whereas eager checking is not, so we'll first discuss lazy checking. Also, the semantics of the D approach is slightly simpler than UD, so we'll start with lazy D. We'll delay discussing the Coercion Calculus until we really need it.
The Lazy D Semantics
We'll define an evaluation (partial) function E that maps a term and environment to a result. That is, we'll give Lazy D a denotational semantics. The values and results are defined as follows: F∈V→cRvaluesv∈V::=k∣F∣v:T⇒ℓ⋆∣v:T1→T2⇒ℓT3→T4resultsr∈R::=v∣blameℓ
To handle the short-circuiting of evaluation in the case of a cast error (signaled by blameℓ), we use the following monadic operators: returnv=vletBX=MinN=caseMofblameℓ⇒blameℓ∣v⇒[X:=v]N
The primitive operators are given their semantics by the δ function. δ(inc,n)=n+1δ(dec,n)=n−1δ(zero?,n)=(n=0)
In lazy cast checking, when determining whether to signal a cast error, we only compare the heads of the types: hd(B)=Bhd(T1→T2)=⋆→⋆
The following auxiliary function, named cast, is the main event. It is defined by cases on the source and target types T1 and T2. The line for projecting from ⋆ to T2 picks the ℓ blame label from the projection (the down-cast), which is what gives this semantics its "D". cast(v,T1,ℓ,T2)=blameℓif hd(T1)≁hd(T2)cast(v,B,ℓ,B)=vcast(v,⋆,ℓ,⋆)=vcast(v,⋆,ℓ,T2)=casevof(v′:T3⇒ℓ′⋆)⇒cast(v′,T3,ℓ,T2)cast(v,T1,ℓ,⋆)=v:T1⇒ℓ⋆cast(v,T11→T12,ℓ,T21→T22)=v:T11→T12⇒ℓT21→T22
The apply auxiliary function performs function application, and is defined by induction on the first parameter. apply(F,v2)=F(v2)apply(v:T1→T2⇒ℓT3→T4,v2)=letBX3=cast(v2,T3,ℓ,T1)inletBX4=apply(v,X3)incast(X4,T2,ℓ,T4)
With these auxiliary functions and monadic operators in hand, the definition of the evaluation function E is straightforward. E(k,ρ)=returnkE(x,ρ)=returnρ(x)E(λx:T.e,ρ)=return(λv.E(e,ρ[x↦v]))E(op(e))=letBX=E(e,ρ)inδ(op,X)E(e:T1⇒ℓT2)=letBX=E(e,ρ)incast(X,T1,ℓ,T2)E(e1e2)=letBX1=E(e1,ρ)inletBX2=E(e2,ρ)inapply(X1,X2)
Exercise: Calculate the output of eval for the example program at the beginning of this post.
Similar to object-oriented languages, we can define a subtyping relation that characterizes when a cast is safe, that is, when a cast will never fail. The following is the subtyping relation for the D semantics. T<:⋆B<:BT3<:T1T2<:T4T1→T2<:T3→T4
Theorem (Subtyping) If the cast labeled with ℓ in program e respects subtyping, then eval(e)≠blameℓ.
The Lazy UD Semantics
One interpretation of the dynamic type ⋆ is to view it as the following recursive type: ⋆≡μd.Int+Bool+(d→d)
Let I be the subset of types that can be directly injected into ⋆: I::=B∣⋆→⋆
The rest of the definitions for Lazy UD are the same as those for Lazy D. The following is the subtyping relation for Lazy UD. With this subtyping relation, the type ⋆ does not play the role of the top element. Instead, a type $T$ is a subtype of ⋆ if it is a subtype of some injectable type I. ⋆<:⋆T<:IT<:⋆B<:BT3<:T1T2<:T4T1→T2<:T3→T4
Theorem (Subtyping) If the cast labeled with ℓ in program e respects subtyping, then eval(e)≠blameℓ.
Exercise: Calculate the output of the Lazy UD eval for the example program at the beginning of this post.
In the next post I'll turn to the efficient implementation of Lazy D and UD.
No comments:
Post a Comment