型駆動開発の裏側 -IdrisのIDEモードを試してみる-

以前紹介したように、AtomにIdris用パッケージをインストールするとキーボードショートカットで様々な機能を利用できます。

takezoe.hatenablog.com

これがどのように実装されているのかが気になったので調べてみようと思い、Atomパッケージのソースコードを眺めてみました。

github.com

どうやらIdrisにはIDEモードというモードがあり、標準入出力を使用してS式でやり取りを行うIDE向けのプロトコルが存在するようです。ちょっと試してみました。

まずはIDEモードでプロセスを起動。

$ idris --ide-mode
000018(:protocol-version 1 0)

入出力は「メッセージの文字数を6桁の16進数にエンコードしたもの+S式のメッセージ」という形式で行われるようです。

こんな感じの作りかけのファイルを用意しておきます。

module Main

main : IO ()

このファイルを読み込みます。メッセージにはユニークなカウンタを含める必要があるようです。

000022((:load-file "/tmp/hello.idr") 1)

出力はこんな感じ。

0000a9(:output (:ok (:highlight-source ((((:filename "/tmp/hello.idr") (:start 1 8) (:end 1 12)) ((:namespace "Main") (:decor :module) (:source-file "/tmp/hello.idr")))))) 1)
00001e(:set-prompt "*/tmp/hello" 1)
000015(:return (:ok ()) 1)

CTRL+ALT+A相当の:add-clauseというメッセージを送信してみます。

00001B((:add-clause 3 "main") 2)

こんな感じで生成されたコードが返ってきます。

000025(:return (:ok "main = ?main_rhs") 2)

シンプルな手法ではありますが、Idris側でこのような機能を持っているので様々なエディタで同じ機能を簡単に実装できるようです。実際Atom以外にもvimEmacsSublime Text用のプラグインなども用意されています。ショートカットは異なりますが、使い慣れたエディタを使用して型駆動開発を行うことができますね。