2月 21 2014

型安全なリストを作るのです(｀・ω・´) ～その2、GADTsと依存型＞ω＜

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

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

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

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

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

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

SafeList_by_PhantomType.hs

{-# 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の簡単な例ですー＞ω＜

{-# 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を使って型安全なリストを定義したときは必要になった、

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という二つのタグしか用意しなかったことが原因となっていますです(｀・ω・´)

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

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

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は自然数を表わす型であって、型が自然数のような構造を持っているわけではないのです)

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

-- 自然数のような構造を持った型であることを表わす型クラスですー＞ω＜
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も定義して、前回と同じくこれらの定義が上手く動くのか試してみましょー＞ω＜

SafeList_by_GADTs.hs

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

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

Moon? Shadow!

kagamilove0707's blog

型安全なリストを作るのです(｀・ω・´) ～その2、GADTsと依存型＞ω＜

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

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

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

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

GADTsとは(・ω・?

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

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

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

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

`SafeList`を改良するのです！！

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

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

結びに……

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

Comments

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

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

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

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

GADTsとは(・ω・?

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

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

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

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

SafeListを改良するのです！！

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

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

結びに……

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

Comments

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

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

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

`SafeList`を改良するのです！！

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