6月 23 2013

型安全なリストに対する補足とGADTsの話ですー＞ω＜

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

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

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

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

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

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

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）を使って定義してみますです＞ω＜

{-# 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はこんな風に書けますです＞ω＜

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

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

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

これなら、

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

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

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

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

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

思うこと(｀・ω・´)

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

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

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

programming

Haskell