TAPL 読書会@東京 第11回 - tokyotaplreading @ ウィキ

みずしまさんを交えてsubtypingのあたり

15 Subtyping

15.1 Subsumption

15.2 The Subytpe Relation
s-refl
s-trans
s-rcdwidth
s-rcddepth

15.2.1

S-rcdwith, s-rcddepth, s-rcdperm

each embody a different sort of flexibility in the use of records.

contravariant
covariant

Top
Finally, it is convenient to have a type that is a subtype of every type.

Formally, the subtype relation is the least relation cloased under the rules
we have given. For easy reference, Figure 15-1, 15-2 and 15-3 recaptotulate the full difinition
of the simply typed lambda calculus with recoreds adn subtyping

15.2.3
EXERCISE
(1) {a:Top, b:Top} {b:Top, a, Top}
(2)
(3)

15.2.4
EXERCISE

引数がbottomの関数→評価するとエラー(のはず)
call by name
call by need

15.3 Propeties of Subtyping and Typing
Having decided on the definition of the lambda-calculus with subtyping,
we now have some work to do to verify that it makes sense

• • in particular, that the presevation and progress teorems of the simply typed

lambda-calculus continue to hold in the presence of subtyping.

15.3.1
ex
15.3.2
ex

15.3.3
lemma

15.3.4
15.3.5

15.3.6
はどこが難しいのか

15.3.7 theorem [progress]

case T-APP

case T-RCD

case T-PROJ

case T-SUB

15.4 The Top and Bottom Types
The maximal type Top is not a neccessary part of the simply typed lambda-calculus with subtyping;

type infarence のときこある
Bot
Haskell で Bottomに相当する型?

15.5 Subtyping and Other Features
Ascription and Casting
Variants
Lists
References
Arrays
References Again
Channels
Base Types

15.6 Coercion Semantics for Subtyping
Problems with the Subset Semantics
Coercion Semantics

C :: S <:T to mean "C is a subtyping derivation tree whose conclusion is S &lt:T."

Coherence
Bool<:Int = λb:Bool. if b then 1 else 0
Int<:String = intToString
Bool<:Float = λb:Bool. if b then 1.0 else 0.0
Float<:String = floatToString

floatToString(0.0) = "0" and floatToString(1.0) = "1"

coercion でなくて subtyping が必要な理由

15.6.4
DEFINITION:
A tanslatoion － from typing derivations in one language to terms in another
is coherent if, for every pair of derivations D1 and D2 wit the same conclusion
Γ |- t : T, the translations D1 and D2 are behaviorally equivalent terms of
the targe language.

15.7
Intersection and Union Types

15.8
Notes
The idea of subtyping in programming languages goes back to the 1960s,

16.1 Algorithmic Subtyping

16.2 Algprithmic Typing

16.2.2
definition:
The algorithmic typing relation is

p211

S<S s-refl 自分自身

S-TRANS

S<Top s-top top/bottom

S-ARROW

s-rcd

Fig 14

16.1.2
LEMMA:
1. S<:S can be derived for every type S withou usig S-REFL.
2. If S<:T is derivable, the it can be derived without using S-TRANS.
Proof: Exercise