Haskell:具有幻像变量的数据的异构列表

目前，我正在学习关于存在性量化，幻像类型和GADT的知识。如何创建带有幻像变量的数据类型的异构列表？例如:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}

data Toy a where
  TBool :: Bool -> Toy Bool
  TInt  :: Int  -> Toy Int

instance Show (Toy a) where
  show (TBool b) = "TBool " ++ show b
  show (TInt  i) = "TInt "  ++ show i

bools :: [Toy Bool]
bools = [TBool False, TBool True]

ints  :: [Toy Int]
ints  = map TInt [0..9]

具有以下功能可以:

isBool :: Toy a -> Bool
isBool (TBool _) = True
isBool (TInt  _) = False

addOne :: Toy Int -> Toy Int
addOne (TInt a) = TInt $ a + 1

但是，我希望能够这样声明一个异类列表:

zeros :: [Toy a]
zeros =  [TBool False, TInt 0]

我尝试使用一个空的类型类通过以下方式限制a的类型:

class Unify a
instance Unify Bool
instance Unify Int

zeros :: Unify a => [Toy a]
zeros =  [TBool False, TInt 0]

但是以上内容无法编译。我能够使用存在量化来获得以下信息:

data T = forall a. (Forget a, Show a) => T a

instance Show T where
  show (T a) = show a

class (Show a) => Forget a
instance Forget (Toy a)
instance Forget T

zeros :: [T]
zeros = [T (TBool False), T (TInt 0)]

但是以这种方式，我无法将基于a中Toy a的特定类型的函数应用于T，例如上面的addOne。

总之，在不忘记/丢失幻象变量的情况下，我可以通过哪些方式创建异构列表？

最佳答案

从Toy类型开始:

data Toy a where
  TBool :: Bool -> Toy Bool
  TInt :: Int -> Toy Int

现在，您可以将其包装在一个存在类中，而不必过度使用类系统:

data WrappedToy where
  Wrap :: Toy a -> WrappedToy

由于包装器仅保存Toy，因此我们可以将其解包并返回Toy:

incIfInt :: WrappedToy -> WrappedToy
incIfInt (Wrap (TInt n)) = Wrap (TInt (n+1))
incIfInt w = w

现在您可以区分列表中的内容:

incIntToys :: [WrappedToy] -> [WrappedToy]
incIntToys = map incIfInt

编辑

正如Cirdec所指出的那样，可以将不同的部分分开来取笑:

onInt :: (Toy Int -> WrappedToy) -> WrappedToy -> WrappedToy
onInt f (Wrap t@(TInt _)) = f t
onInt _ w = w

mapInt :: (Int -> Int) -> Toy Int -> Toy Int
mapInt f (TInt x) = TInt (f x)

incIntToys :: [WrappedToy] -> [WrappedToy]
incIntToys = map $ onInt (Wrap . mapInt (+1))

我还应该指出，到目前为止，没有任何东西可以证明Toy GADT的合理性。 bheklilr使用普通代数数据类型的更简单方法应该可以正常工作。