TaPL読む３

TaPL

5章読んだ。 正直もうきつい。

  • 評価戦略苦手…なんとなく正規順序が括弧の外からで適用順序が中から、としか認識してない…値がラムダ抽象値なのが混乱の元っぽい。
    • 完全ベータ簡約は任意の順序でベータ簡約。簡約基は簡約（できる）基なのね。ベータ簡約って代入ってことでいいか。章の終わりに記号被りを自動的にうまくやりくりするために代入についていろいろ書いてたけど…
    • 操作的意味論で見たら値呼びは外から項を評価して巨大なラムダ抽象を作っていくように見える。関数適用が内側から行われるのかな。
    • 遅延評価はとにかく前から評価して適用してるように見えるけど…？

vvv 追記11/23 vvvvvvvvvvvv

  • 評価戦略について
    • 正規順序・名前呼びはともに引数を先に評価せず左外側から評価する非正格戦略。特に正規順序は完全に展開するのに対し名前呼びはラムダ抽象の内部を見ずに停止する。必要呼びは名前呼びの変種で、同じ引数を同一とみなし一度評価された場合全て値に置き換える（構文木が閉路を持つ→構文グラフ）
    • どんな評価戦略でも式は左からしか読めないが、被適用項が値でない場合そちらを評価するようにすることで内側から展開している。
  • 代入の場合分け、アルファ変換を許したうえでってことを意識しないと全域的にならなくて混乱してしまう。

^^^ 追記ここまで ^^^^^^^^^^^^

  • Church数の確認をいちいち:tで確認するのが面倒なので関数をつくった。後で本でも出てきたけど…
realbool b = b True False
realnat c = c (1+) 0
--list l = l (:) []
blist l = l (\h -> \t -> (realbool h):t) []
clist l = l (\h -> \t -> (realnat h):t) []

  • チャーチ数のflsとc0、空リストnilが同じだったり、sccとconsが似てたりするのは面白かった。特にprdで一度自分を再構築して1つ前を取り出すところがすごいよかった。表示させるときに思ったけどチャーチ数は組み立て方を表してるんだって感じ。

  • equalで盛大に躓いた。どうしてもcannot construct the infinite typeで怒られる。よくよく試してみるとc2以上の引き算の時点でだいぶ怪しい…よくわかってないけどどうもunsafeCoerceを使うといいらしい（参考：https://kazu-yamamoto.hatenablog.jp/entry/20091118/1258535348）のでちまちまと加えていったら引き算は多分できるようになった。一部はこんな感じ

-- c2 = \s -> \z -> s (s z)
c2 = \s -> \z -> s (unsafeCoerce (s z))
scc = \n -> \s -> \z -> s (unsafeCoerce (n s z)) 
plus = \m -> \n -> \s -> \z -> m s (unsafeCoerce (n s z))

\x -> x xみたいに入れ子っぽいところにとにかく入れまくったのでどれが効いたのか正直わかってない。しかも結局equalはどうにもならなかった…

lcr = \l -> \r -> iszero (minus l r)    -- l < r
rcl = \l -> \r -> iszero (minus r l)    -- r < l
--equal m n = and $ (lcr m n) (rcl m n)  -- どうしても無限型？で怒られる…

（2回に分けたらどうか？と思って轟沈した図）

  • 再帰のomega = (\x -> x x) (\x -> x x)でもcannot construct the infinite type in first x :: t0 ~ t0 -> tが出る。この~は検索で先に出るチルダ演算子ではなくて、型が等しいことを表してるっぽい。軽率にunsafeCoerceをした結果無限ループになった。

  • fixや階乗関数のtest部分で本では値を関数に包んで評価が発散しないようにしていたけど、Haskellは必要呼びなので、fixでは項の評価だけで簡約が走らず待てるし、testで分岐するときは選ばれなかったほうは評価されないので通常のifと同様にあまり気にしないでできた。

  • このあたり、とにかく無限型でエラーがでたのでunsafeCoerceの山になっている。

  • factorialの評価を自分でやってみると

fix g = fct = g fct = g (g fct)...

という感じになっていたので、gの不動点fix gを作るのが不動点コンビネータなのかな。コンビネータって工場っぽいと思ったけどそれはコンビナートだった。コンビナートってロシア語なんか…