函数返回 GADT 的任何构造函数的结果

Question

当我尝试创建一个返回 Thing a 的函数（其中 Thing 是 GADT）时，我目前正在与类型检查器发生争执。一个最小的人为示例：

{-#LANGUAGE GADTs, EmptyDataDecls #-}
module Main where

-- Define a contrived GADT
data TFoo
data TBar
data Thing a where
  Foo :: Int -> Thing TFoo
  Bar :: String -> Thing TBar

combine :: [Thing a]
combine = [Foo 1, Bar "abc"]

main :: IO ()
main = undefined

类型检查器对a 不匹配TBar 感到不满。大概这是因为它已经推断出a 是TFoo。但是，这令人惊讶，因为您可以使用常规 sum 类型：

data Thing = Foo Int | Bar String

combine :: [Thing]
combine = [Foo 1, Bar "abc"]

是否有返回 GADT 参数的类型参数？

在人为示例的上下文之外，我需要 GADT，因此我可以键入某些函数以仅获取 Foo，但在此之前我还需要能够仅返回 Things 的列表。

Answer 1

你的量词搞混了。

combine :: [Thing a]

表示（forall 隐含在语法中）

combine :: forall a. [Thing a]

本质上，combine 必须是 [Thing a]，无论 a 是什么，因为 a 是由调用 combine 的代码选择的。或者，在另一种意义上，

-- psuedo-Haskell
combine :: (a :: *) -> [Thing a]

combine 是一个函数，它接受一个类型作为参数，并承诺构造一个该类型的Things 列表。具有这种类型签名的combine 的唯一可能定义是combine = []，加上一堆像[undefined] 等愚蠢的定义。 combine = [Foo 1] 也不起作用，因为a 没有被推断出来，因为设置combine 的不是a；是用户。

你想要

-- psuedo-Haskell
combine :: [exists a. Thing a]

这意味着“combine 是一个事物列表，每个事物都是某种未知类型的 Thing”（每个 Thing 都可以是不同的类型）。 exists 量词是forall 的反面。这意味着combine 的定义可以设置它想要的任何类型，用户将不得不处理它。 Haskell 不支持开箱即用的exists，所以需要定义一个中间数据类型：

data SomeThing = forall a. SomeThing (Thing a)

使用通用量词创建存在量词的语法有点倒退，但想法是你得到

SomeThing :: forall a. Thing a -> SomeThing

这基本上抹去了a是什么的知识。

然后你可以拥有

combine :: [SomeThing]
combine = [SomeThing $ Foo 1, SomeThing $ Bar "abc"]