GADT 类型变量中的 Union

Question

我有一个代表相同想法的 GADT 构造函数，但我需要其中两个，因为类型根据上下文是灵活的。看这个人为的例子：

data A
data B
data C

data Thing a where
  AFoo :: String -> Thing A
  Bar  :: Float -> Thing A
  BFoo :: String -> Thing B
  Baz  :: Int -> Thing B
  Bah  :: Char -> Thing C

AFoo 和 BFoo 代表相同的底层数据概念：一些带有字符串的数据。但在这种情况下，它不止于此。理想情况下 AFoo 和 BFoo 将合并到 Foo，因为它们代表完全相同的东西，但我需要一个像 Thing A 和一个像 [=21] 的类型=].如前所述，某些可以使用 Foo 的上下文需要 Thing A，有些需要 Thing B，因此为了满足类型系统，每个构造函数都需要存在。

如果需要，我当然可以通过切换构造函数来编写一个 "casts" 到所需类型的函数：

fooAsThingA :: Thing a -> Maybe (Thing A)
fooAsThingA t@(AFoo _) = Just t
fooAsThingA (BFoo s) = Just $ AFoo s
fooAsThingA _ = Nothing

（fooAsThingB 也类似）

但这很难看，因为它需要一个我必须传播的Maybe，因为不是所有的Thing B都能变成Thing A（事实上，只有BFoo 可以）。

理想情况下，我想写：

data A
data B
data C

data Thing a where
  Foo :: String -> Thing ??
  Bar :: Float -> Thing A
  Baz :: Int -> Thing B
  Bah :: Char -> Thing C

但我不清楚用什么代替 ??。大概这是表示 A 和 B 联合的某种方式（也许这需要更改此 GADT 的其他构造函数的类型，但这没关系）。

明确一点，如果以上内容有效，我希望提供以下功能：

processThingA :: Thing A -> String
processThingB :: Thing B -> Int
processThingC :: Thing C -> Float

然后，我将能够执行以下所有操作：

processThingA $ Foo "Hello"
processThingB $ Foo "World"

processThingA $ Bar 3.14
processThingB $ Baz 42

processThingC $ Bah '\n'

tl;dr 在第一个代码段中，是否可以将 AFoo 和 BFoo 合并为一个 Foo 类型为 Thing A 和 Thing B?

编辑： 注意：除 A 和 B 之外，还有其他 EmptyDataDecls 用于 Thing a。我添加了 C 作为示例。

Answer 1

一个可能的解决方案如下，虽然我觉得不太优雅

我们首先定义一个GADT和一个类型class为"A or B":

{-# LANGUAGE DataKinds, KindSignatures, GADTs, EmptyCase,
             ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

data Sort = A | B | C | D

data AorB (s :: Sort) where
  IsA :: AorB 'A
  IsB :: AorB 'B

class IsAorB (s :: Sort) where
  aorb :: AorB s

instance IsAorB 'A where aorb = IsA
instance IsAorB 'B where aorb = IsB

然后我们在我们的类型中利用我们的类型class。这将导致 Foo 需要更多 space，因为它需要在运行时存储 typeclass 字典。这是少量的开销，但仍然很不幸。另一方面，这也可以在运行时辨别 Foo 中使用的 s 实际上是 A 还是 B.

data Thing (s :: Sort) where
  Foo :: IsAorB s => String -> Thing s 
  Bar :: Float -> Thing 'A
  Baz :: Int -> Thing 'B
  Bah :: Char -> Thing 'C

一些测试：

processThingA :: Thing 'A -> String
processThingA (Foo x) = x
processThingA (Bar x) = show x

processThingB :: Thing 'B -> Int
processThingB (Foo _) = 0
processThingB (Baz i) = i

一个主要的缺点是我们需要让穷举检查器相信我们的模式匹配是正确的。

-- This unfortunately will give a spurious warning
processThingC :: Thing 'C -> Float
processThingC (Bah _) = 42.2
-- To silence the warning we need to prove that this is indeed impossible
processThingC (Foo _) = case aorb :: AorB 'C of {}

processThingAorB :: forall s. IsAorB s => Thing s -> String
processThingAorB (Foo x) = x
processThingAorB (Bar x) = "Bar " ++ show x
processThingAorB (Baz x) = "Baz " ++ show x
-- Again, to silence the warnings
processThingAorB (Bah _) = case aorb :: AorB 'C of {}

test :: ()
test = ()
  where
  _ = processThingA $ Foo "Hello"
  _ = processThingB $ Foo "World"
  _ = processThingA $ Bar 3.14
  _ = processThingB $ Baz 42
  _ = processThingC $ Bah '\n'

这项技术的扩展性不是很好。我们需要自定义 GADT 和类型 class 用于 Thing 的任何构造函数，它可以在某些 "union" 中生成任何标记。这样还是可以的。为了检查详尽性，我们需要利用所有这些 classes.

我认为这应该需要线性数量的样板文件，但它仍然很重要。

也许使用单例更简单，在一般情况下，将 s 的值存储在构造函数 Foo 中，并避免所有自定义 GADT 和类型 classes。

GADT 类型变量中的 Union

Union in GADT type variable

haskell

gadt