=Paper=
{{Paper
|id=Vol-2585/paper3
|storemode=property
|title=Gradual typing using union typing with records
|pdfUrl=https://ceur-ws.org/Vol-2585/paper3.pdf
|volume=Vol-2585
|authors=Karla Ramı́rez Pulido,Jorge Luis Ortega Arjona,Lourdes del Carmen González Huesca
|dblpUrl=https://dblp.org/rec/conf/lanmr/PulidoOG19
}}
==Gradual typing using union typing with records==
https://ceur-ws.org/Vol-2585/paper3.pdf
Gradual typing using union typing with records
Karla Ramı́rez Pulido1 , Jorge Luis Ortega Arjona1 , and Lourdes del Carmen
González Huesca1
Departamento de Matemáticas, Facultad de Ciencias,
Universidad Nacional Autónoma de México
{karla, jloa, luglzhuesca}@ciencias.unam.mx
Abstract. Dynamic typed languages are characterized by their expres-
siveness and flexibility to develop prototypes, while static typed lan-
guages 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 advan-
tages 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
1 Introduction
Commonly, programming languages can be broadly categorized according to
their typing as static or dynamic. Nevertheless, there are other typing classi-
fications 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 ex-
plicit 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. More-
over, not having explicit types allows programmers to have a better expressive-
ness, 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 se-
curity [5], type states [8], Object-Orientation [14,18], and so on. Although the
interest for Gradual Typed languages has been increased over the last few years,
Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0)
24
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 explic-
itly write static types, as well as leave some parts of the code without typing. A
type that has not been defined as “static” by the programmer should be verified
at run-time, and gradual type systems should be developed in order to preserve
type consistency.
The relation of consistency has a significant 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 pre-
sented 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 com-
bined 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 different 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 struc-
ture allows the programmer to manipulate expressions that could have different
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 Typ-
ing (GUT) approach, in which it is possible to have the two different types of
25
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 different
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 different 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 finite 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 defined 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 method-
ology [19]. The first 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 infinite power set ℘(T Y P E), to
the syntactic category GTYPE using functions α? and γ? . From these sets, it is
26
necessary to lift the set of types into a finite one, this implies the use of the power
set operator ℘. Then, functions α ı? and γÙ? are defined between ℘f in (℘(T Y P E))
and ℘f in (GT Y P E) [19].
Fig. 1: On the left the finite lifting over ℘(T Y P E) and GT Y P E. On the right the finite
lifting over ℘f in (GT Y P E) and U T Y P E.
The right side of Figure 1 shows the last transformation in order to obtain sys-
tem GT F L⊕ , through functions α⊕ and γ⊕ , in particular between ℘(GT Y P E)
and U T Y P E (i.e. between GT F L and GT F L⊕ ) [19].
3 Gradual Union Types with Records
This paper extends the GUT by Toro and Tanter with records. A record is a data-
type that describes variables (called fields) and their values. Fields possibly have
different types. Some programming languages use records to define 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 identifier of each one of its fields. 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 i∈1,...,n ], where `i denote
a label. A record term is expressed as [`i = ti i∈1,...,n ], where `i denotes a field
for term ti and a record value is defined as [`i = vi i∈1,...,n ] where each vi is a
value. Each record has a fixed 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 i∈1..n ] has type [`i : Ti i∈1..n ], in the same context Γ .
27
fin
T ∈ T Y P E, x ∈ V AR, t ∈ T ERM, Γ ∈ V AR * T Y P E, ` ∈ LABEL
T ::= Int | Bool | T → T | [`i : Ti i∈1..n ] (type)
v ::= n | b | λx : T.t | [`i = vi i∈1..n ] (values)
t ::= v | x | t t | t + t |if t then t else t | t :: T | [`i = ti i∈1..n ] | t.`j (terms)
x:T ∈Γ
(Tx ) (Tn ) (Tb )
Γ `x:T Γ ` n : Int Γ ` b : Bool
Γ ` t1 : T1 Γ ` t2 : T2 T2 = dom(T1 )
(Tapp )
Γ ` t1 t2 : cod(T1 )
Γ ` t1 : T1 T1 = Int Γ ` t2 : T2 T2 = Int
(T+ )
Γ ` t1 + t2 : Int
Γ ` t1 : T1 T1 = Bool Γ ` t2 : T2 Γ ` t3 : T3
(Tif )
Γ ` if t1 then t2 else t3 : equate(T2 , T3 )
Γ, x : T1 ` t : T2 Γ ` t : T T = T1
(Tλ ) (T:: )
Γ ` (λx : T1 .t) : T1 → T2 Γ ` (t :: T1 ) : T1
Γ ` ti : Ti i∈1..n f or each i
(Trec )
Γ ` [`i = ti i∈1..n ] : [`i : Ti i∈1..n ]
Γ ` t : [`i : Ti i∈1..n ]
(Tproj )
Γ ` t.`j : Tj f or some j ∈ 1..n
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 ) undef ined in other case cod(T ) undef ined in other case equate(T1 ,T2 ) undef ined in other case
Fig. 2: Syntax and type system of Simply Typed Functional Language, STFL [7] ex-
tended with records (shown in boldface).
Tproj : in order to assign a type to a projection j, if a term t has a record type t : [`i :
Ti i∈1..n ] in context Γ , then term tj of type Tj can be obtained through label `j .
System STFL has been proved safe [12], we only give some properties in order
to prove the gradual extensions.
Record substitution:
[`1 = t1 , `2 = t2 , ..., `n = tn ][v/x] = [`1 = t1 [v/x], `2 = t2 [v/x], ..., `n = tn [v/x]]
Projection of record substitution: (t.`j )[v/x] = (t[v/x].`j )
We show only the cases for records of the Lemma of Inversion which is based
on [12].
Lemma 1 (Inversion of typing relation).
1. If Γ ` [`i = ti i∈1..n ] : [`i : Ti i∈1..n ] then Γ ` ti : Ti f or each i ∈ 1..n.
2. If Γ ` t.`j : Tj f or some j ∈ 1..n then Γ ` t : [`i : Ti i∈1..n ].
28
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 bold-
face:
G ∈ GT Y P E G ::= Int | Bool | G → G | ? | [`i : Gi i∈1..n ]
The concretization function is defined as follows:
γ? (Int) = {Int} γ? (Bool) = {Bool} γ? (?) = T Y P E
γ? (G1 → G2 ) = {T1 → T2 | T1 ∈ γ? (G1 ) ∧ T2 ∈ γ? (G2 )}
γ? ([`i : Gii∈1..n ]) = {[`i : Ti i∈1..n ] | Ti ∈ γ? (Gi ) i∈1..n ]}
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 defined in STFL.
The abstraction function, following [19], is defined using TÛ which denotes a
set of types induced by T :
0 00 0 00
1 → T2 = {T → T | T ∈ T1 ∧ T ∈ T2 }
T¸ ı ı
i∈1..n ] = {[` : T i∈1..n
[`ˇ
i : Ti i i,j ] | Ti,j ∈ G
ıi ∧ i ∈ 1..n ∧ j ∈ 1..|G
ıi |}
α? ({T }) = T 1 → T2 ) = α? (T1 ) → α? (T2 )
α? (T¸ ı ı α? (∅) = undef ined
α? ([`iˇ ıi ) i∈1..n ]
: Ti i∈1..n ]) = [`i : α? (T α? (TÛ) = ? otherwise
Th abstraction function α? helps the language to obtain or retain more pre-
cision, while the unknown type is decreased, that is, the α? function can produce
a gradual type that abstracts a given set [7]. Toro and Tanter define optimal as
the best approximation of α? , that means the most precise gradual type that is
possible. Both functions γ? and α? define the Galois connection [19].
Definition 1 (GT Y P E Precision). G1 is less imprecise than G2 , G1 v G2 ,
if and only if γ? (G1 ) ⊆ γ? (G2 ).
The next proposition defines 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 ([`˛ : T i∈1..n ])
i i
i∈1..n ] = {[` : T i∈1..n
If TÛ = [`ˇ
i : Ti i i,j ] | Ti,j ∈ T
Ùi ∧ i ∈ 1..n ∧ j ∈ 1..|T
Ùi |} then
29
by definition of α? : α? ([`ˇ i : Ti
i∈1..n ]) = [` : α (T
i
Ù i∈1..n ]
? i)
and by definition of γ? for records we have γ? (α? (TÛ)) = γ? ([`i : α? (T Ùi ) i∈1..n ]) =
i∈1..n i∈1..n i∈1..n
γ? ([`i : Gi ]) = {[`i : Ti ] | Ti ∈ γ? (Gi ) } = {[`i : Ti i∈1..n ] | Ti ∈
i∈1..n
γ? (α? (TÙi )) }. By induction hypothesis Ti,j ∈ T Ùi ⊆ γ? (α? (T Ùi )) for each Ti,j
then the result holds.
i∈1..n
Case 2 for records ([`˛ i : Ti ])
Let T = [`i : Ti i∈1..n ], and suppose TÛ = [`ˇ i∈1..n ] ⊆ γ ([` : G i∈1..n ])
i : Ti
Û ˇ ? i i
and by definition of γ? : {[`i : Ti i∈1..n ] | Ti ∈ γ? (Gi ) i∈1..n }
By definition of α? for records: α? ([`ˇ i : Ti
i∈1..n ]) = [` : α (T
i
Ù i∈1..n ]
? i)
By the induction hypothesis, for each Ti if Ti ⊆ γ? (Gi ) then α? (T
Ù Ù Ùi ) v Gi .
Therefore, by definition 1 γ? (α? ([`ˇ i : Ti ? i
Ù i∈1..n ]) ⊆
i∈1..n ])) = γ ([` : α (T
? i)
i∈1..n
γ? ([`i : Gi ]) and the result holds.
The next step to give a Gradual Union Typing is to lift functions α? and γ?
to sets, that is from ℘f in (℘(T Y P E)) to ℘f in (GT Y P E) and vice-versa. Observe
that this lifting is over finite sets of types. We follow again Toro and Tanter [19].
Definition 2 (℘f in (GT Y P E) Concretization).
γÙ? : ℘f in (GT Y P E) → ℘f in (℘(T Y P E)) is defined as: γÙ? (G)
Ù = {γ? (G) | G ∈ G}
Ù
Definition 3 (℘f in (GT Y P E) Abstraction).
α
ı? : ℘f in (℘(T Y P E)) * ℘f in (GT Y P E) is defined as:
[
α
ı? (∅) = undef ined α
ı? (T
Ù) = α? (TÛ)
Ù
Û∈TÛ
T Û
Proposition 2 (ı
α? is sound and optimal). If T
Ù is non empty, then:
Ù
Ù ⊆ γÙ? (ı
1. T
Ù
α? (T
Ù))
Ù Ù ⊆ γÙ? (G)
2. T
Ù Ù =⇒ α Ù) v G
ı? (T
Ù Ù
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 ∈ ST Y P E S ::= Int | Bool | S → S | S ⊕ S | [`i : Si i∈1..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 finite set of types [19], where the concretization and abstraction
30
functions are defined between static types and finite 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 ∈ UTY PE U ::= Int | Bool | U → U | U ⊕ U | ? | [`i : Ui i∈1..n ]
We define a Galois connection between U T Y P E and ℘f in (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:
Definition 4 (U T Y P E concretization). γ⊕ : U T Y P E → ℘f in (GT Y P E)
γ⊕ (Int) = {Int} γ⊕ (Bool) = {Bool} γ⊕ (?) = {?}
γ⊕ (U1 → U2 ) = {G1 → G2 | G1 ∈ γ⊕ (U1 ) ∧ G2 ∈ γ⊕ (U2 )}
γ⊕ (U1 ⊕ U2 ) = γ⊕ (U1 ) ∪ γ⊕ (U2 )
γ⊕ ([`i : Ui i∈1..n ]) = {[`i : Gi i∈1..n ] | Gi ∈ γ⊕ (Ui ) i∈1..n }
The definition of abstraction function α⊕ (U T Y P E abstraction) is the same
defined by Toro and Tanter [19] and produces finite sets, that is the gradual
union of all elements in G:
Ù
Definition 5 (U T Y P E abstraction). α⊕ : ℘f in (GT Y P E) * U T Y P E
Ù = LG
α⊕ (G) Ù if G 6= ∅
= α⊕ (G1 ) ⊕ α⊕ (G2 ) ⊕ . . . ⊕ α⊕ (Gm ) where Gi ∈ 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:
Ù ⊆ γ⊕ (α⊕ (G))
1. G Ù Ù ⊆ γ⊕ (U ) =⇒ α⊕ (G)
2. G Ù vU
Proof. The proof is carried out by induction on the structure of U .
Case 1 for records.
Suppose G = [`i : Gi i∈1..n ] then G
Ù = {[`i : Ti,j i∈1..n ] | Ti,j ∈ G
ıi ∧ i ∈ 1..n ∧ j ∈
1..|Gi |}. Without loss of generality, take j = 1 for each Gi with i ∈ 1..(n − 1)
ı ı
and |Gˆn | = m.
To prove that G Ù ⊆ γ⊕ (α⊕ (G))
Ù we proceed by applying the definition of α⊕ (G): Ù
0 0
α⊕ ({[`i : Ti , `n : T ] | T ∈ G
ˆn ∧ i ∈ 1..n − 1}) =
31
{[`i : Ti , `n : T 0 ] | T 0 ∈ G
L ˆn ∧ i ∈ 1..n − 1} =
[`i : α⊕ (Ti ), `n : α⊕ (Gn1 )] ⊕ . . . ⊕ [`i : α⊕ (Ti ), `n : α⊕ (Gnm )]
Using definition of γ⊕ :
γ⊕ ([`i : α⊕ (Ti ), `n : α⊕ (Gn1 )] ⊕ · · · ⊕ [`i : α⊕ (Ti ), `n : α⊕ (Gnm )]) =
γ⊕ ([`i : α⊕ (Ti ), `n : α⊕ (Gn1 )]) ∪ · · · ∪ γ⊕ ([`i : α⊕ (Ti ), `n : α⊕ (Gnm )]) =
{[`i : γ⊕ (α⊕ (Ti )), `n : γ⊕ (α⊕ (Gn1 ))]}∪· · ·∪{[`i : γ⊕ (α⊕ (Ti )), `n : γ⊕ (α⊕ (Gnm ))]} =
{[`i : γ⊕ (α⊕ (Ti )), `n : Gnj ] | Gnj ∈ γ⊕ (α⊕ (G ˆn )) ∧ j ∈ 1..m}.
By induction hypothesis, Ti ∈ Gi and also belongs to γ⊕ (α⊕ (G
ı ıi )) for each
i ∈ 1..n − 1 and Gnj ∈ G ˆn belongs also to γ⊕ (α⊕ (G ˆn )) and therefore
G ⊆ γ⊕ (α⊕ (G)).
Ù Ù
Case 2 for records.
Suppose that G Ù ⊆ γ⊕ (U ) where G Ù = [`ˇ i∈1..n ] and
i : Gi
i∈1..n i∈1..n
γ⊕ (U ) = γ⊕ ([`i : Ui ]) = {[`i : Gi ] | Gi ∈ γ⊕ (Ui ) i∈1..n }
To prove α⊕ (G) Ù v U we proceed by definition of α⊕ (G): Ù
i∈1..n
L
α⊕ ([`i : Gi i∈1..n ]) = {[`i : Ti,j
ˇ ] | Ti,j ∈ Gıi ∧ i ∈ 1..n ∧ j ∈ 1..|G ıi |}
Without loss of generality, take j = 1 for each Gi with i ∈ 1..(n − 1) and
ı
|G
ˆn | = m, then by definition of γ⊕
γ⊕ ({[`i : Ti , `n : T 0 ] | T 0 ∈ α⊕ (G
ˆn ) ∧ i ∈ 1..n − 1}) =
0 0
S
γ ({[`i : Ti , `n : T ] | T ∈ α⊕ (G ˆn ) ∧ i ∈ 1..n − 1}) =
S ⊕ 0 0
{[`i : Ti , `n : T ] | T ∈ γ⊕ (α⊕ (G ˆn )) ∧ i ∈ 1..n − 1}
The induction hypothesis states that G ıi ⊆ γ⊕ (Ui ) =⇒ α⊕ (G ıi ) v Ui for each i
which by definition of precision gives γ⊕ (α⊕ (Gi )) ⊆ γ⊕ (Ui ), in particular for Gn .
ı
{[`i : Ti , `n : T 0 ] | T 0 ∈ γ⊕ (Ui ) ∧ i ∈ 1..n − 1} which is indeed
S
Therefore
{[`i : Gi i∈1..n ] | Gi ∈ γ⊕ (Ui ) i∈1..n }.
Therefore, following Toro and Tanter [19], the stratified interpretation of
U T Y P E is defined in terms of sets of sets of static types with the composition
of two presented Galois conections:
Definition 6 (U T Y P E concretization).
γ : U T Y P E → ℘f in (℘(T Y P E)) γ = γÙ? ◦ γ⊕
Definition 7 (GT Y P E abstraction).
α : ℘f in (℘(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:
Ù
Ù ⊆ γ(α(T
1. T
Ù Ù))
Ù Ù ⊆ γ(U ) =⇒ α(T
2. T
Ù Ù) v U
Ù
Proof. This proposition holds by Propositions 1, 3, and composition of sound
and optimal abstractions.
32
fin
U ∈ U T Y P E, x ∈ V AR, t ∈ U T ERM,
e Γ ∈ V AR * U T Y P E, ` ∈ U LABEL
i∈1..n
U ::= U ⊕ U | Bool | Int | U → U | ? | [`i : Ui ] (types)
t) | [`i = vii∈1..n ]
v ::= n | true | f alse | (λx : U.e (values)
t ::= v | x | e
e tet|e t | if e
t+e t then e
t else e t :: U | [`i = tei j∈1..n ] | te.`j
t|e (terms)
x:U ∈Γ
(Ux ) (Un ) (Ub )
Γ `x:U Γ ` n : Int Γ ` b : Bool
Γ, x : U1 ` e t : U2 Γ `e
t : U U ∼ U1
(Uλ ) (U:: )
Γ ` (λx : U1 .e
t) : U1 → U2 Γ ` (e
t :: U1 ) : U1
Γ ` te1 : U1 Γ ` te2 : U2 U2 ∼ dom(U
fi 1 )
(Uapp )
Γ ` te1 te2 : c›
od(U1 )
Γ ` te1 : U1 U1 ∼ Int Γ ` te2 : U2 U2 ∼ Int
(U+ )
Γ ` t1 + te2 : Int
e
Γ ` te1 : U1 U1 ∼ Bool Γ ` te2 : U2 Γ ` te3 : U3
(Uif )
Γ ` if te1 then te2 else te3 : U2 u U3
Γ ` tei : Ui i∈1..n f or each i
(Urec )
Γ ` [`i = tei i∈1..n ] : [`i : Ui i∈1..n ]
Γ ` te : [`i : Ui i∈1..n ]
(Uproj )
Γ ` te.`j : Uj f or some j ∈ 1..n
dom:U T Y P E*U T Y P E
› cfod:U T Y P E*U T Y P E
d›
om(U )=α(d”
om(γ(U )) cf
od(U )=α(cc od(γ(U ))
Fig. 3: Gradual Typed Functional Language system, GTFL⊕ , extended with records.
Figure 3 shows the grammar of the full system GT F L⊕ , following [19]. We use
t to denote terms in this system.
e
The next consistency relation is defined for U T Y P E as U1 ∼ U2 if and only if
ı1 ∈ γ(U1 ), T1 ∈ T
there exists T ı2 ∈ γ(U2 ) and T2 ∈ T
ı1 , T ı2 , such that T1 = T2 :
Proposition 5 (Consistency Relation).
U ∼ U1 U ∼ U2
U ∼U ?∼U U ∼? U ∼ U1 ⊕ U2 U ∼ U1 ⊕ U2
U1 ∼ U U2 ∼ U U21 ∼ U11 U12 ∼ U22
U1 ⊕ U2 ∼ U U1 ⊕ U2 ∼ U U11 → U12 ∼ U21 → U22
U11 ∼ U21 ... U1n ∼ U2n
[`1 : U11 , ..., `n : U1n ] ∼ [`1 : U21 , ..., `n : U2n ]
In order to present the static semantics of Gradual Union Typing is provided
the next definition of Gradual Meet [19], which is extended for records.
33
Definition 8 (Gradual Meet). Let u : U T Y P E * U T Y P E be defined as:
1. U u U = U
2. ? u U = U u ? = U
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 undefined otherwise.
The following definition states the translation of the equate from STFL to a
function in GTFL⊕ , in order to preserve typing:
Definition 9 (Equate Lifting).
‡ 1 , U2 ) = U1 u U2 = α({T
equate(U ı1 ∩ T
ı2 | T
ı1 ∈ γ(U1 ), T
ı2 ∈ γ(U2 )}) =
·? (G1 , G2 ) | G1 ∈ γ⊕ (U1 ), G2 ∈ γ⊕ (U2 )})
α⊕ ({equate
And the next proposition is needed to prove the gradual meet for GT F L⊕
Proposition 6. u = α ◦ equate
˙ ◦γ
˙
Proof. Proof is made using structural induction and the definition 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 inter-
action between union types and Gradual Typing [16,1], typestates [8], refinement
types [11], information-flow security typing [5], set-theoretic types and subtyping
[2], refinement 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 predefined 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.
34
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 differs 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. Pro-
ceedings of the ACM on Programming Languages 1(ICFP), 41 (2017)
2. Castagna, G., Petrucciani, T., Nguyẽn, 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 gener-
ating gradual type systems. ACM SIGPLAN Notices 51(1), 443–455 (2016)
4. Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based pro-
gram analysis by abstract interpretation. In: FPCA. vol. 95, pp. 170–181 (1995)
5. Disney, T., Flanagan, C.: Gradual information flow typing. In: International work-
shop 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 Pro-
gramming Languages. pp. 429–442. POPL ’16, ACM, New York, NY, USA (2016)
8. Garcia, R., Tanter, É., Wolff, 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-efficient gradual typing. Higher-Order
and Symbolic Computation 23(2), 167 (2010)
10. Jafery, K.A., Dunfield, J.: Sums of uncertainty: Refinements go gradual. ACM
SIGPLAN Notices 52(1), 804–817 (2017)
11. Lehmann, N., Tanter, E.: Gradual refinement 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 & effi-
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 Object-
Oriented 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)
35
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 first-class classes. In: Proceedings of the ACM International
Conference on Object Oriented Programming Systems Languages and Applica-
tions. pp. 793–810. OOPSLA ’12, ACM, New York, NY, USA (2012)
19. Toro, M., Tanter, É.: A gradual interpretation of union types. In: International
Static Analysis Symposium. pp. 382–404. Springer (2017)
36