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

第六回 5/7
第10章 すきっぷ

第11章
Simple Externsions

第10章の話
実行器がないので実際に動かすのは苦労が
OTT というツール

普段見慣れている言語に近づける
Base Type

11.2 The Unit Type
Unit型

Even in purely functional language, the type Unit is not completely without interrest,
but its main aplication is in lanugages with side effects, such as assingmnents to
reference cells -- a topic we will return to Chapter 13.

Unit 型の唯一の値が value
void みたいなもの

Bot型→§15.4
評価するとエラーになるもの Bottom ?

オブジェクト指向プログラミングだと何にでも代入できるような型が欲しくなる
ありとあらゆる型を受けられる型
値が Bottom と型が Bottom

Intを出力する関数

Int → () → ()
Int → IO() Haskellの場合

let fx y

最後に渡すものがないからUnitであって、何かを出力するからUnitではない。

11.2.1 Execise
t n と t n+1 は定数分のサイズしか違わないのに、t n+1 の簡約は tn の2倍かかるようなt n

twice camlspotterさんの高階関数クイズ

(λx.(x x))

(λx.x x
 (λx.x x
     …
      (λx.x x))))

→ tower

11.3

文法として組み込む方法
1) E-Seq, E-SeqNext, T-Seqを文法に追加する
2) t1;t2 を(λx: Unit. t2)t1 の略記とみる (derived form)

→P72

11.3.1 derived form であること
Theorem
t1;t2 と (λx:Unit.t2)t1は書き換えがいつでも可能
可換図式

宣言に手を加えずに

wildcard

11.4 Ascription
UU = Unit→Unit
型と型の略記
言語によってあったり(OCaml)なかったり(Java)

Exercise 11.4.1
(1) Show how to

t as T ≡ (λx:T x)t

(2) Suppose that, instead of the pair of evaluation rules E-Ascribe and E-Ascribe1, we
had given an "eager" rule

   t1 as T → t1

that throws away an ascription as soon as it is reached. Can ascription still be
considered as a derived form?

11.5 Let Bindings
複雑な式で、部分式の繰り返しを避けて読みやすくする
この本ではML流を採用

let x = t1 in t2 ≡ (λx: T1・t2)t1
T1をどこからか調達しないといけない

• Sequence、Wildcard、Ascription = term の変形

11.5.1 Exercise

11.5.2 Exercise
Is this a good idea?

11.6 Pairs

11.7 Tuples
Pair との違い?
It is easy to generalize the binary products of the previous section to n-ary
products, often called tuples.

SML
多相レコード OCamlのObject

11.8 Record

The generalization from n-ary tuples to labeled record is equally straightforward.

11.8.1 Exercise
Write E-PROJR CD more explicitly, for comparison.

Figure 11-8
{1:Bool, 2:Nat, 3:Bool}
{a:Bool, 2:Nat, c:Bool}

Record field の順序
多くの言語では、Record の個々の要素の順番は無視して同値性を考える
{a:1, b:2} と {b:2, a:1} を同一視するか?

拡張されたLet Binding
destructuring-binding (Common Lisp)
multiple-value-binding (Emacs Lisp)
multiple assignment (Python)
「同じ変数は二度現れない」という仮定の下、M-Rcdでは代入演算を合成している

Python

a, (b, c) = (1, (2, 3))

→

11.8.2 Exercise
1) Pattern に型をつけろ
2)ここまでの文法のtype preservation と progress の証明の概形を書け

P={a=x, b=y}:{a:Num. b:Bool}
=> x:Num, y:Bool

match({x, y}, {5, true}) yields [x|→ 5, y|→ true]
match(x, {5, true}) yields [x |→ {5, true}]
match({x}, {5, true}) yields [x |→ {5, true}]

E-LETV

11.9 Sums
型の和
heterogeneous collections of values

Either(Haskell), 共通インターフェース(Java)
trait

Type Sum を導入すると型の一意性が崩れてしまう

11.10 Variants
Type Sumを任意個の型の和に拡張
使い勝手などはSumと同じ
Enumerations
Single-Field Variant 型の目印としての名前

C の union
int で代入して float で読む →OK?

次回
p140
Variants vs. Datatypes