近況

ご飯炊けるまでに最近やってることとか書きます.

System Fω の実装

js-sandbox/system-f-omega at master · susisu/js-sandbox · GitHub

前回やった System F の続き.

簡単に説明すると System F に加えて型レベルの関数 (type operator とか type constructor とか) が追加されて強くなる. 詳しくは TaPL を読んで下さい. System Fω の実装は演習問題です.

Calculus of Constructions の実装

js-sandbox/coc at master · susisu/js-sandbox · GitHub

これも続き.

Dependent product (値に依存した型) が追加され, と思いきやその dependent product は arrow (関数型), forall と統一され, 値と型の境界は曖昧になり, プログラムの動作に関する証明が可能になります (というのであってる?).

あまり資料が見当たらなかったので Wikipedia をはじめ, 原論文 とか Coq のリファレンス (これは CoC ではなく pCIC だけど, まあ根本的には大体同じなはず) とか Barendregt 1992 とかを眺めながら適当に実装しました. 眺めただけなのでどこか間違ってるかも.

ご飯

まだ炊けていません.

OCaml の練習

以前 JavaScript でパーサコンビネータを作っていたときに, 拡張モジュールみたいなものを作ると依存関係がごにょごにょで, 結局 ML でいうところの functor みたいな形 (モジュールを引数にとってモジュールを返す関数) で実装したのですが, これは現行の Flow では型が付けられなさそうでした (たぶん).

で, これ型つけるんだったら OCaml くらいの型システムが必要なんじゃないっすかねと適当なことを言っていたんですが, 実際 OCaml を (ほぼ) まともに触らずに言うのはアレだったので, ちゃんとやってみようという感じです.

Real World OCaml がオンラインで無料で読めるので (ありがたいことです), これをとりあえず第二部まで読みました.

今後読む場合の注意点としてひとつ, record やvariant などのデータと S 式との相互変換を行う関数を定義するための拡張構文 with sexp が紹介されているのですが, これは最新のバージョンでは削除されていて, 代わりに ppx_sexp_conv というのを使って [@@deriving sexp] などと書けば良いらしいです (参考: https://github.com/susisu/est-ocaml/blob/master/src/reader.ml#L46-L51).

ついでに, 読んでるだけだと飽きたし, どう書いたらいいかとかあまり覚えられなさそうだったので (実際書いてみたら覚えてなかった), 練習がてら昔 JSで書いたコマンドラインツール を書き直してみたりしていました.

github.com

こういう感じの, AWK や R で書くのが面倒なときにちょうどいい感じのやつです.

$ cat sample.dat
1   2   3
4   5   6
7   8   9
$ est '$0 + 2 * $1' sample.dat
5
14
23
$ est 'sum $0' sample.dat
12

ご飯

まだ炊けない.

読書

上でも挙げた Barendregt 1992 が面白げなのでちゃんと読んでみています. あと Real World OCaml の続き.

JavaScript

Flow こわれた 一緒に楽しく遊んでいたのに.

ご飯

まだ?

型無しラムダ計算での不動点オペレータの導出

公式は覚えるものではなく, 必要に応じて導出するものだよ (?)

不動点オペレータ

不動点オペレータ (大抵 fix という名前, コンビネータ計算の文脈では Y とも) は Haskell では以下のように定義される関数である.

fix f = f (fix f)

つまり, fix f は関数 f不動点となっている.

OCaml のような値呼びの言語では, 評価順序の影響で, 定義は以下のようになる.

let rec fix f = f (fun x -> fix f x)

fix が何に使えるのかは直感的にはわかりにくいが, これは再帰関数を定義するときに便利である. 例えば let recfix を用いた式の糖衣構文と見ることもできる.

以下では型無しラムダ計算での不動点オペレータの導出?を行う. 型無しラムダ計算の説明は省く (面倒なので). あと文法は例によって謎の ML 風のアレ.

再帰関数の定義

型無しラムダ計算には組み込みの fix のようなオペレータは存在しない. それではどのように再帰関数を定義するのかというと, 例えば階乗を計算する関数は素朴には以下のように書ける.

let factorial f n =
  if n = 0 then 1
  else n * f f (n - 1)

let ans = factorial factorial 10 

このままだと n の階乗を計算するためには factorial factorial n のように factorial にそれ自身を引数として明示的に与えてやる必要がある. これは面倒なので, 次のように定義し直す.

let factorial =
  let m f = fun n ->
    if n = 0 then 1
    else n * f f (n - 1)
  in
  m m

let ans = factorial 10

一般に再帰関数は次のように書ける.

let recursive =
  let m f = C[f f] in
  m m

ここで C[f f] となっているのは f f を含む項という程度の意味で, 上の階乗の例では C[t] = fun n -> if n = 0 then 1 else n * t (n - 1) だった.

この let m f = ... in m m という部分はどのような再帰関数に対しても同じなので, C を外部から与えるようにしてしまえば, 再帰関数を定義するための関数が作れる.

let recursive g =
  let m f = g (f f) in
  m m

あるいは let を使うのをやめると,

let recursive g = (fun f -> g (f f)) (fun f -> g (f f))

これは以下のように使用できる.

let factorial = recursive (fun f n ->
    if n = 0 then 1
    else n * f (n - 1)
  )

また, recursive g の呼び出しを適当に評価してやると,

recursive g
~> (fun f -> g (f f)) (fun f -> g (f f))
~> g ((fun f -> g (f f)) (fun f -> g (f f)))
== g (recursive g)

となっており, 実は最初に挙げた Haskell での fix と同じ動きをするということが分かる. というわけで, 以降 recursive ではなく fix と呼ぶことにする.

let fix g = (fun f -> g (f f)) (fun f -> g (f f))

いかにも数学的な概念そのもののような定義の fix だが, そのまま便利な道具として使えるのは少し面白い.

値呼びでの注意点

ところでこの関数の呼び出しは値呼びだと問題があり, 評価を追ってみると,

fix g
~> (fun f -> g (f f)) (fun f -> g (f f))
~> g ((fun f -> g (f f)) (fun f -> g (f f)))
~> g (g ((fun f -> g (f f)) (fun f -> g (f f))))
~> ...

のように引数部分を延々と評価し続けてしまい, g が呼び出されることはない. 一方で最初に定義した factorial の動作に問題はなかった. なぜこのようになってしまったかというと, C[f f]g (f f) で置き換えたとき, 元の定義では f f は直ちに評価されなかったのが, 置き換えた後では g の呼び出し前に評価するようになってしまっているためである.

この f f の評価されるタイミングを調整する (遅延させる) ため, f f の代わりに同じ動きをする関数 fun x -> f f x (η-expansion とかいう名前がついている) を g に与えるように変更する.

let fix' g =
  let m f = g (fun x -> f f x) in
  m m

あるいは let を使わずに書けば,

let fix' g = (fun f -> g (fun x -> f f x)) (fun f -> g (fun x -> f f x))

このようにすることで, f f が評価されるタイミングが元と同じになる. 実際, 呼び出しの評価がどのように行われるかを見てみると,

fix' g
~> (fun f -> g (fun x -> f f x)) (fun f -> g (fun x -> f f x))
~> g (fun x -> (fun f -> g (fun y -> f f y)) (fun f -> g (fun y -> f f y)) x)
== g (fun x -> fix' g x)

となり, 正しく g が呼び出されるようになる. また, この挙動は一番最初に挙げた OCaml での fix と一致する.

このように変更しても使い方は変わらない.

let factorial = fix' (fun f n ->
    if n = 0 then 1
    else n * f (n - 1)
  )