Gradual typing using union typing with records

Abstract

Dynamic typed languages are characterized by their expressiveness and exibility to develop prototypes, while static typed languages allow early detection of errors and the optimization of source code. Gradual typing languages allow programmers to make use of both approaches, static and dynamic typing, and thus, obtaining the advantages that both represent. The objective here is to revisit the static part of the approach to a gradual interpretation of union types based on the design of Gradual Union Types through an extension with the record data-structure. This contributes to understand the abstraction and reasoning behind Gradual Typing in order to have useful future extensions for other data-structures.

Keywords

• Gradual typing
• Union types
• Records

-

Introduction Commonly, programming languages can be broadly categorized according to their typing as static or dynamic. Nevertheless, there are other typing classi

cations that allow to mix typing features between both static and dynamic extremes, such as hybrid typing and gradual typing [ 15 ]. In particular, gradual typing languages allow programmers to make use of static and dynamic typing, and thus, obtaining the advantages that both represent.

Gradual typing makes use of typed and untyped code in the same language.

The idea has been proposed by Siek and Taha in 2006 [ 15 ], who expose the idea that mixing dynamic and static features in a single language may improve the intrinsic typing characteristics of such a programming language. Having explicit types can guarantee certain properties about the program, related with its soundness and security, and thus, certain kind of optimizations can be performed during of executable code, since some typing information is already known. Moreover, not having explicit types allows programmers to have a better expressiveness, and generate prototypes of programs faster to test and execute.

Since Siek and Taha introduced the term Gradual Typing [ 15 ], several other studies have been performed which encompass Gradual Typing with type security [ 5 ], type states [ 8 ], Object-Orientation [ 14,18 ], and so on. AlthCooupygrhightht©e 2019 for this paper by its authors. interest for Gradual Typed languages has been increased over the last Afetwtribution 4.0 International (CC BY 4.0) years, there are still questions about how more sophisticated language features can be included into them [ 7 ].

In their original work, Siek and Taha [ 15 ] start from a language which is statically typed to obtain a gradual system by adding the character ? to express an unknown type. Having this type enforces the static properties of the system as gradual types represent static information, in this way gradual typing supports static and dynamic checking of program properties [ 2 ]. Programmers can explicitly write static types, as well as leave some parts of the code without typing. A type that has not been de ned as \static" by the programmer should be veri ed at run-time, and gradual type systems should be developed in order to preserve type consistency.

The relation of consistency has a signi cant importance in this approach, because it must be guaranteed that programs do not fail, that is, if they reach an unsoundness state. The relation of consistency has to be maintained, even when the unknown type ? of Gradual Typing is present [ 7 ]. A consistency relation is given to extend conservatively the type equality: T T 0 expresses that during run-time, T is structurally equal to T 0 with the exception of some features but mainly to do not allow any type inconsistency.

Robustness of usual extensions of functional languages are based on the preservation of fundamental properties such as security. A meta-theory, as presented by Toro and Tanter allows to extend a language into a gradual one in a safe manner: the gradual union of types and the unknown type ? are combined through the Abstract Gradual Typing (AGT) methodology. The AGT is based on abstract interpretation due to [ 4 ], for a sound abstraction using Galois connections. Abstract Interpretation describe the computations made in a given system but in a di erent universe. For example, the elements in a program and their operations can be modeled in another language, preserving their semantics.

We present an extension of a functional language with records. Such an structure allows the programmer to manipulate expressions that could have di erent types. The gradual extension is cartied out with gradual union types, which are intended to preserve the safety property. In this paper the extension of the type system is provided in order to understand the abstraction behind the AGT methodology, as proposed by [ 19 ]. 2

Gradual Union Typing Some proposals have been made to address the inexactness introduced by the unknown type ? of Gradual Typing languages. Two are mainly used [ 19 ]: 1. The use of disjoint (or tagged) types, such as the sum of the types T1 + T2

explicitly tagged; and 2. Untagged union types, denoted by T1 _ T2, which denotes the union of values of type T1 and of type T2.

Toro and Tanter combine these two proposals into a Gradual Union Typing (GUT) approach, in which it is possible to have the two di erent types of union: disjoint (also known as tagged) union types, and untagged union types.

Mixing tagged and untagged unions in a language is named as optimistic type checking [ 19 ] to ensure that statically any term will have a type. In particular, optimistic type checking means that some statement is well typed without the occurrence of any explicit projection or case analysis.

An Abstract Gradual Interpretation of union types is presented in order to understand both proposals for the union of types. Thus, it is possible to mix both: disjoint (also known as tagged) union types (T1 + T2) and their variant types, as well as untagged union types (T1 _ T2): { Disjoint union types or tagged unions (T1 + T2) denote values of di erent types. It is called disjoint because some elements are explicitly tagged, so the type system recognizes the type of each element. Hence, it guarantees and ensures the type of each element during compilation and execution time. { Untagged unions (T1 _ T2) denote the unions of values of types T1 and T2 without any tagging mechanism. For example, a value v of type T1 is included as a value of type T1 _ T2, that is, the type of value v appears in the union of both sets of types T1 and T2, i.e. the highest lower bound between T1 and T2. Untagged unions can be used in the branches of conditionals inside of an if expression, where then and else branches can return a di erent type of values. Thus, untagged unions can be safely compiled, but can lead to errors during execution time. 2.1

A Gradual Interpretation of Union Types

Toro and Tanter, based on the AGT methodology, propose static semantics for a Gradual Typed Functional Language, which make use of gradual unions and unknown typing. The notion of gradual union types is to restrict the imprecise types to denote a nite number of static types [ 19 ]. Such a semantic is based on the Simply-Typed Functional Language (STFL), which is statically typed.

Types of a Gradual Type Functional Language (GTFL ) as de ned by Toro and Tanter [ 19 ] extends the STFL syntax by adding the symbol ?, introduced as the unknown type. This type is present in the Gradual Type Functional System (GTFL) [ 7 ], which preserves the STFL structure, but static types, predicates, and partial functions are lifted to gradual types. This transformation between sets of static types and gradual types is based on a Galois connection as the AGT approach states.

In this paper, the extension with records is carried out using this methodology [ 19 ]. The rst transformation uses an abstraction function ? to convert STFL into an GTFL, and a concretization function ? from GTFL to STFL to complete the Galois connection. Second step is to obtain a GTFL from GTFL by adding the gradual union denoted by: T1 T2 and using and functions between these two languages for the Galois connection.

For the purposes of this paper, the left side of Figure 1 shows the lifting of the types on STFL, which is expressed by the in nite power set }(T Y P E), to the syntactic category GTYPE using functions ? and ?. From these sets, it is necessary to lift the set of types into a nite one, this implies the use of the power set operator }. Then, functions ? and ? are de ned between }fin(}(T Y P E)) õ ô and }fin(GT Y P E) [ 19 ].

Gradual Union Types with Records This paper extends the GUT by Toro and Tanter with records. A record is a datatype that describes variables (called elds) and their values. Fields possibly have di erent types. Some programming languages use records to de ne new types, and therefore, are able to extend the language [ 6,12 ]. A record is composed by one or more labels, here denoted as `. Each label has an assigned term, which also has a type. Adding records allows to extend a language maintaining complex information in the same structure, and having the possibility to access it through an identi er of each one of its elds. The extension here presented is based on the system of Toro and Tanter [ 19 ] and is given in Figure 2. The system adds records as primitive types (shown in boldface) where the labels `i belong to a predetermined set LABEL.

From Figure 2, a record type is denoted by [`i : Ti i21;:::;n], where `i denote a label. A record term is expressed as [`i = ti i21;:::;n], where `i denotes a eld for term ti and a record value is de ned as [`i = vi i21;:::;n] where each vi is a value. Each record has a xed size n. The typing rules for records are Trec and Tproj , following the typing rules given in [ 12 ]: Trec: in order to assign a type to a record term, if each term ti has type Ti under , then term [`i = ti i21::n] has type [`i : Ti i21::n], in the same context .

T ::= Int j Bool j T ! T j [`i : Ti i21::n] v ::= n j b j x : T:t j [`i = vi i21::n] 2 V AR *n T Y P E; ` 2 LABEL

(type) (values) t ::= v j x j t t j t + t jif t then t else t j t :: T j [`i = ti i21::n] j t:`j (terms) x : T 2 ` x : T (Tx)

` n : Int ` t2 : T2 ` t1 : T1 T2 = dom(T1)

` t1 t2 : cod(T1) ` t1 : T1 T1 = Int ` t2 : T2 T2 = Int

` t1 + t2 : Int ` t1 : T1 T1 = Bool ` t2 : T2 ` t3 : T3

` if t1 then t2 else t3 : equate(T2; T3) ; x : T1 ` t : T2

(T ) ` ( x : T1:t) : T1 ! T2 ` t : T T = T1 ` (t :: T1) : T1

(Tapp) (Tn) ` b : Bool (T+) (Tif ) (Tb) (T::) ` ti : Ti i21::n

f or each i ` [`i = ti i21::n] : [`i : Ti i21::n]

` t : [`i : Ti i21::n] ` t:`j : Tj f or some j 2 1::n (Trec) (Tproj ) dom:T Y P E*T Y P E cod:T Y P E*T Y P E equate:T Y P E T Y P E*T Y P E dom(T ) undefined in other case cod(T ) undefined in other case equate(T1;T2) undefined in other case ` [`i = ti i21::n] : [`i : Ti i21::n] then ` t:`j : Tj f or some j 2 1::n then

` ti : Ti f or each i 2 1::n.

` t : [`i : Ti i21::n]. 3.1

A Gradual Typing Language

The following step is to add records for a Gradual Typing Language (GTFL). This means adding the unknown type ? to the STFL. In the following, we present the extension with records based on the work of [ 19 ], the new cases are in boldface:

G 2 GT Y P E

G ::= Int j Bool j G ! G j ? j [`i : Gi i21::n] The concretization function is de ned as follows: ?(Int) = fIntg ?(Bool) = fBoolg ?(?) = T Y P E ?(G1 ! G2) = fT1 ! T2 j T1 2 ?(G1) ^ T2 2 ?(G2)g ?([`i : Gii21::n]) = f[`i : Tii21::n] j Ti 2 ?(Gi) i21::n]g

Notice that the above function helps to preserve (i.e. to know) the static information of gradual types [ 19,7 ]. The case for ?(?) = T Y P E states that the unknown type could be any of the types in the category T Y P E de ned in STFL.

The abstraction function, following [ 19 ], is de ned using Tó which denotes a set of types induced by T :

Tü1! T2 = fT 0 ! T 00 j T 0 2 Tõ1 ^ T 00 2 Tõ2g [`i ÿTii21::n] : = f[`i : Ti;j i21::n] j Ti;j 2 Gõi ^ i 2 1::n ^ j 2 1::jGõijg ?(fT g) = T ?(Tü1! T2) = ?(Tõ1) ! ?(Tõ2) ?(;) = undef ined ?([`i ÿTii21::n]) : = [`i : ?(Tõi) i21::n] ?(Tó) = ? otherwise

Th abstraction function ? helps the language to obtain or retain more precision, while the unknown type is decreased, that is, the ? function can produce a gradual type that abstracts a given set [ 7 ]. Toro and Tanter de ne optimal as the best approximation of ?, that means the most precise gradual type that is possible. Both functions ? and ? de ne the Galois connection [ 19 ]. De nition 1 (GT Y P E Precision). G1 is less imprecise than G2, G1 v G2, if and only if ?(G1) ?(G2).

The next proposition de nes when ? is sound and optimal.

Proposition 1 ( ? is sound and optimal). If Tó is non empty, then:

1: Tó ?( ?(Tó)) 2: Tó ?(G) =) ?(Tó) v G Proof. Proof by induction on the structure of G, we show the case for records.

Case 1 for records ([`i þTii21::n]) :

If Tó = [`i ÿTii21::n] : = f[`i : Ti;j i21::n] j Ti;j 2 Tôi ^ i 2 1::n ^ j 2 1::jTôijg then by de nition of ?: ?([`i ÿTii21::n]) : = [`i : ?(Tôi) i21::n] and by de nition of ? for records we have ?([`i : Gi i21::n]) = f[`i : Ti i21::n] j Ti 2 ?( ?(Tó)) = ?([`i : ?(Tôi) i21::n]) = ?(Gi) i21::ng = f[`i : Ti i21::n] j Ti 2 ?( ?(Tôi)) i21::ng. By induction hypothesis Ti;j 2 Tôi then the result holds.

Case 2 for records ([`i þTii21::n]) :

Let Tó = [`i ÿTii21::n], : and suppose Tó = [`i ÿTii21::n] : and by de nition of ?: f[`i : Ti i21::n] j Ti 2 ?(Gi) i21::ng ?( ?(Tôi)) for each Ti;j ?([`i : Gi i21::n]) By de nition of ? for records: ?([`i ÿTii21::n]) : = [`i : ?(Tôi) i21::n] By the induction hypothesis, for each Tôi if Tôi ?(Gi) then ?(Tôi) v Gi.

Therefore, by de nition 1 ?( ?([`i ÿTii21::n])) : = ?([`i : ?(Tôi) i21::n]) ?([`i : Gi i21::n]) and the result holds.

The next step to give a Gradual Union Typing is to lift functions ? and ? to sets, that is from }fin(}(T Y P E)) to }fin(GT Y P E) and vice-versa. Observe that this lifting is over nite sets of types. We follow again Toro and Tanter [ 19 ].

De nition 2 (}fin(GT Y P E) Concretization).

? : }fin(GT Y P E) ! }fin(}(T Y P E)) is de ned as: ô?(Gô) = f ?(G) j G 2 Gôg ô

De nition 3 (}fin(GT Y P E) Abstraction).

? : }fin(}(T Y P E)) * }fin(GT Y P E) is de ned as: õ õ?(;) = undef ined õ?(Tôô) = [

?(Tó) Tó2Tóó Proposition 2 ( ? is sound and optimal). If Tôô is non empty, then: õ 1: Tôô ô?(õ?(Tôô)) 2: Tôô ô?(Gô) =) õ?(Tôô) v Gô Proof. The proof is the same as in [ 19 ] as we are working with sets. An important observation is that Tôô is indeed a Gô. 3.2

A Gradual Union Typing Language

In order to construct a Gradual Union Typing, it is proposed in [ 19 ] a ST Y P E grammar for the static types. This grammar is made up only of gradual unions (without the unknown type ?).

S 2 ST Y P E

S ::= Int j Bool j S ! S j S

S j [`i : Si i21::n]

The static types are integers (Int), booleans (Bool), functions (S ! S), the gradual unions denoted by S S and the record type. Recall that gradual unions represent a nite set of types [ 19 ], where the concretization and abstraction functions are de ned between static types and nite sets of types generating a Galois connection.

For a gradual interpretation of union types with records, the next step is to design gradual union types, using the AGT to construct the semantics for gradual types in terms of pre-existing sets of static types.

The new type system is composed of Gradual Unions , named GTFL , combining both ST Y P E and U T Y P E. The last syntactic category, U T Y P E, is the extension including the unknown type, the gradual unions and records: U 2 U T Y P E

U ::= Int j Bool j U ! U j U

U j ? j [`i : Ui i21::n]

We de ne a Galois connection between U T Y P E and }fin(GT Y P E) as the next concretization function in U T Y P E [ 19 ]. The extension with records is again expressed in boldface: De nition 4 (U T Y P E concretization).

: U T Y P E ! }fin(GT Y P E) (Int) = fIntg (Bool) = fBoolg (?) = f?g (U1 ! U2) = fG1 ! G2 j G1 2 (U1) ^ G2 2

(U2)g (U1

U2) = (U1) [ (U2) ([`i : Ui i21::n]) = f[`i : Gi i21::n] j Gi 2 (Ui) i21::ng

The de nition of abstraction function (U T Y P E abstraction) is the same de ned by Toro and Tanter [ 19 ] and produces nite sets, that is the gradual union of all elements in Gô: De nition 5 (U T Y P E abstraction).

: }fin(GT Y P E) * U T Y P E (Gô) = L G

ô = (G1) (G2) : : : (Gm) if G 6= ; where Gi 2 Gô and jGönj = m.

To prove that Gô

The next proposition states that is sound and optimal for U T Y P E. The notion of precision for U T Y P E is the same as the one given above, that is U1 v U2 if and only if (U1) (U2) Proposition 3. (

is sound and optimal). If Gô is non empty, then: 1: Gô ( (Gô)) 2: Gô Proof. The proof is carried out by induction on the structure of U .

Case 1 for records.

Suppose G = [`i : Gi i21::n] then Gô = f[`i : Ti;j i21::n] j Ti;j 2 Gõi ^ i 2 1::n ^ j 2 1) 1::jGõijg. Without loss of generality, take j = 1 for each Gõi with i 2 1::(n (f[`i : Ti; `n : T 0] j T 0 2 Gön ^ i 2 1::n ( (Gô)) we proceed by applying the de nition of 1g) =

(Gô): L f[`i : Ti; `n : T 0] j T 0 2 Gön ^ i 2 1::n 1g = [`i : (Ti); `n : (Gn1)] : : : [`i : (Ti); `n : (Gnm)] Using de nition of : ([`i : (Ti); `n : (Gn1)] [`i : (Ti); `n : (Gnm)]) = ([`i : (Ti); `n : (Gn1)]) [ [ ([`i : (Ti); `n : (Gnm)]) = f[`i : ( (Ti)); `n : ( (Gn1))]g[ [f[`i : ( (Ti)); `n : ( f[`i : ( (Ti)); `n : Gnj] j Gnj 2 ( (Gön)) ^ j 2 1::mg: By induction hypothesis, Ti 2 Gõi and also belongs to ( (Gõi)) for each i 2 1::n 1 and Gnj 2 Gön belongs also to ( (Gön)) and therefore Gô ( (Gô)).

Case 2 for records.

Suppose that Gô (U ) where Gô = [`i ÿGii21::n] : and

(U ) = ([`i : Ui i21::n]) = f[`i : Gi i21::n] j Gi 2 (Ui) i21::ng To prove (Gô) v U we proceed by de nition of (Gô): ([`i ÿGii21::n]) : = Lf[`i : Ti;j i21::n] j Ti;j 2 Gõi ^ i 2 1::n ^ j 2 1::jGõijg Without loss of generality, take j = 1 for each Gõi with i 2 1::(n 1) and jGönj = m, then by de nition of

(f[`i : Ti; `n : T 0] j T 0 2 (Gön) ^ i 2 1::n 1g) = S (f[`i : Ti; `n : T 0] j T 0 2 (Gön) ^ i 2 1::n 1g) = Sf[`i : Ti; `n : T 0] j T 0 2 ( (Gön)) ^ i 2 1::n 1g The induction hypothesis states that Gõi (Ui) =) (Gõi) v Ui for each i which by de nition of precision gives ( (Gõi)) (Ui), in particular for Gn. Therefore Sf[`i : Ti; `n : T 0] j T 0 2 (Ui) ^ i 2 1::n 1g which is indeed f[`i : Gi i21::n] j Gi 2 (Ui) i21::ng.

Therefore, following Toro and Tanter [ 19 ], the strati ed interpretation of U T Y P E is de ned in terms of sets of sets of static types with the composition of two presented Galois conections:

De nition 6 (U T Y P E concretization).

: U T Y P E ! }fin(}(T Y P E)) = ? ô (Gnm))]g =

De nition 7 (GT Y P E abstraction).

: }fin(}(T Y P E)) * U T Y P E ? õ The next proposition is needed to prove that is sound and optimal: = Proposition 4. ( is sound and optimal). If Tôô is non empty, then: Proof. This proposition holds by Propositions 1, 3, and composition of sound and optimal abstractions. U 2 U T Y P E; x 2 V AR; et2 U T ERM;

U ::= U U j Bool j Int j U ! U j ? j [`i : Uii21::n] (types)

v ::= n j true j f alse j ( x : U:et) j [`i = vii21::n] (values) et::= v j x j etetj et+ etj if etthen etelse etj et:: U j [`i = tei j21::n] j te:`j (terms) x :`Ux2: U (Ux) ` n : Int (Un) (Ub) ; x : U1 ` et: U2 (U ) (U::) ` ( x : U1:et) : U1 ! U2

` te1 : U1 ` te1 : U1 U1

` te2 : U2 U2 ` te1 te2 : cÝod(U1)

Int ` te2 : U2 U2

Int ` te1 + te2 : Int ` te1 : U1 U1 Bool ` te2 : U2 ` te3 : U3 ` if te1 then te2 else te3 : U2 u U3

` tei : Ui i21::nf or each i ` [`i = tei i21::n] : [`i : Ui i21::n]

` te : [`i : Ui i21::n] ` te:`j : Uj f or some j 2 1::n

(Urec) (Uproj)

` b : Bool ` et: U U U1 ` (et:: U1) : U1 dÞom(U1) (Uapp) (U+) (Uif ) dÝom:UT Y P E*UT Y P E cod:UT Y P E*UT Y P E

f dÝom(U)= (dom( (U)) cfod(U)= (cod( (U))

Ó c De nition 8 (Gradual Meet). Let u : U T Y P E * U T Y P E be de ned as:

8 U u U1 if U u U2 is undef ined 3. U u (U1 U2) = (U1 U2) u U = < U u U2 if U u U1 is undef ined : (U u U1) (U u U2) otherwise 4. (U11 ! U12) u (U21 ! U22) = (U11 u U21) ! (U12 u U22) 5. [`1 : U11; :::; `n : U1n] u [`1 : U21; :::; `n : U2n] = [`1 : (U11 u U21); :::; `n : (U1n u U2n)] 6. U1 u U2 is unde ned otherwise.

The following de nition states the translation of the equate from STFL to a function in GTFL , in order to preserve typing:

De nition 9 (Equate Lifting).

eàquate(U1; U2) = U1 u U2 =

(fTõ1 \ Tõ2 j Tõ1 2 (U1); Tõ2 2 (U2)g) = (feáquate?(G1; G2) j G1 2 (U1); G2 2 (U2)g)

And the next proposition is needed to prove the gradual meet for GT F L Proposition 6. u =

eúúquate Proof. Proof is made using structural induction and the de nition of meet as intersection of sets of sets [ 19 ]. The case for records is straightforward as the meet is pointwise. 4

Conclusion and Future Work Gradual Union Typing was initially proposed by Toro and Tanter [ 19 ], showing properties such as safety and consistency using AGT and Galois connections. Nevertheless, there has been investigated a lot of settings related to gradual typing in order to promote the development of more expressive programming languages. For instance, subtyping by Garc a, Siek and Taha [ 14,7 ], Gradual Typing systems and cast insertion procedures by Cimini and Siek [ 3 ], the interaction between union types and Gradual Typing [ 16,1 ], typestates [ 8 ], re nement types [ 11 ], information- ow security typing [ 5 ], set-theoretic types and subtyping [ 2 ], re nement sums for exhaustive and non-exhaustive matches [ 10 ], and studies focused on performance at run-time and space management [ 13,9 ].

The type setting here provides a static extension using records for the study of Gradual Union Typing, as presented by Toro and Tanter in [ 19 ]. This approach contributes to the study of the theoretical perspective for the foundations of programming languages. Adding records to a functional language allows to create new variants of types, using them as basic types prede ned in the language, for a richer and more versatile language. Extending the methodology for languages with gradual typing helps to combine the advantages of using both static and dynamic typing, while preserving the properties of consistency and security in it.

A related work from Garcia, Clark and Tanter [ 7 ] proposes an extension of a type system with records using subtyping, and formalizing a relation of consistency on gradual typing language, by following the methodology proposed by Siek and Taha [ 15 ]. Our approach here di ers from theirs as we rely on gradual union types. Here it is already provided a static formal system. Further, the dynamic formal part, demonstrating its static and dynamic semantics properties, is aimed as future work. The main goal is to obtain a gradual system with records using the so-called Threesome Calculus [ 17 ] for the dynamic semantics.

References

1. Castagna , G. , Lanvin , V. : Gradual typing with union and intersection types . Proceedings of the ACM on Programming Languages 1(ICFP) , 41 ( 2017 )

2. Castagna , G. , Petrucciani , T. , Nguy~en, K.: Set-theoretic types for polymorphic variants . In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming . pp. 378 { 391 . ICFP 2016 , ACM, New York, NY, USA ( 2016 )

3. Cimini , M. , Siek , J.G. : The gradualizer: a methodology and algorithm for generating gradual type systems . ACM SIGPLAN Notices 51 ( 1 ), 443 { 455 ( 2016 )

4. Cousot , P. , Cousot , R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation . In: FPCA . vol. 95 , pp. 170 { 181 ( 1995 )

5. Disney , T. , Flanagan , C. : Gradual information ow typing . In: International workshop on scripts to programs ( 2011 )

6. Friedman , D.P. , Wand , M. , Haynes , C.T.: Essentials of programming languages . MIT press ( 2001 )

7. Garcia , R. , Clark , A.M. , Tanter , E.: Abstracting gradual typing . In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . pp. 429 { 442 . POPL '16, ACM , New York, NY, USA ( 2016 )

8. Garcia , R. , Tanter , E. , Wol , R. , Aldrich , J.: Foundations of typestate-oriented programming . ACM Transactions on Programming Languages and Systems (TOPLAS) 36(4) , 12 ( 2014 )

9. Herman , D. , Tomb , A. , Flanagan , C. : Space-e cient gradual typing . Higher-Order and Symbolic Computation 23 ( 2 ), 167 ( 2010 )

10. Jafery , K.A. , Dun eld , J.: Sums of uncertainty: Re nements go gradual . ACM SIGPLAN Notices 52 ( 1 ), 804 { 817 ( 2017 )

11. Lehmann , N. , Tanter , E.: Gradual re nement types . In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages . pp. 775 { 788 . POPL 2017 , ACM, New York, NY, USA ( 2017 )

12. Pierce , B.C. , Benjamin , C. : Types and programming languages . MIT press ( 2002 )

13. Rastogi , A. , Swamy , N. , Fournet , C. , Bierman , G. , Vekris , P. : Safe &# 38 ; e - cient gradual typing for typescript . In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . pp. 167 { 180 . POPL '15, ACM , New York, NY, USA ( 2015 )

14. Siek , J. , Taha , W. : Gradual typing for objects . In: European Conference on ObjectOriented Programming . pp. 2 { 27 . Springer ( 2007 )

15. Siek , J.G. , Taha , W. : Gradual typing for functional languages . In: Scheme and Functional Programming Workshop . vol. 6 , pp. 81 { 92 ( 2006 )

16. Siek , J.G. , Tobin-Hochstadt , S.: The recursive union of some gradual types . In: A List of Successes That Can Change the World , pp. 388 { 410 . Springer ( 2016 )

17. Siek , J.G. , Wadler , P. : Threesomes, with and without blame . In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . pp. 365 { 376 . POPL '10, ACM , New York, NY, USA ( 2010 )

18. Takikawa , A. , Strickland , T.S. , Dimoulas , C. , Tobin-Hochstadt , S. , Felleisen , M. : Gradual typing for rst-class classes . In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications . pp. 793 { 810 . OOPSLA '12, ACM , New York, NY, USA ( 2012 )

19. Toro , M. , Tanter , E.: A gradual interpretation of union types . In: International Static Analysis Symposium . pp. 382 { 404 . Springer ( 2017 )