2月 20 2014

型安全なリストを作るのです(｀・ω・´) ～ その1、Phantom Type（幽霊型）入門ですー＞ω＜

Phantom Typeってなんです(・ω・?

Phantom Type…、幽霊型…

みなさん、ご存知でしょうか(・ω・?

わたしは昔に何度かTwitterで見かけたので、名前だけは知っていました(｀・ω・´)

かっこいい名前だな―って感じです＞ω＜　ファントム・タイプ！！！

で、ちょっと面白そうな香りがしたので調べてみましたのです＞ω＜

Phantom Typeさん、名前は仰々しいですが、その実態は非常に単純なものでした＞ω＜

Phantom Typeとはつまり、こういうことです＞ω＜

data PhantomType x a = PhantomType a

え(・ω・?　どういこと(・ω・?

これだけでは分かりにくいかもしれませんです(´・ω・｀)
ですがよく見てください。PhantomType型は二つの型変数を取りますが、右辺のデータ構築子では一つの型しか使っていません(ﾟдﾟ)！

実は、この 使われていない型 こそがPhantom Typeなのです＞ω＜

って、これじゃPhantom Typeの何がすごいのか全然分かりませんね(´･ω･｀)

というわけで、Phantom Typeのすごさを伝えるため型安全なheadとtailを作ってみたいと思いますです＞ω＜

型安全？？　どういう意味です(・ω・?

まずは、この話からしなければいけませんね(｀・ω・´)

HaskellのPreludeのとある関数には欠陥があります(｀・ω・´)　さて、それはどの関数でしょうか？

答えはheadとtailです＞ω＜　ではなぜこの二つは欠陥品なのでしょう…(・ω・?

それは、このようなコードを書いてみれば分かりますです＞ω＜

main = do
  print $ head []
  print $ tail []

headの型 は[a] -> a、tailの型 は[a] -> [a]なので、コンパイルは通ります＞ω＜　しかし、実行してみると…

*** Exception: Prelude.head: empty list

こんなものが表示されてしまいましたです＞＜;

よくよく考えれば当然ですね…。空のリストに先頭も末尾もありませんです…＞＜;;

そう考えると、headやtailの型はMaybeで包むべきであるように感じますです。しかし、ちょっと考えてみてください。一々headやtailする度に、case ofと括ったりmaybeを使って値を取り出さなければいけない世界を(ﾟдﾟ)！

煩わしいですよね？？

そこで、 型安全 という言葉が出てきますです＞ω＜

headやtailでは空のリストを 型レベル で受け取らないようにする――つまり、コンパイル時にエラーにしてしまおうという考えです＞ω＜

そんなことHaskellで出来るのか！？

出来るんです、そう、Phantom Typeならね

それでは、型安全なheadの実装ですー＞ω＜

型安全なheadに比べてtailを作るのは、ほんの少し難しいので、それは次に回すとして……

今回は。型安全なheadを作ってみますですー＞ω＜

では早速、型安全な操作のできるリストSafeListを定義しますです＞ω＜

{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Prelude hiding (head)

data Empty
data NonEmpty

data SafeList x a = forall y. Cons a (SafeList y a)
                             |Nil

最初の一行目は言語プラグマで、データ構築子などの中でforallを使うときに必要です＞ω＜

三行目で、これからオーバライドする予定のPreludeのheadを隠しています＞ω＜

五、六行目では右辺のないデータ型を定義しています。これはEmpty Data Declsといって、データ構築子のない型を宣言できます。これについてはあとで話しますです＞ω＜

八行目、ようやくSafeListの定義です＞ω＜

最初のforall y. Cons a (SafeList y a)という型、再帰的になっていてリストを表しています。また、型変数xが一度も出てきてないことにも注目です＞ω＜　（forall y.というのは英単語の通り(?)、yの型はひとまず何でもいいことを表わすていますです）

次に、Nil。これは単純にリストの終端ですー＞ω＜

ひと通りの定義をみてきました(｀・ω・´)　しかし、これだけでは型安全なリストは作りにくいです＞＜;

なので次の 補助関数 を定義しますです＞ω＜

nil :: SafeList Empty a
nil = Nil

cons :: a -> SafeList x a -> SafeList NonEmpty a
cons x xs = Cons x xs

型に注目です＞ω＜　わたしが言えることじゃありませんが、Haskellのコードを見た時、ぱっと型を確認する癖をつけておくといいと思いますです＞ω＜

で、その型についてです＞ω＜

nilとcons、その返す型をよく見比べてみてくださいです。

気づきましたか？？　そう、返される型が違うのです(ﾟдﾟ)！

nilはSafeList Empty a、consはSafeList NonEmpty aと。

このとき、EmptyとNonEmptyはSafeListの状態を表す タグ のようになっていますです＞ω＜

空のリストとそうでないリストで型が違う――という、型安全なリストを実装するのにうってつけな性質の持ち主たちですー＞ω＜

これで、EmptyとNonEmptyがEmpty Data Declsされていた理由や、foall y. Cons a (SafeList y a)という型の理由も分かったずです(｀・ω・´)

リストが空かどうかを表す タグ である型が実体化できる必要はないですし、、もしCons a (SafeList x a)のような型だったらSafe NonEmpty aが無限に終わらないリストになってしまうのです(｀・ω・´)

また、この タグ はコンパイル時には意味がありますですが実行時に消えてしまいますです。この、コンパイル時にゆらりと現れて実行時には消えている、というふわふわした感覚が Phantom ―― 幽霊 と言われる所以なのではとわたしは思いますです＞ω＜

それではついに、型安全なheadを実装しますです＞ω＜

head  :: SafeList NonEmpty a -> a
head (Cons x _) = x

できましたー＞ω＜

headはSafeList NonEmpty a――空でないリストを受け取るようになっていて、型安全であることが分かりますです＞ω＜

ひと通り出来上がったので、これが本当に型安全であるのか試してみましょー＞ω＜

SafeList_by_PhantomType.hs

{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Prelude hiding (head)

data Empty
data NonEmpty

data SafeList x a = forall y. Cons a (SafeList y a)
                             |Nil

nil :: SafeList Empty a
nil = Nil

cons :: a -> SafeList x a -> SafeList NonEmpty a
cons x xs = Cons x xs

head  :: SafeList NonEmpty a -> a
head (Cons x _) = x

main :: IO ()
main = do
  print $ head (cons "＞ω＜" nil) -- これはOKですー＞ω＜
  print $ head nil -- これはコンパイルエラーです(｀・ω・´)

ここまでのコードを、まとめてghcででも実行してみますですー＞ω＜

SafeList_by_PhantomType.hs:
    Couldn't match expected type `NonEmpty' with actual type `Empty'
    Expected type: SafeList NonEmpty a0
      Actual type: SafeList Empty a0
    In the first argument of `head', namely `nil'
    In the second argument of `($)', namely `head nil'

おおおおお＞ω＜！

ちゃんとコンパイルエラーになりましたです＞ω＜

Phantom Typeを使って型安全なheadが実装できましたのですー＞ω＜

というわけで次回は型安全なtailの作るとして、次のセクションからはちょっとした閑話休題です(｀・ω・´)

ところで、型ってなんです(・ω・?

少し、Haskellらしく抽象的な話をしますです＞ω＜

抽象的、と言っても圏論が絡んでくる話のように難しくはないので安心してくださいです＞ω＜

今回の記事でわたしは、 型 という言葉を重視して使ってきたつもりです。

では、その型とは一体何だったのでしょうか？？

コンパイルの時に注意してくる面倒くさい奴？？　――それも、きっと間違いではないです＞ω＜

ですが、ただ厄介と一括りに囲って丸めてしまうのではなく、もう少し考えを進めてみてくださいです＞ω＜

話が変わりますが、 契約による設計(Design by Contract : DbC) という考え方がありますです。

これはプログラムの中に契約（引数はこういう値にしなさいー、返り値はこうじゃなきゃダメだぞ！）というものを設定して、守らなければ開発時はプログラムを即時に失敗させる、という開発技法のことです＞ω＜

契約を守らなければ即時に失敗させる――これって、 型 とコンパイルにすごく似ていませんか？？

契約は守らなければプログラムが失敗する、型は守らなければコンパイルに失敗する。

見事な対称性ですー＞ω＜

つまり、わたしが言いたいのはこういうことになりますです＞ω＜

型は、プログラムの最大の契約だ！！

今回は 型レベル で 契約 することで空リストに対するheadのバグをコンパイル時に見つけられるようにしました。

同じように、他のことでも 型レベル で 契約 を結ぶことでもっとたくさんバグをコンパイル時に見つけられるかもしれません。

これは、とても強固なソフトウェアの開発につながるのではないかと思いますです＞ω＜

次回予告ですー＞ω＜

さて、ここでみなさんはこんなことを思うのではないでしょうか？？

(。-`ω-) headと同じようにすればtailも定義できるんじゃないのか？

確かにそんな気もしますです(｀・ω・´) 具体的にはこんなふうにして……

tail :: SafeList NonEmpty a -> SafeList x a
tail (Cons _ xs) = xs

一見これは上手くいきそうです。しかし、実際にコンパイルしてみると……

SafeList_by_PhantomType.hs:21:20:
    Couldn't match type `y' with `x'
      `y' is a rigid type variable bound by
          a pattern with constructor
            Cons :: forall x a y. a -> SafeList y a -> SafeList x a,
          in an equation for `tail'
          at SafeList_by_PhantomType.hs:21:7
      `x' is a rigid type variable bound by
          the type signature for tail :: SafeList NonEmpty a -> SafeList x a
          at SafeList_by_PhantomType.hs:20:9
    Expected type: SafeList x a
      Actual type: SafeList y a
    In the expression: xs
    In an equation for `tail': tail (Cons _ xs) = xs

何だかよく分からないエラーに遭遇してしまいます＞＜

次回はこのエラーを回避して、型安全なtailも定義できるようにしますです＞ω＜

programming

Haskell, TypeSafe