端端舝

.
TaPL 掂𤩸頗 #9 ∫14 Exception
.

A. Miyashita (@yaggy gcv)

2012.11.21

A. Miyashita (@yaggy gcv) TaPL 掂𤩸頗 #9 ∫14 Exception 2012.11.21 1 / 17

公丹分﹜瞰俋毛妏云丹

皿伕弘仿丞匹▲瞰俋◎腔卅袨暿互逃汜允月仇午手丐月
0 壺呾支左奈田奈白伕奈互逃汜仄凶
棗𤩸卞卅中平奈毛統桽仄方丹午仄凶
饜蹈及奶件犯永弁旦��巨仿奈
白央奶伙互�勾井日卅中﹜嶱仃卅中
交奈扒互皿伕本旦毛 kill 仄凶卅升祡韜腔卅巨仿奈互逃汜仄凶
仇木日毛黱隙伕斥永弁匹隙旌允月及反嬪褣﹝
瞰俋毛爀⻌允月午＃
皿伕弘仿丞毛笢砦允月
娗逋仄化隙覧毛�心月
瞰俋及逃汜仄凶ロ�毛眭月
仇氏卅仇午互堤懂月


覧� ‵ 倰☆↙★(1)

Syntax

t ::= terms:
t variable
竹x:T.t abstraction
t t application

v ::= values:
竹x:T.t abstraction value

T ::= types:
T↙T type of functions

忙 ::= contexts:
? empty context
忙, x:T term variable binding


覧� ‵ 倰☆↙★ (2)
Evaluation t ↙ t∩
t1 ↙ t∩
1
(E-App1)
t1 t2 ↙ t∩ t2
1
t2 ↙ t∩
2
(E-App2)
v1 t2 ↙ v1 t∩2
(竹x:T11 .t12 ) v2 ↙ [x ↙ v2 ]t12 (E-AppAbs)

Typing 忙 ? t:T
x:T ﹋忙
(T-Var)
忙 ? x:T
忙, x:T1 ? t2 : T2
(T-Abs)
忙 ? 竹x:T1 .t2 : T1 ↙ T2
忙 ? t1 : T11 ↙ T1 2 忙 ? t2 : T11
(T-App)
忙 ? t1 t2 : T12

瞰俋 ‵ error 及爀⻌
New syntactic forms
t ::= ... terms:

error run-time error

New evaluation rules t ↙ t∩
error t2 ↙ error (E-AppErr1)
v1 error ↙ error (E-AppErr2)

New typing rules 忙?t:T
忙 ? error : T (T-Error)


E-AppErr2 及啐�卞憝允月娗逋 (1)

瞰尹壬
(竹x : Nat.0)
反﹜
(竹x : Nat.0) error ↙ error(E-AppErr2)
午 (珨砩卞) 啐�今木月﹝

error 反 value 匹反卅中及匹﹜E-AppAbs

(竹x : T.t)v ?↙ [x ↙ v ] t

反羥蚚匹五內﹜

(竹x : Nat.0) error ↙ [x ↙ error](竹x : Nat.0) ↙ 0

午啐�今木月陑饜反卅中﹝


E-AppErr2 及啐�卞憝允月娗逋 (2)

肮�卞﹜
(fix(竹x : Nat.x)) error
反﹜酘�及�互 value 卞卅月引匹啐�匹五卅中及匹﹜剠癹卞砦引日卅中﹝


error 及倰 (T-Error) 卞憝允月娗逋

T-Error 及��t反﹜error 互￤砩及倰午卅月仇午毛砩庤允月互﹜仇木反﹜
☆凶井分井 1 勾及倰仄井厥凶卅中★午中丹隅燴 (9.3.3) 卞毀仄化仄引丹﹝
error 毛郔苤倰 Bot 午允月 (∫15, subtyping)
error 毛嗣眈倰 ?X.X 午允月 (∫23, parametric polymorphism)


Preservation/Progress �t

Preservation �t反瞰俋爀⻌摽手劐歹日卅中
丐月�互倰 T 毛厥切﹜1 僇蕆啐�今木凶�磁﹜啐�摽及倰手
T 匹丐月﹝
Progress 反嗣屾及劐載互斛猁
t 互寯元凶﹜謎仁倰葆仃今木凶淏�倛匹丐月午五﹜t 反 value
手仄仁反 t = error 匹丐月 (隅燴 14.1.2)


今化﹜礿砦反匹五月方丹卞卅勻凶互

砦引月分仃元扎傺互剠中

棒卞﹜瞰俋毛娗逋仄化﹜�I燴及隙覧毛俴丹方丹卞仄凶中﹝
↙ 云鎧�心﹜try...with... 恅 (Java/C++及 try...catch...) 毛爀⻌


瞰俋�I燴 ‵ try 及爀⻌
New syntactic forms
t ::= ... terms:

try t with t trap errors

try v1 with t2 ↙ v1 (E-TryV)
try error with t2 ↙ t2 (E-TryError)
t1 ↙ t∩
1
(E-Try)
try t1 with t2 ↙ try t∩ with t2
1

忙 ? t1 : T 忙 ? t2 : T
(T-Try)
忙 ? try t1 with t2 : T


瞰俋及��ロ�毛敵埣六午

☆瞰俋逃汜仄引仄凶★勻化晟歹木化手珨极升丹允木壬謎中及井�絞手葆
井卅中

↙ 瞰俋卞☆瞰俋互逃汜仄袨暿★毛�午仄化厥凶六月


�毛厥勾瞰俋 ‵ raise 及爀⻌ (1)
.
New syntactic forms

t ::= ... terms:

raise t raise exception

try t with t handle exceptions


(raise v11 ) t2 ↙ raise v11 (E-AppRaise1)
v1 (raise v21 ) ↙ raise v21 (E-AppRaise2)
t1 ↙ t∩ 1
(E-Raise)
raise t1 ↙ raise t∩ 1
raise (raise v11 ) ↙ raise v11 (E-RaiseRaise)
try v1 with t2 ↙ v1 (E-TryV)
try raise v11 with t2 ↙ t2 v11 (E-TryRaise)
t1 ↙ t∩
1
(E-Try)
try t1 with t2 ↙ try t∩ with t2
1


�毛厥勾瞰俋 ‵ raise 及爀⻌ (2)


忙 ? t1 : Texn
(T-Exn)
忙 ? raise t1 : T
忙 ? t1 : T 忙 ? t2 : Texn ↙ T
(T-Try)
忙 ? try t1 with t2 : T

↗ error 反 raise unit 及�恅昒畟午�卅仄化謎中?


Texn 及倰卞勾中化 (1)
. Nat 倰午允月 (瞰: Unix 及巨仿奈戊奈玉)
1

0: 傖髡﹜0 眕俋: 瞰俋逃汜及袨暿毛桶允
卅中方曰反穴扑分仃升﹜少勻切扎仃 500 巨仿奈勻化晟歹木化手嬪月
.
2 String 倰午允月 (巨仿奈丟永本奈斥)

袨暿毛參挍允月凶戶卞�恅賤昴互斛猁卞卅月仇午手
. 田伉失件玄倰 (Java/C++及 enum 卞眈絞) 卞允月
3

Texn = <divideByZero : Unit,
overflow : Unit,
fileNotFound : String,
fileNotReadable : String,
... >
仇及引引匹反﹜☆丐日井元戶★�化及摩磁毛隅膽 (?x) 仄化云井卅仃
木壬卅日卅中及匹﹜嶱逃氪互失皿伉弗奈扑亦件黃赻及瞰俋毛隅膽允
月豻華互卅中﹝


4 交奈扒奈隅膽及瞰俋毛庲戶月��田伉失件玄倰卞允月 (瞰: ML 及
exn 倰)
exception l of T 午隅膽 (凶分仄﹜l 反踏引匹卞隅膽今木化中月
Texn 卞漪引木化反中仃卅中)
允月午眕蔥反﹜Texn 互 < l1 : T1 , ..., ln : Tn , l:T > 午仄化婬隅膽 (let)
今木月
瞰俋毛 raise l(t) 匹網太堤允
def
raise l(t)) = raise (l=t) as Texn
try �恅
def
try t with l(x)↙ h = try t with
竹 e:Texn .case e of
<l=x>?h
| ? raise e



5 交奈扒隅膽瞰俋弁仿旦 (瞰: Java 及 Throwable)
仿白卞晟尹壬 ML 及��田伉失件玄倰午湮极肮元﹝�卅月萸反﹜
扔皮弁仿旦及�唗勿仃卞方曰﹜圉�唗憝�S互丐月 (瞰尹壬
IOException 匹 catch 允月午﹜IOException 云方太﹜公及�化及扔
皮弁仿旦 (ex. FileNotFoundException) 毛手�I燴匹五月)
隙覧及褫瘁匹瞰俋弁仿旦互Е�e今木月
Throwable
念 Error: 隙覧祥夔 (�I燴反￤砩分互�I燴允屯五匹卅中)
岫 JVM 卅升匹逃汜允月祡韜腔卅巨仿奈
弩 Exception: 隙覧褫夔 (�I燴反斛�)
岫伕斥永弁匹隙旌允月及互醱給卅瞰俋
弩 RuntimeException: 隙覧褫夔 (�I燴反￤砩)
皿伕弘仿丞及田弘卞お秪允月瞰俋


端端舝

TaPL掂𤩸頗 #9 ‵ ∫14 Exception

More Related Content

TaPL掂𤩸頗 #9 ‵ ∫14 Exception