Phantom Type（幽霊型）入門ですー＞ω＜

この記事を改めて書き直しましたのです＞ω＜

できれば、こちらの記事を見てもらいたいのですー＞ω＜

あいさつ＞ω＜

みなさん、お久しぶりです、月影です＞ω＜

「いつかブログを書こう」と思っていたら、なんと一週間もたってしまいました(ﾟдﾟ)！

「いつか」なんて考えていちゃいけませんね、「今でしょ！」の精神でいかなくちゃです＞ω＜

というわけで、今回はPhantom Typeについてのお話です＞ω＜

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

Phantom Type…、幽霊型…

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

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

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

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

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

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

1

data PhantomType x a = PhantomType a

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

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

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

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

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

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

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

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

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

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

1
2
3

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とtailの実装ですー＞ω＜

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

1
2
3
4
5
6
7
8
9

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

data Empty
data NonEmpty

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

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

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

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

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

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

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

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

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

1
2
3
4
5

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とtailを実装しますです＞ω＜

6/22追記 (このtail関数は動きません。以下のtail関数に対する記述も嘘になります。すみませんです＞＜)

1
2
3
4
5

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

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

できましたー＞ω＜

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

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

1
2
3
4

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やtailというバグをコンパイル時に見つけられるようにしました。

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

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

終わりに(｀・ω・‘)

みなさん、こんな長い記事に付き合っていただきありがとうございますです＞ω＜

この記事を読んで、型 がコンパイルを邪魔するいじわるさんではないことを分かってもらえたならわたしとしては本望です＞ω＜

また、この記事を書いたのはまだまだHaskell力の未熟な月影ですので、どこか間違ってるかもしれないです(´・ω・｀)

間違っているところを見つけた時はそっと教えて下さいm(_ _)m

本当の最後に、この記事のアイデアとなった型安全なheadとtailを考えている時にTwitterで色々教えてくださった@func_hsさん、@fumievalさん、分かりやすいScalaでのPhantom Typeのスライドを公開している@maeda_、GADTsの記事ですがものすごく参考になった@cpp_akiraさん、その他どこかでわたしの記事に関わっているみなさん、この記事を読んでくださったみなさんに最大限の感謝を！！

おまけですー＞ω＜

どこかに書こうと思って書きどころを逃したものですー＞ω＜

参考記事

上に挙げた二つと、Haskell WikiにあるPhantom Typeのページですー＞ω＜

GADTについて

GHCには一般化代数データ型という拡張があり、今回作ったnil、consと同様のことを

1
2
3
4
5
6

data Empty
data NonEmpty

data SafeList x a where
  Nil  :: SafeList Emoty a
  Cons :: a -> SafeList y a -> SafeList NonEmpty a

のようにデータ構築子の中に隠蔽して書くことができます。

これの方が 抜け道がなく さらに安全なので、通常はこちらを用いたほうがいいかと思いますです―＞ω＜

詳しくは上に挙げた@cpp_akiraさんの記事を参照してくださいです＞ω＜

他の言語について

Phantom Typeは、Haskellに限らず、ScalaやOCamlといった型付きの関数型言語でも使えるテクニックですー＞ω＜

それにC++やD言語でもテンプレートを使えば出来るはずですー＞ω＜

Javaはちょっと自信ありません(´・ω・｀;)　でもScalaで出来るのだからできそうな気もしますです＞ω＜

これで、ソフトウェア開発の可能性が少し広がったのでは？？

では、型を守ってバグの無いプログラミングライフを、ですー＞ω＜