{-# LANGUAGE ExistentialQuantification #-}module Main whereimport Prelude hiding(head, tail)dataEmptydataNonEmptydataSafeList x a = forall y. Cons a (SafeListya)
|Nilnil :: SafeListEmpty a
nil = Nilcons :: a -> SafeList x a -> SafeListNonEmpty a
cons x xs = Cons x xs
head :: SafeListNonEmpty a -> a
head (Cons x _) = x
tail :: SafeListNonEmpty 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 withconstructorCons :: 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
{-# LANGUAGE GADTs #-}-- GADTsを使うためのLANGUAGEプラグマですー＞ω＜dataEmptydataNonEmptydataSafeList x a whereNil :: SafeListEmpty a
Cons :: a -> SafeList x a -> SafeListNonEmpty a
{-# LANGUAGE GADTs #-}module Main whereimport Prelude hiding(head, tail, foldr)-- 自然数のような構造を持った型であることを表わす型クラスですー＞ω＜classNat x wheredataZerodataSucc xinstanceNatZerowhereinstanceNat x => Nat(Succx)wheredataSafeList x a whereNil :: SafeListZero 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))'
{-# LANGUAGE ExistentialQuantification #-}module Main whereimport Prelude hiding(head)dataEmptydataNonEmptydataSafeList x a = forall y. Cons a (SafeListya)
|Nil
最初の一行目は言語プラグマで、データ構築子などの中でforallを使うときに必要です＞ω＜
三行目で、これからオーバライドする予定のPreludeのheadを隠しています＞ω＜
五、六行目では右辺のないデータ型を定義しています。これはEmpty Data Declsといって、データ構築子のない型を宣言できます。これについてはあとで話しますです＞ω＜
八行目、ようやくSafeListの定義です＞ω＜
最初のforall y. Cons a (SafeList y a)という型、再帰的になっていてリストを表しています。また、型変数xが一度も出てきてないことにも注目です＞ω＜ （forall y.というのは英単語の通り(?)、yの型はひとまず何でもいいことを表わすていますです）
{-# LANGUAGE ExistentialQuantification #-}module Main whereimport Prelude hiding(head)dataEmptydataNonEmptydataSafeList x a = forall y. Cons a (SafeListya)
|Nilnil :: SafeListEmpty a
nil = Nilcons :: a -> SafeList x a -> SafeListNonEmpty a
cons x xs = Cons x xs
head :: SafeListNonEmpty 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: SafeListNonEmptya0
Actual type: SafeListEmptya0
In the first argument of `head', namely `nil'
In the second argument of `($)', namely `head nil'
tail :: SafeListNonEmpty 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 withconstructorCons :: 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 :: SafeListNonEmpty 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 withconstructorCons :: 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
前回の記事では、Phantom Typeを主張するためにあえて普通のデータ型を使って定義しましたが、ここでは簡潔と単純のためにGADTs（Generalized Algebraic Data Types）を使って定義してみますです＞ω＜
1
2
3
4
5
6
7
8
9
10
{-# LANGUAGE GADTs #-}module Main wheredataEmptydataNonEmpty xinfixr5 :::dataSafeList x a whereNil :: SafeListEmpty a
(:::) :: a -> SafeList x a -> SafeList (NonEmpty x) a
{-# LANGUAGE ExistentialQuantification #-}module Main whereimport Prelude hiding(head, tail)dataEmptydataNonEmptydataSafeList x a = forall y. Cons a (SafeListya)
|Nilderiving(Show)
最初の一行目は言語プラグマで、データ構築子などの中でforallを使うときに必要です＞ω＜
三行目で、これからオーバライドする予定のPreludeのheadとtailを隠しています＞ω＜
五、六行目では右辺のないデータ型を定義しています。これはEmpty Data Declsといって、データ構築子のない型を宣言できます。これについてはあとで話しますです＞ω＜
八行目、ようやくSafeListの定義です＞ω＜
最初のforall y. Cons a (SafeList y a)という型、再帰的になっていてリストを表しています。また、型変数xが一度も出てきてないことにも注目です＞ω＜ （forall y.というのは英単語の通り、任意の型変数yが存在することを表しています）
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: SafeListNonEmptya0
Actual type: SafeListEmptya0
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) という考え方がありますです。
