近況

日記 プログラミング JavaScript OCaml

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

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 こわれた 一緒に楽しく遊んでいたのに.

ご飯

まだ?