第6回TAPL読書会

TAPL

Prelude

cocoatomoさんのTAPL発表資料

https://github.com/cocoatomo/TAPL_Tokyo

10 An ML Implementation of Simple Types

実行器が掲載されてない

  • ifとtrue、falseが足されてるので、これまでのコードに加えて修正が必要
  • ott アスキーアートで証明木を書くと、Coqのコードを出力してくれるものがある

http://www.cl.cam.ac.uk/~pes20/ott/

11 Simple Extentions

11.1 Base Types

UnitとBotの違い
voidはUnitに近い
HaskellでBotというと、評価するとエラーとか、無限ループする気がする
BottomはScalaのNothing
TopはScalaのAny

nullはJavaでのBottom。ありとあらゆる型に代入できる。

値がBottomと、型がBottomは区別する。
Haskellは値のBottom。数学のBottomと同じ。
Bottom値にとって、型はどうでもよい（有効な結果が返せないので）。

Intを出力する関数の型: Int -> () -> ()
Haskellだと： Int -> IO()
OCaml

let f x y = print_int x;;

let f x () = print_int x;;という書き方もアリ

11.2.1 Exercise

(ネストしたletの多相型の型推論は、また別の話)

ex.1

(\x.(x x))
 (\x.(x x)
  :
  (\x.x)))

ex.2 twiceをひたすら続けて（高階関数クイズ）
http://d.hatena.ne.jp/camlspotter/20100710/1278752186
というのは、2のタワーになる。

11.3 Derived Forms

Evaluation rule
Typing rule
(\x:Unit. t2) t1のt1はUnitでなくても良い。t2の中にt1が現れなければOK

11.3.1

t１；t２と(\x:Unit.t2)
TypingとEvaluationは可換である

derived form 言語に手を加えず、表面の文法を拡張すること

11.3.2

のちのち"パターン"の型も出てくるよ

11.4 Ascription

わざわざasと書いて明記するのは、Evaluation ruleで書くとasってことかな

11.4.1 （２）

やりたいこと：t1の評価を遅らせる
delayとforceをかけてやる

11.5.1

let x = tの形式は、そのままでは(\x:T1.t2)t1に変換できない（型の情報が足りない)。
単純な書き換えでは対応できないので、letはderived formではない、ということになる。
どうすれば型情報を得られるか-> 型付き導出木から調達する

let多相は、本来のlambda抽象や適用では模倣できない。確かにLispでは面倒なコードになりそう

11.7 Tuples

評価順序はPairと同じく左から

intermission

SML+多相レコード
多相レコードはOCamlのオブジェクトのフィールドと同じ感じ

11.8 Records

構造体とか連想配列と同じ。Labelで値がとれる

11.8.1 Exercise

気になるとしたら、E-ProjRcdの

  • 添字jの範囲?vの型?同じラベル名が複数あってはいけないとか?
  • p129の11.8.1の直前に、「i番めのラベルというのが取得できる」ことになっているが、それをきちんと書けということらしい。lispでいうassoc。
l_j -> l_i
----------------------
{l_i=v_i~{i:1..n}}.l_j -> v_j

Figure 11-7のtype of recordsの":"は多重定義になってる

Rubyでは、名前付きの正規表現でも添字を指定してアクセスできる

Record fieldの順序

静的なチェックとして順序を無視する、とは。

11.8.2 Exercise

Record pattern matching
Common Lispだと、多値を返す関数があります（floorとか)

let {a=x, b=y}={a:1, b:2} in add x y
let {a={c=x, d=y}, b=z}={a={c=1, d=2}, b=3} in add x y z

11.9 Sums

Javaでインターフェースを使って実現する?

  • ScalaのTraitが分からない
    • Haskellにはtype classあります
    • OCamlにはModule signatureあります
    • JavaでGenerics Eitherクラスを作るとか

Sums and Uniqueness of Types

11.10 Variants

cのunionにはラベルがないので、variantとしては不十分

Single-Field Variants

OCamlでは幽霊型を使う

次回

p140 Variants vs. Datatypes

宿題

Cのunionの定義を調べる(型変換に使えるか)