GADTsなデータ型をQuickCheckのArbitraryクラスのインスタンスにする

QCWithGADTs.hs

{-# LANGUAGE FlexibleInstances, ExistentialQuantification, StandaloneDeriving, GADTs #-}
module QCWithGADTs where
import Control.Applicative ((<$>), pure)
import Test.QuickCheck (Arbitrary(..), oneof)

{- FOP: Fun with Phantom Tyepsより

Term tをArbitraryのインスタンスにするには、2つやるべきことがある。
  1) 各構成子の結果型が異なる問題を解決する
  2) 構成子によって引数の型が異なる型に特殊化されているので、それぞれの型に対応する
     値を生成できるようにする

1) Term tのarbitraryはTerm tを生成するが、実際にはTerm tはGADTsなので、
   構成子によって結果型が変わる。arbitraryがTerm IntやTerm Boolを同時に
   返すことはできないので、existentialsを使ってtを押しつぶす。このための
   ラッパー型Tを導入する。こうすることでarbitraryメソッドはTを返せばよい
   ことになる。

2) Succの引数はTerm IntでIfの第1引数はTerm Boolのように、構成子によって
   引数の型が異なるため、それぞれの型についてarbitraryを実装する必要がある。
   1)とは違ってTerm IntならTerm Intだけを返すarbitraryを実装すればいいので
   Term tではなくTerm IntをArbitraryのインスタンスにすればよい。
   同様のことをTerm Boolについても行うので、FlexibleInstances言語拡張が
   必要になる。

-}

data Term t where
  Zero   :: Term Int
  Succ   :: Term Int -> Term Int
  Pred   :: Term Int -> Term Int
  IsZero :: Term Int -> Term Bool
  If     :: Term Bool -> Term a -> Term a -> Term a

instance Arbitrary (Term Int) where
  arbitrary = oneof [ pure Zero
                    , Succ <$> arbitrary
                    , Pred <$> arbitrary ]

instance Arbitrary (Term Bool) where
  arbitrary = oneof [ pure $ IsZero Zero
                    , pure $ IsZero (Succ Zero) ]

data T = forall t. Show t => T (Term t)

instance Arbitrary T where
  arbitrary = oneof [ T <$> pure Zero
                    , T <$> Succ <$> arbitrary
                    , T <$> Pred <$> arbitrary
                    , T <$> IsZero <$> arbitrary
                    , do T t <- arbitrary
                         T <$> (If <$> arbitrary <*> pure t <*> pure t)
                    ]

deriving instance Show t => Show (Term t)

instance Show T where
  show (T t) = "T (" ++ show t ++ ")"

{- サンプル出力

Prelude> sample (arbitrary :: Gen T)
T (IsZero (Pred (Pred Zero)))
T (IsZero Zero)
T (IsZero Zero)
T (Zero)
T (IsZero Zero)
T (Succ (Pred (Succ (Succ (Succ (Pred (Pred Zero)))))))
T (IsZero Zero)
T (IsZero Zero)
T (Succ (Pred (Succ Zero)))
T (Pred Zero)
T (If (IsZero (Succ Zero)) (Succ Zero) (Succ Zero))
-}