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

Question

当我尝试创建一个返回函数Thing a（ThingGADT 在哪里）时，我目前正在与类型检查器进行斗争。一个最小的例子：

{-#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。但是，这是令人惊讶的，因为使用常规求和类型，您可以执行以下操作：

data Thing = Foo Int | Bar String

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

是否有办法通过 GADT 参数返回类型参数？

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

Answer 1

你把量词搞混了。

combine :: [Thing a]

意味着（forall语法中隐含的）

combine :: forall a. [Thing a]

本质上，无论是什么，combine都需要是 a ，因为是由调用 的代码选择的。或者，从另一种意义上来说，[Thing a]aacombine

-- 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"]