Phantom Type、GADTsで書いてみた型安全なリストです＞ω＜

SafeList_by_GADT.hs

-- Generalized Algebraic Data Types(一般的代数データ型)が使えるようになるみたいです＞ω＜
{-# LANGUAGE GADTs #-}
module Main where
import Prelude hiding (head)

-- Phantom Typeではラッパー関数が必要でしたけれど、
-- GADTではデータ構築子の返す型を別々にできるみたいですー＞ω＜
-- シンプルで堅牢で、とても素敵ですっ＞ω＜
data Empty
data NonEmpty
data SafeList a x where
  Nil :: SafeList a Empty
  Cons :: a -> SafeList a x -> SafeList a NonEmpty

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

main = do
  print $ head (Cons "＞ω＜" Nil)
  print $ head Nil -- 例によってコンパイル時にエラーです＞ω＜

SafeList_by_PhantomType.hs

-- 存在量子化されたデータ構築子が使えるみたいです＞ω＜←よく分かってないヾ(ﾟДﾟ )ｫｨｫｨ
{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Prelude hiding (head)

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

-- 上のStrongListだけでは型が決定されないのでラップする関数が要ります＞ω＜
nil :: SafeList a Empty
nil = Nil
cons :: a -> SafeList a x -> SafeList a NonEmpty
cons x ys = Cons x ys

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

main = do
  print $ head (cons "＞ω＜" nil)
  print $ head nil -- コンパイル時にエラーになります＼_(・ω・`)ココ重要！