前回のあらすじですー＞ω＜

Phantom Typeを駆使して空リストに適用しようとすると、コンパイル時にエラーを吐く型安全なリストを定義したのです(｀・ω・´)

しかし、tailはよく分からないエラーに阻まれて定義することができなかったのです……＞＜;

今回は型安全なtailはどうやったら実現可能か考えてみたいと思いますです＞ω＜

前回のエラーをもう一度確認してみますです。

前回のソースコードとエラーを再掲しておきますです(｀・ω・´)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

{-# 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

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

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

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

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

では早速このエラーを紐解いていくのですー＞ω＜

エラーメッセージをよくよく観察してみますです。

すると、とりあえず21行目の20文字目でエラーが起きていることが分かりますです(｀・ω・´)

(↑当たり前すぎるかもしれませんが、原因の分からないバグというのは大抵そういうところに潜むものなのではないかと思いますです)

その21行目とは、ここのことになります。

1

tail (Cons _ xs) = xs

で、更に20文字目というと、ちょうど右辺のxsのことになりますです(｀・ω・´)

さて、このxsの型は、

1

forall y. SafeList y a

になりますです(｀・ω・´)

……みなさん、少し思い出してみて欲しいのです(｀・ω・´)

このforallがどこにあったかを

1
2

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

そう、このforallはSafeListの宣言の中にあって、yはそこに 隠されて いたのです！

forallを使うと、型変数を 隠す ことができますです＞ω＜　しかし、その 隠した型は基本的に外へ取り出して返すことができない のです

（この「外へ取り出して返すことができない」という表現を見て、IOモナドのことを思い出した方は、中々の筋のいい方です。なぜなら、forallはIOモナドの元になるSTモナドにも使われているのです！）

しかし、外側へ返すのではなく内側で処理をするようにすることはできますです(｀・ω・´)

なので、このようにすればとりあえずtailは実装できますです＞ω＜

1
2
3

{-# LANGUAGE Rank2Types #-}
tail' :: (forall x. SafeList x a -> b) -> SafeList NonEmpty a -> b
tail' f (Cons _ xs) = f xs

関数を引数で受け取って、それでtailを処理するというわけです

o(*≧д≦)oこんな不恰好なtailじゃ満足はしないのです

さっき作ったtail'では、

• 型が変わってしまっているし、
• 関数に 渡されるリストがEmptyかNonEmptyか分からない

という問題がありますです＞＜;

特に二つ目は大きな問題だと思うのです！　何せ、このままではheadにもtailにも渡すことができないのです…

では、それをどうやって解決したらいいのでしょうか？？

そのためのキーワードが二つありますです。

一つは「GADTs」で、もう一つは「依存型」です＞ω＜

まずはGADTsから始めていきますですー＞ω＜

GADTsとは(・ω・?

GADTsとは、GHC拡張の一つでGeneralized Algebraic Data Typesの略。日本語にすると、一般的代数的データ型のことです(｀・ω・´)

……なんて言われて、「この言葉論文で見たことある！（進研ゼミ風）」と理解できる人にはこの記事は必要ないと思うので、もう少し踏み込んで解説しますです

まずは、何はともあれGADTsの簡単な例ですー＞ω＜

1
2
3
4
5
6
7
8

{-# LANGUAGE GADTs #-} -- GADTsを使うためのLANGUAGEプラグマですー＞ω＜

data Empty
data NonEmpty

data SafeList x a where
  Nil  :: SafeList Empty a
  Cons :: a -> SafeList x a -> SafeList NonEmpty a

これはさっきのSafeListの定義をGADTsを使って書きなおした例ですー＞ω＜

さて、肝心の定義が始まるのは6行目からですが、普通に定義した場合と一体何が違っているのでしょうか(・ω・?

まず最も大きな違いとして、whereを用いて、まるでclassの定義のようになっているところがありますです(｀・ω・´)

しかし、これはGADTsの本質ではないのです

では一体どこが本質になるのでしょうか？？

data以下のインデントされた部分がコンストラクタの定義になっているのは、何となく想像できると思いますです

実際、この部分はコンストラクタの名前 :: コンストラクタの型という定義になっていますです(｀・ω・´)

例えば、みなさんのよく知っているEitherを敢えてGADTsで書き下したとしたら、

1
2
3

data Either l r where
  Left  :: l -> Either l r
  Right :: r -> Either l r

のようになりますです＞ω＜

と、ここで注目してもらいたいのは、GADTsでは コンストラクタの返り値の型 まで指定することができる、という点なのです

当然ながら、コンストラクタの返り値はそのデータ型になりますが、GADTsを使うことでそのパラメーターの型を指定することができるようになるのです！！

つまり、通常のデータ型とPhantom Typeを使って型安全なリストを定義したときは必要になった、

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

といった関数の機能までもGADTsを使った定義、

1
2
3

data SafeList x a where
  Nil  :: SafeList Empty a
  Cons :: a -> SafeList x a -> SafeList NonEmpty a

では内包している、というわけなのですー＞ω＜

Nilの返り値部分がSafeList Empty aになっていること、Consの返り値がSafeList NonEmpty aになっていることからもそれが確認できると思いますですー＞ω＜

また、GADTsを使った定義ではSafeList Boolean aのような意味のない意図しない型が作られてしまうことを回避することもできますですー＞ω＜

実のことを言えば、前回も本来ならこのGADTsを使ってSafeListを定義するべきだったのですが、いきなりこれを使ってしまうと説明することが増えて分かりにくくなってしまうと思い避けることにしたのです(｀・ω・´)

長さを型にするのですー＞ω＜

前のセクションではGADTsについてお話しましたが、さっきの話だけでは何も解決できそうにありませんです＞＜;

なので、ここでは前のSafeListの何が問題だったのか、少し踏み込んで考察してみるのです＞ω＜

SafeListの問題なところ(｀・ω・´)

前に定義したtail'の問題点として、

• 関数に 渡されるリストがEmptyかNonEmptyか分からない

というものがありましたです(｀・ω・´)

これは、SafeListに付けるタグとして、EmptyとNonEmptyという二つのタグしか用意しなかったことが原因となっていますです(｀・ω・´)

この問題を回避するにはどのようにしたらよいのです？？

最も簡単な方法としては、

1
2
3
4
5

data Empty
data Size1
data Size2
data Size3
-- and more...

のように複数のタグを用意する方法が思いつくかもしれませんが、これはあまりにナンセンスですし、そもそも上手くいかないのです＞＜;;

では一体全体、どうしたらよいのでしょうか(・ω・?

自然数を定義しますです＞ω＜

さてみなさん、少し話が変わりますが、次のようにしてHaskellで自然数を定義したことがある方は多いのではないのでしょうか？？

1
2

data Nat = Zero
         | Succ Nat

（0は自然数じゃないとか些細なことは言わないでくださいです）

Zeroが単位元で、Succ NatがNatの次の数を表わす、という再帰的な構造となっているわけです(｀・ω・´)

ところで、このNatをSafeListのタグとして用いることができれば、問題は解決するような気がしませんですか(・ω・?

要するに、タグをNonEmptyとEmpty――あるかないか、という情報しか持たなかった状態から、 タグ自身がそのリストの長さの情報を持つ ようにすることができれば、現状のSafeListの問題は解決するのではないでしょうか？？

型レベルの 自然数を定義しますです＞ω＜

とは言ったものの、タグにするためには自然数が型によって表現されなければいけないです＞＜; (さっき示したNatは自然数を表わす型であって、型が自然数のような構造を持っているわけではないのです)

しかし、そのような型は意外と簡単に定義することができますです(｀・ω・´)

1
2
3
4
5
6
7
8

-- 自然数のような構造を持った型であることを表わす型クラスですー＞ω＜
class Nat x where

data Zero
data Succ x

instance Nat Zero where
instance Nat x => Nat (Succ x) where

このようにして定義された型は、自然数の何であるか、という情報をその型自身が持っていることになりますです(・ω・、)

例えば、自然数の2であれば、対応する型は、

1

Succ (Succ Zero)

ですし、5であれば、

1

Succ (Succ (Succ (Succ (Succ Zero))))

となって、一目瞭然で何の数の型か分かるわけですー＞ω＜

そこらへんが、自然数であることしか分からないさきほどのNatとは違うところ、というわけなのです！

SafeListを改良するのです！！

新しくタグとするべき型は手に入れました(｀・ω・´)

あとはアンパンマンよろしく、「新らしい型よ！」とSafeListにNat型クラスの型を当てはめればいいわけです＞ω＜

そのようなSafeListの定義はこんな風になりますです

1
2
3

data SafeList x a where
  Nil  :: SafeList Zero a
  Cons :: Nat x => a -> SafeList x a -> SafeList (Succ x) a

ここで注目すべきは、コンストラクタConsの返り値です！！
タグとなる型の部分がSucc xとなっていて、Consによって要素数が1増えることが型に表われていますです！！

これは中々興味深いのではないのでしょうか(・ω・?

最後に、目的のtailですー＞ω＜

では、最後の仕上げとしてtailを定義しますですー＞ω＜

これは簡単ですー＞ω＜

1
2

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

これも、引数のタグがSucc xに対して、返り値のタグがxとなっていて、要素数が1減ることが示されていますですー＞ω＜

では、ついでにheadも定義して、前回と同じくこれらの定義が上手く動くのか試してみましょー＞ω＜

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

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

-- 自然数のような構造を持った型であることを表わす型クラスですー＞ω＜
class Nat x where

data Zero
data Succ x

instance Nat Zero where
instance Nat x => Nat (Succ x) where

data SafeList x a where
  Nil  :: SafeList Zero a
  Cons :: Nat x => a -> SafeList x a -> SafeList (Succ x) a

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

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

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

そして、これをコンパイルしてみると……、

SafeList_by_GADTs.hs:27:16:
    Couldn't match type `Zero' with `Succ x0'
    Expected type: SafeList (Succ x0) a0
      Actual type: SafeList Zero a0
    In the first argument of `head', namely `Nil'
    In the second argument of `($)', namely `head Nil'
    In a stmt of a 'do' block: print $ head Nil

SafeList_by_GADTs.hs:29:34:
    Couldn't match type `Zero' with `Succ x1'
    Expected type: SafeList (Succ x1) [Char]
      Actual type: SafeList Zero [Char]
    In the second argument of `Cons', namely `Nil'
    In the first argument of `tail', namely
      `(Cons "\65310\969\65308" Nil)'
    In the first argument of `head', namely
      `(tail (Cons "\65310\969\65308" Nil))'

きました＞ω＜！！

tailの部分でもキチンとエラーが表示されていますです＞ω＜

これで今回の目的は大方果たせたのです＞ω＜

ところで、依存型とは何だったのです？？

途中でキーワードとか語っておきながら全く説明がありませんでした、依存型さん……＞＜;

ですが、わたしたちはもうこの依存型を存分に使っていますです！！

どういうことかって(・ω・?

思い出してみて欲しいのです！！
わたしたちは、SafeListに要素の数を 依存 させて、型安全なリストを作りました(｀・ω・´)

このように、型に値を依存させることを、依存型と言いますです＞ω＜
（Haskellの場合は完全に値を型にすることはできないので、値のような型ということになりますですが……）

言っていることは何だか難しそうですが、今回作ったSafeList型そのものだと思えば理解できるはずですー＞ω＜

結びに……

前回の記事も含めて読んで下さったみなさん
今回の記事だけでも読んで下さったみなさん

こんな長い記事たちにお付き合いいただきどうもありがとうございましたですー＞ω＜

みなさまはこの記事たちを読んで、型についての認識はどのようになりましたでしょうか？？

「依存型を使ってコンパイル時に見つけられるバグを増やしたい」なんて思ってもらえたなら、わたしとして本望の限りですー＞ω＜

また、HaskellやOCamlなどのプログラムを書くのが上手な人がよく言う言葉に、

「 コンパイルは証明だ 」

というものがありますです

これは、カリーハワード同型（Wikipedia参照）のことを指して言っているのだと思われますが、わたしにはこの言葉は、

「 コンパイルは（正しく動くことの）証明だ 」

と言っているように思えてならないのですー＞ω＜

コンパイラが「OK」と言ってくれれば、少なくとも型レベルでは安全なプログラムであることが保証されるわけ、なのですのでー＞ω＜

ちなみに、前回や今回の内容は、言語によって制限がある程度はあると思いますが、別の言語でも応用することは十分にできるはずです

特に、ScalaやOCamlと言った言語ならほぼ完璧に再現することができるはずですー＞ω＜

JavaやC#でも少し大変ですが（そしてキャストを使いたくなりますが）、幽霊型を使うことはできるはずです＞＜;

というわけでみなさん、コンパイルが通らないからってunsafeCoerceで型を騙したりせず、素敵な型安全ライフをー、なのですー＞ω＜

参考や謝辞などですー＞ω＜

まず、@func_hs
さんや@fumieval
さん、@pasberth
さんなど（ぱっと思い出せた方だけしか上げられなくてもうしわけないです…）からは、数え切れないほどの知識とインスピレーションを頂きましたです

他には、この記事や前回の記事を書く際の資料として、

• Phantom Type in Scala - http://www.slideshare.net/maedaunderscore/phatom-type-14612078
• GADTs使ってみた - Faith and Brave - C++で遊ぼう - http://faithandbrave.hateblo.jp/entry/20111201/1322718742

などを参考にさせていただきました（これももっとあったはずなのですが、特に整理していなかったので、思い出し次第追加していきたいです＞ω＜）

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

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

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

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

1
2
3
4
5
6
7
8
9

{-# 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。これは単純にリストの終端ですー＞ω＜

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

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

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

1
2

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

できましたー＞ω＜

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

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

{-# 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も定義できるんじゃないのか？

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

1
2

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も定義できるようにしますです＞ω＜

お久しぶりですー＞ω＜　気がついたら一ヶ月も経っていてしまいました(´・ω・｀)

前回の記事で実際に動かすことの出来ないtailを公開してしまったので、この記事はその謝罪と説明と補足になります(｀・ω・´)

前回の記事で問題だったところ(・ω・?

問題だったのは、具体的にはここですm9（・∀・）ﾋﾞｼｯ!!

1
2

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

このtailは残念なことに型エラーが出て動かないのです(´・ω・｀)

なぜなのでしょうか？？

出てきたエラーメッセージを見てみます＞＜

SafeList_by_PhantomType.hs:
    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:26: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:26:1
    Expected type: SafeList x a
      Actual type: SafeList y a
    In the expression: xs
    In an equation for `tail': tail (Cons _ xs) = xs

長いエラーですー(((ﾟωﾟ)))

ゆっくりと見ていくと、SafeListのデータコンストラクタ宣言の存在型のyとtailの型に現れるxが同じものだと確証を得られない、というエラーのようです＞＜

このエラーを無くすにはどうしたらいいのでしょう？？

というわけで、作りなおしてみますですー＞ω＜

設計そのものが間違っていたのです(｀・ω・´)

前回の記事では、Phantom Typeを主張するためにあえて普通のデータ型を使って定義しましたが、ここでは簡潔と単純のためにGADTs（Generalized Algebraic Data Types）を使って定義してみますです＞ω＜

1
2
3
4
5
6
7
8
9
10

{-# LANGUAGE GADTs #-}
module Main where

data Empty
data NonEmpty x

infixr 5 :::
data SafeList x a where
  Nil :: SafeList Empty a
  (:::) :: a -> SafeList x a -> SafeList (NonEmpty x) a

dataのあとにwhereがあったり、関数の型宣言みたいだったりしますが、これがGADTsというものですー＞ω＜

また、NonEmptyの定義も微妙に変わっていて、型を一つ受け取るようになっています＞＜　（←じつはGADTs云々よりもこっちの方が重要だったりしますです＞＜

で、こうすると、headとtailはこんな風に書けますです＞ω＜

1
2
3
4
5

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

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

こんな風、というか前回と型が変わっただけで中身はそのままでしたです＞＜

これなら、

1
2

main = do
  print $ head (tail (tail ("＞＜" ::: "＞＜" ::: "＞ω＜" ::: Nil)))

という風にtailを２回適用してからheadしても上手くいきますですー＞ω＜

map関数だって定義できます＞＜

1
2
3

map :: (a -> b) -> SafeList x a -> SafeList x b
map _ Nil = Nil
map f (x ::: xs) = f x ::: map f xs

こんな感じでどうでしょうか？

思うこと(｀・ω・´)

急いで書いた記事なので、文章がややおかしかったり説明不足なところがあると思いますが、許してもらえると嬉しいです＞＜

あと、最初のtailがなぜエラーになったのか実はあまりよく分かっていないので、もう少し深く考えてみたいと思います＞＜

ではでは、ありがとうございましたですっ＞ω＜

あいさつ＞ω＜

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

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

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

というわけで、今回は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を実装しますです＞ω＜

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で出来るのだからできそうな気もしますです＞ω＜

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

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