GADT 类型变量中的联合

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 这样的类型和一个像Thing B 这样的类型。如前所述，可以使用Foo 的某些上下文需要Thing A，而有些则需要Thing B，因此为了满足类型系统，每个上下文都需要存在一个构造函数。

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

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

（fooAsThingB 也是如此）

但这很丑陋，因为它需要我必须传播的Maybe，因为并非所有Thing Bs 都可以变成Thing As（实际上，只有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 在第一个 sn-p 中，是否可以将 AFoo 和 BFoo 合并到一个类型为 Thing A 和 Thing B 的 Foo 中？

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

Answer 1

一个可能的解决方案如下，即使我认为它不优雅。

我们首先定义一个 GADT 和一个类型类作为“A 或 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

然后我们在我们的类型中利用我们的类型类。这将导致Foo 需要更多空间，因为它需要在运行时存储类型类字典。这是少量的开销，但仍然很不幸。另一方面，这也可以在运行时辨别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'

这种技术不能很好地扩展。对于Thing 的任何构造函数，我们需要一个自定义的 GADT 和类型类，它们可以在某个“联合”中生成任何标记。这仍然可以。为了检查详尽无遗，我们需要利用所有这些类。

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

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