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

Question

我现在正在学习存在主义量化、幻影类型和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)]

但是这样，我不能将基于Toy a中特定类型的Toy a的函数应用到T，例如上面的addOne。

总之，有哪些方法可以在不忘记/丢失幻影变量的情况下创建异构列表？

Answer 1

从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使用普通代数数据类型的更简单的方法应该工作得很好。

Answer 2

几天前有一个非常类似的question。

在你的情况下

{-# LANGUAGE GADTs, PolyKinds, Rank2Types #-}

data Exists :: (k -> *) -> * where
  This :: p x -> Exists p

type Toys = [Exists Toy]

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

很容易消除一个存在主义：

recEx :: (forall x. p x -> c) -> Exists p -> c
recEx f (This x) = f x

如果您有一个用于Toy数据类型的递归

recToy :: (Toy Bool -> c) -> (Toy Int -> c) -> Toy a -> c
recToy f g x@(TBool _) = f x
recToy f g x@(TInt  _) = g x

您可以映射包装好的toy

mapToyEx :: (Toy Bool -> p x) -> (Toy Int -> p y) -> Exists Toy -> Exists p
mapToyEx f g = recEx (recToy (This . f) (This . g))

例如

non_zeros :: Toys
non_zeros = map (mapToyEx (const (TBool True)) addOne) zeros

这种方法类似于@dfeuer的回答，但并不是特别的。

Answer 3

由元素类型列表索引的普通异构列表是

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

data HList l where
    HNil :: HList '[]
    HCons :: a -> HList l -> HList (a ': l)

我们可以将其修改为在某些f :: * -> *中保存值。

data HList1 f l where
    HNil1 :: HList1 f '[]
    HCons1 :: f a -> HList1 f l -> HList1 f (a ': l)

它可以用于编写zeros而不忘记类型变量。

zeros :: HList1 Toy [Bool, Int]  
zeros = HCons1 (TBool False) $ HCons1 (TInt 0) $ HNil1