なのログ

だから見てて下さい・・・俺の・・・変身

型システム入門を読んでいます(第2回)

お久しぶりです(?)。読んでいます。
他の本が挟み込まれたり例のC#の事があったりと色々読めていなかったんですが、
これもおろそかにはできんなということで、記事を起こしに来ました。

第3章 型無し算術式
 5節 評価

です。


型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (11件) を見る
(特にアフィとかは無いです)(小声)

3章「型無し算術式」

まずおさらいです。前回したこと。

  • 構文の定義
    f:id:nanoyatsu:20181002192100p:plain trueとfalseがあって、ifにかけて他の項に行ったりする。
    zeroがあって、前後の値を表現したりiszeroで真偽値になったりする。
    iszero trueとかはまだ考えて無くて、項としては存在を認めている。

  • 項の定義(列挙) f:id:nanoyatsu:20181002192159p:plain 横並びがどんどん増えるたび表現の幅が広がる。
    (この集合Siの各要素が、この構文の取りうる項の形)

という事に対して、
ぶっちゃけ全然わかんないんですが数学的な証明とかをしていました。

そこでなんですが、前回の更新から今日に至るまでの間に d.hatena.ne.jp

こんな記事を読みまして、
「これはもしかして"わかり"が進んだのでは~??」
という要素があったのでちょろっと感想をば。

この型システム入門を読むに当たって前提のレベルで、
「型というのには数学の圏論というやつが密接に関わっているらしい」
という認識がなんとなくありました。
なので、この「しりとりの圏」も関連があるものと考えて読みます。

「しりとりの圏」も読んだ上で、圏論という学問(?)がやりたい事は
「計算対象のグループ分け」と
「分けたグループへの計算の定義」みたいな??ことか??
という気持ちになります。

で、「オッ? それってまさしく型の話やん??」となりまして、

圏論一般 しりとりの例
対象 ひらがな文字
ひらがな文字列
恒等射 長さ1の文字列
結合(合成) しりとり結合
対象の集合 ひらがな文字の集合H
射の集合 ひらがな文字列の集合HStr
dom (域) first
cod (余域) last
id (恒等射) unit

この表を見ながら
「しりとりの例」→「圏論一般」→「型無し算術式」と当てはめた場合、
対象→true, false, 0(, if, succ, pred, iszeroも入る?)
射→任意の項t
恒等射→true, false, 0

こういうことか~~???となり、
超ややこしく集合の項tの定義と形の証明をしまくってたのは射を洗い出す為で、
射を列挙することが「型無し算術式の圏」に対する理論を
展開する準備になっとるんやな~~~~?????

という納得をするなどしました。
ぼく的にはわりと納得です。

というか、
「どういう動機でわざわざこのSiとかいうヤツの定義してんねん」
とか思っていたんですが、

  1. 圏論というのがある
  2. 圏論おいてはまずグループ(=圏?)に含まれるモノ(=対象,射?)を定義しないと始まらない
  3. そっからなんか考えましょうね

みたいな雰囲気を感じることができ、
そしたらまあ確かに当然Siの取りうるパターンを網羅するよね、という気持ちになりました。

まあそんな感じです。
要するに、その定義の為に色々と数学の話が出ましたが、
「true, false, 0, succ t, pred t, iszero t, if t then t else t を使って無限に積み木するで」
という理解でなんら問題なさそうです。(幼稚園児並の比喩が爆誕
少なくともぼくは今のところそんな気持ちで進んでいます。ヨッシャ。

(なんか間違ってそうだったらマジでどなたかツッコミをしてやってください・・・)

5節 評価

で。やっと続きです。

ここに関しても色々とあるんですが、定義のところだけ抜いてきましょう。

  • bool値
    f:id:nanoyatsu:20181002200317p:plain

  • 数値
    f:id:nanoyatsu:20181002200354p:plain

  • 評価の失敗(行き詰まり状態)を拡張
    (これは半分非公式で、演習の中で定義)
    f:id:nanoyatsu:20181002200603p:plain

なんというか、見ての通りでした。
t -> t'の記法は、「tを評価するとt'になる」といった感じに読めます。
まあt == t'と思って大丈夫だと思います。
それと、分数みたいに上下で書かれているのは、
「上の式が成り立つ時、下の式はこう評価できるよ」というかんじ。

このそれぞれのtに今まで見たあらゆる項が入ってくるわけですが、
ifsuccprediszeroもまあ定義の通りッスねという。
(多少プログラムを見慣れていたらそう見えると思います)
唯一predに「負の値にはならないのね」というところがあるくらい。
(数値のところで値の項をnvとしてワンクッションしているのはそのため)
ぶっちゃけちょっとpredまわり噛み砕けてないですけどそれはそれで。

あ、あとそれから、wrongは例外投げるよみたいな。かんじで。した。


とまあここまで書いて、
「よーしパパプログラム的に解釈したのを実際にプログラムで書いちゃうぞ~」
とか思いかけたんですが、
「いやそれでさえ僕には過ぎた作業だ」と思い返したり、
そもそも次の4章からコレの実装に入るぞというお話だったのでやめました。

とはいえ、チラ見したら4章はたったの4ページでした。
F#くんの前身であるOcaml先輩で実装されているので、
ぜひともF#で書き下したいところだな・・・と思うだけ思っています。

イケるかなあ。また次回。がんばります。

ではでは。