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

Posted 2021-03-31

当我尝试创建一个返回Thing a（其中Thing是GADT）的函数时，我正在与typechecker进行斗争。一个极简的人为例子：

{-#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

typechecker对a与TBar不匹配感到不快。据推测这是因为它已经推断出a是TFoo。但是，这是令人惊讶的，因为您可以使用常规总和类型：

data Thing = Foo Int | Bar String

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

无论如何返回GADT参数的类型参数？

在人为例子的背景之外，我需要GADT，所以我可以输入某些函数来只接受Foo，但在此之前我还需要能够返回一个Things列表。

答案

你已经把你的量词混淆了。

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