topical media & game development
subsections:
Types as sets
The subtype refinement relation
Objects as records
Types as sets of values
V \approx Int \cup ... \cup V \times V \cup V -> V
Ideals
-- over $V$
subtypes --
ordered by set inclusion
lattice --
Top = V
,
Bottom = \emptyset
Type system
subtypes correspond to subsets
a collection of
ideals
of
V
slide
:
The interpretation of types as sets
Sub-range inclusion
<=
\ffrac{
n <= n'
and
m' <= m
}{
n'..m' <= n..m
}
Functions
contravariance
\ffrac{
%s <= %s'
and
%t' <= %t
}{
%s' -> %t' <= %s -> %t
}
Records
\ffrac{
%s_i <= %t_i
for
i = 1..m
(
m <= n
) }{
{a_1: %s_1, ... , a_n: %s_n} <= {a_1: %t_1 , ... , a_m: %t_m}
}
Variants
\ffrac{
%s_i <= %t_i
for
i = 1..m
(
m <= n
) }{
[a_1:%s_1 \/ ... \/ a_m:%s_m] <= [a_1:%t_1 \/ ... \/ a_n:%t_n]
}
slide
:
The subtype refinement relation
Examples
subtyping
8..12 -> 3..5 <= 9..11 -> 2..6
{ age : int, speed : int, fuel : int } <= { age : int, speed : int }
[ yellow \/ blue ] < [ yellow \/ blue \/ green ]
slide
:
Examples of subtyping
Function refinement
f' : Nat -> Nat \not<= f : Int -> Int
Functions
-- as a service
contravariance
domain
-- restrictions for the client
range
-- obligations for server
slide
:
The function subtype relation
Objects as records
record = finite association of values to labels
Field selection
-- basic operation
(a = 3, b = true ).a == 3
Typing rule
\ffrac{
e_1 : %t_1
and ... and
e_n : %t_n
}{
{ a_1 = e1,..., a_n = e_n } : { a_1 : %t_1, ..., a_n : %t_n }
}
slide
:
The object subtype relation
Subtyping
-- examples
type any = { } type entity = { age : int } type vehicle = { age : int, speed : int } type machine = { age : int, fuel : string } type car = { age : int, speed : int, fuel : string }
Subtyping rules
%t <= %t
\ffrac{
%s_1 <= %t_1, ..., %s_n <= %t_n
}{
{ a_1 : %s_1, ..., a_{n + m} : %s_{n + m} } <= { a_1 : %t_1 , ..., a_n : %t_n }
}
slide
:
Examples of object subtyping
Subtyping in Emerald
-- S conforms to T
S
provides at least the operations of
T
for each operation in
T
, the corresponding operation in
S
has the same number of arguments
the type of the result of operations of
S
conform to those of the operations of
T
the types of arguments of operations of
T
conform to those of the operations of
S
slide
:
The subtype relation in Emerald