３日ほど前に、↓の記事を読んで「最近 Idris 熱いのかー」と思ったので入門してみた。
takezoe.hatenablog.com
実は以前から Elm コミュニティのエッジな人が Idris すごいと言ってて気になっていて、ちょうどバージョンも最近 1.0 になったばかりというのもあってタイミングとして良いと思った。
出来たのがこれ。
github.com
■ ■ □ ■ ■
■ ■ □ □ ■
□ □ ■ □ ■
■ □ □ □ □
■ ■ ■ □ ■
33
■ ■ □ ■ ■
■ ■ □ □ ■
□ □ ■ ■ ■
■ □ ■ ■ ■
■ ■ ■ ■ ■
12
■ ■ ■ ■ ■
■ □ ■ ■ ■
□ □ □ ■ ■
■ □ ■ ■ ■
■ ■ ■ ■ ■
21
Cleared! Press any key to continue.
ライツアウトを知らない人はググってください。
依存型の旨味を感じたかった
依存型を使うと、値から型を作ったりということができる。例えば「長さ n のベクトル」だったら Vect n のようになる。そうすると、 IndexOutOfBounds 例外を未然に防げる。これが Elm とかだと範囲を超えたら Maybe が返るから例外は出ないんだけど、確かに Maybe を取得した後に即座に分岐して Nothing の方に Debug.crash "ここに来ることはあり得ない"
とか書いたりするので、それを防げるのは嬉しいのかもしれない。そういう期待があったのと、それ以外の用途が知りたいという動機があった。
お題にライツアウトを選ぶのは、以前からオセロとか 15 パズルみたいな盤面を使うゲームを使う時に、上で触れた「いちいち Maybe で面倒」問題が発生しやすいのを感じていたから。
実装例（一部）
今回は Lights n という型で長さ n の正方形を表したいので、２次元のベクトルの別名とする。型の別名は次のように書く。
Lights : Nat -> Type
Lights n =
Vect n (Vect n Bool)
Lights n は自然数（Nat 型）の引数 n を取って型を作る関数とみなせるので、 Nat -> Type 。
続いて２次元のインデックスも型にしておく。長さ n までのインデックスが Fin n なので、それをタプルにする。（Fin は Finite Set の意味でインデックスというよりは有限な集合的な意味らしいのだが、詳しいことはよくわからない。）
Position : Nat -> Type
Position n =
(Fin n, Fin n)
ライツアウトの場合、押したボタンとその上下左右のボタンが反転するので、全てのインデックスが盤面をはみ出ないようにしたい。次の関数は、指定した分だけ移動した時に成功したら Just (Position n)、失敗したら Nothing を返す関数。
move : Integer -> Integer -> Position n -> Maybe (Position n)
move {n} dx dy (x, y) =
case (integerToFin (finToInteger x + dx) n, integerToFin (finToInteger y + dy) n) of
(Just x, Just y) => Just (x, y)
_ => Nothing
一応出来た…がこれで良いのだろうか。 finToInteger で整数にして integerToFin でインデックスに戻しているところが、すごく負けた感がする。結局そこで整数にするのかよ。ちなみに最初の {n} は、型引数にある n の値をそのまま持ってこれる。なにやらすごく不思議な感じがする。
メインループは Elm アーキテクチャで実装
CUI だけど GUI とみなせば、見慣れた Elm アーキテクチャが使える。
モデルは、タイトル画面とプレイ中の状態のいずれか。
data Model =
Start | Playing (Lights Main.size)
メッセージは、タイトルからゲーム画面への遷移と盤面を押すアクション。
data Msg
= NoOp
| StartGame
| Toggle (Position Main.size)
アップデート。本当は最初の盤面をランダムにしたかったが、その辺は未学習なので決め打ち。 NoOp とかあり得ないモデルとメッセージの組み合わせがやはり出てきてしまったのが無念。その辺も型でなんとかできることを期待しているのだが。
update : Msg -> Model -> Model
update msg model =
case (msg, model) of
(NoOp, _) =>
model
(StartGame, _) =>
Playing $ toggle (position 2 2) (empty size)
(Toggle position, Playing lights) =>
Playing $ toggle position lights
_ =>
model
ビューは、モデルが与えられた時に画面に表示する情報と入力をどうメッセージに変換するかをタプルで返す。Html msg のように Output msg のような別名を与えてもいいかもしれない。
view : Model -> (String, String -> Msg)
view model =
case model of
Start =>
("Press any key to start.", \_ => StartGame)
Playing lights =>
if isEmpty lights then
("Cleared! Press any key to continue.", \_ => StartGame)
else
(format lights, decodePosition)
感想
正直、ここまでで依存型の恩恵を肌で感じ取るには至らなかった。「盤面の長さが５なんだけど８とかが来るのを未然に防げてよかったー」みたいな気持ちにならない。null が来ないのを未然に防ぐのに比べて、ある範囲の整数値が来ないことはあまり嬉しくないということなのかなんなのか。あるいは使い方が間違っている？その辺り、 Idris 脳にならないと普通の Haskell を書いてしまうので難しいと思った。
当初の予定としては JavaScript に吐き出して HTML のデモを作ろうと思ったのだが、 FFI に関するドキュメントが古いのか、うまくインストールが出来なかったので諦めた。
コンパイル時のエラーメッセージに関しては、親切にしようという努力は見られるものの結構おかしな事を言ってくるので注意が必要。本当は「変数が見つからない」なのに「型が曖昧」と怒ってきたり、パターンマッチでコンストラクタ名を間違えるとワイルドカードになってコンパイルが通ってしまったり、色々と問題がある。
あと、型システムに関しても微妙に Haskell と違う点があって、Wiki にまとめられている。さらっと書かれてるけど「deriving does not work yet」めっちゃ辛い。
現時点での感想は以上です。
