この記事は学生エンジニア Advent Calendar 2015 21日目の記事です．

この間このカレンダーを落とさないために今日の分のネタを投下してしまったので今日はおそらく一部の界隈にしか受け入れられないであろうお話をします (かなしい)．

Agenda

agda2-mode で TDD をした
上の経験により TDD 初学者の心を取り戻した
OCaml ver. を作った

界隈の方にはふわっとしすぎたお話ですし，そうでない方にとっては聞き慣れない単語の羅列になっていると思います．頑張って動画とか載せてイメージしやすくしていくのでどうか諦めないでください…

agda2-mode

Agda というプログラミング言語がありまして，Coq を知っている方は聞いたことあるかなと思うのですが，定理証明をするための言語です．Coq との違いはここでは触れませんが，Coq よりも プログラミングしているっぽい 感覚で定理証明をすることができます．Haskell を書いたことがある人は，あれに依存型が入ったような感じと思っていただければ．そう，依存型．Dependent Type．

依存型 - Wikipedia

一言でいうと (たぶん怒られそうなのですが) 「型に依存した定義を持つ型」というわけです．依存型の説明でおそらく一番有名なのは「安全な head 関数を作る」だと思います．@yoshihiro503 さんのこのブログなど分かりやすいです (これは Coq ですが)．

Coqで依存型 - にわとり小屋でのプログラミングブログ

分からなくても大丈夫です．今回は依存型の話はしません．できません．とりあえずおそらく皆さんが普段イメージする「型」の概念よりももう数段神様の世界に近づく概念だと思ってください．

で，この Agda の授業が大学院の授業であったんですね (講義録)．

このとき私は Agda を書いていたというよりも agda-mode (agda2-mode) というものに Agda を書かされていたわけです．

github.com

これは Emacs のモードの一つで，Agda を書いているときにプログラム中に expression として ? (hole) を書くことができ，その部分の型とそのときの型環境を表示してくれるものです．あと hole 内に書いた変数で case 式 (pattern match) とかを展開してくれます．とにかく agda2-mode が言った通りの型 (の値) を型環境にあるものを使ってうまく作って hole に入れてあげればいいわけです．

言っても分からないと思うので見てください．下のウィンドウに hole の型が表示されています．今回コマンドを押し忘れたのですが，hole のところで C-c C-, とすると hole の型だけでなくスコープ内にある変数の型一覧 (型環境) も表示してくれます．

youtu.be

超便利！！型合わせゲーム最高！！！TDD (Type Driven Development)！！！TDD (Type Driven Development)！！！

ちなみになんと最近流行りのモダンなエディタ Atom にもこの agda-mode があるので宗教上の理由により Emacs を使えない方はこちらをお試しください．

agda-mode

実際に使ってみた私のらぼの同期の記事はこちら

Atom で Agda - Qiita

プログラミング初学者の心

当時私は大学の後輩になんとか OCaml の可愛さを理解していただきたく，先輩が実装された型デバッガというものを初学者向けに改良する，ということをしていました．この型デバッガはコンパイラの型推論器を使ってプログラム中の型エラーの原因を特定していくデバッガなのですが，対話的である という点が画期的なところ (の1つ) です．型デバッガはユーザに，例えば「ハイライト部分にある変数 x の型を int だと意図しているか？」と (n >= 1 回以上) 尋ねます．ユーザはこの問いに対して yes, no で回答していくだけでどこで型 (推論) が conflict しているのかを見つけ出すことができます．要するに，コンパイラが推論した型とユーザが意図している型がどこで食い違っているかを探索していく，というものです．

こちらも百聞は一見に如かずです．以下では見かけは同じ2つのプログラムの型エラーの原因が，ユーザが意図している型によって異なる例です． (ちなみに以下では OCaml 3.12 になっていますが 4.01 まで対応しています)

youtu.be

おかげ様で型デバッガを採用した OCaml の授業を受けた学年は「C より Java より OCaml が好き」と言ってくれるまでに OCaml を愛してくれました．めでたしめでたし……

というわけにもいかなかったのです．

弊大学の OCaml の授業では TDD (言わずもがな T は Type の T) を最初から導入していて，関数を書く前にコメントアウトでその関数の型を書かせるようにしています．例えば「リストの中の整数全てに与えられた整数 p を足したリストを返す関数 plus_p」なら

(* plus_p: int list -> int -> int list *)

というのが全体像となります．これを考えさせてから実際に plus_p 本体の実装をするようにしています．これを考えるとき，自然とアルゴリズムや他の関数のことやモジュールの設計なんかについてなんとなーく考えるようになりますから．それからこれがしっかり書いてあると他の人が読みやすいのです．なんていったって型はドキュメントですので．

型はドキュメント
— ゆずこ＠這いよるお嬢様 (@yuzumikan15) 2015, 8月 17

…でもさっきのあれ，コメントアウトなんですよね．

だから適当なこと書く人も割といて，最初に全体像を把握出来ていない，ドキュメントを考えられていないからプログラムの中身をどう書いていいのか分からない，そんな """負 (不)""" があったわけです．

前置きが長くなりましたが，そんなわけでさっきの agda2-mode の OCaml ver. を作ろうと，そう，思ったのです．

ocaml-alab-mode

名付け親は私です．alab は弊研究室がこの界隈では「A研」で通っていて，弊大学の OCaml の授業で使う OCaml のサブセットについては網羅していこう，というところから alab-mode となりました．あと現段階では Emacs でしか使えません．agda-mode for Atom が悔しかったので時間できたら Atom 用のパッケージでも作ります．Vim 用は Vimmer のどなたかにお任せ致します (びむすくりぷと…)．

ソースコード

yuzumikan15/ocaml-alab-mode · GitHub

なんかいろいろ入っていますが dev branch の

OCamlMakefile
Makefile
main.ml
my_compile.ml
expander.ml
printtypes.ml
hole.el

があればいいと思います．あと README の Requirements にあるものたち．

全然リファクタリングしてなくてとっ散らかったプログラムなので本当に全方位平謝りです．まさかり投げないでくださいごめんなさい…

型注釈を付ける

今回 alab-mode を実装するために，ユーザが書いているプログラムを OCaml のコンパイラに渡して型付きの抽象構文木 (Typedtree) を作ってもらい，それを walk することで hole や環境の型を求めています．なので expression をいきなり hole にしてしまうと全てが多相になってしまいます．何を言っているか分からない人はとりあえずこれだけ覚えてください．

ソースコードには型の annotation を付けて！

(* plus_p: int list -> int -> int list *)
let plus_p lst p = List.map (fun x -> x + p) lst

というコードは

(* plus_p: int list -> int -> int list *)
let plus_p (lst: int list) (p: int): int list = List.map (fun x -> x + p) lst

か

(* plus_p: int list -> int -> int list *)
let plus_p: int list -> int -> int list = fun lst p -> List.map (fun x -> x + p) lst

という形で型注釈を付けることができます．でないと今デバッグ用のエラーメッセージ出てきてしまいますから！！お願いします！！！

機能

hole の挿入，削除
hole の展開 (expression 指定なし): tuple, record のみ
hole の展開 (expression 指定あり)
指定した変数での match 式の挿入: list, option, ユーザが定義した型 (record, variant) のみ
if 式の挿入

key bind は README にある通りです．

hole の挿入，削除

agda2-mode では ? が書けるようになっていましたが alab-mode では C-c h で入ります．いきなりハイライトされていますが内部的には (exit(*{}*n)) (n は自然数) となっています．なので alab-mode では exit n が使えないのですね…

gyazo.com

hole の展開 (expression 指定なし)

agda2-mode の hole に何も書かないときの refine と同じことをしています．

(* make_pair: 2つの整数をもらい2つ組を返す *)
(* make_pair: int -> int -> int * int *)
let make_pair: int -> int -> int * int = fun p q -> (p, q)

を書きたいときに最後の expression を C-c h で hole にしてあげて (以下のようになります)

(* make_pair: int -> int -> int * int *)
let make_pair: int -> int -> int * int = fun p q -> {}0

0番の hole のところにカーソルを合わせて C-c r とすると

(* make_pair: int -> int -> int * int *)
let make_pair: int -> int -> int * int = fun p q -> ({}0, {}1)

みたいに勝手に2つ組の形に展開してくれるような機能です．tuple と record に対応しています．

tuple の例．2つ整数をもらってきて2つ組を作ります．

gyazo.com

hole の展開 (expression 指定あり)

hole に expression を書いた状態で refine をします．このとき expression を入れた状態でコンパイラがエラーを出さなかったら refine でき，何かしらのエラーメッセージが出たら refine できないようになっています．

person 型が先に type で定義されていて，make_person ではこの person を作ります．以下では最初に0番目の hole に型の違う変数 age を入れると下のウィンドウにエラーメッセージが出てきて refine できません．

gyazo.com

match 式, if 式の挿入

hole に書いた変数で pattern match をすることができます．現段階では tuple, list, option, ユーザが定義した (同一ファイル内の) 型 (record, variant) に対応しています．また，hole のところで C-c i とすると if 式を挿入できます．

gyazo.com

実際に使ってみる

目標は弊大学の OCaml の授業でまともに使えるようにすることなので，この授業の課題を1つ解いてみましょう．

八百屋木（「文字列（野菜名）と整数（値段）のペア」の木）と野菜リスト（文字列（野菜名）のリスト）を受け取ったら、野菜リストの中にある全ての野菜を買えた場合のみ、その代金の合計を返し、野菜リストの中にひとつでも八百屋に置いていない野菜があった場合は 0 を返すような関数 total_price をデザインレシピに従って作れ。

一般的な木の型として以下が与えられているものとします．ちなみに二分探索木とします．

type ('a, 'b) tree_t = Empty
                     | Node of ('a, 'b) tree_t * 'a * 'b * ('a, 'b) tree_t

'a, 'b は型変数なので，この課題の八百屋木は (string, int) tree_t となります．

youtu.be

issue

github の issue の通りですが目下の課題は

next goal, previous goal の key bind による移動
任意の型 (を持つ変数) について pattern match (現在決め打ちで出力している list, option などの OCaml が定義している型は，本当はそこまで探索できるようにしたい)
ocaml-alab-mode を minor mode にする

です．あとなんか無駄に改行が入るのと，pattern match したときのコンストラクタの引数名どうにかしたいですね……

まともに使えるようになったら来年度の OCaml の授業はこれと，型デバッガと，あともう一つ秘密兵器を使えるようになります (論文とかの関係で言っていいのか分からないので伏せておきます…)．みんな頑張ってください．

ゆずとみかんといちご

ゆるゆる書きます

ocaml-alab-mode もどきを作っているお話

Agenda

agda2-mode

プログラミング初学者の心

ocaml-alab-mode

ソースコード

型注釈を付ける

機能

hole の挿入，削除

hole の展開 (expression 指定なし)

hole の展開 (expression 指定あり)

match 式, if 式の挿入

実際に使ってみる

issue