GADT 的类似 newtype 的操作语义，其中类型完全确定构造函数

Question

假设我有一个如下所示的 GADT：

data Tag = A | B | C

data Payload (tag :: Tag) where
  PA :: Int -> Payload A
  PB :: Double -> Payload B
  PC :: Bool -> Payload C

我想要Payload自己没有运行时表示——即我想要Coercible Int (Payload A)，我想要零成本模式匹配，并且通常我希望它表现得好像我有以下三个 newtype 定义：

newtype PayloadA = PA Int
newtype PayloadB = PB Double
newtype PayloadC = PC Bool

有没有办法说服 GHC 给我那个？

Answer 1

这看起来不可能实现，至少在当前的 GHC 中是这样。假设你Payload A有相同的表示Int，等等。

data Tag = A | B | C

data Payload (tag :: Tag) where
  PA :: Int -> Payload A
  PB :: Double -> Payload B
  PC :: Bool -> Payload C

那么，我们应该如何实现呢？

foo :: Payload tag -> Int
foo (PA i) = i
foo (PB _) = 1
foo (PC _) = 2

为了实现foo，我们需要以某种方式tag从 中提取Payload tag，但如果Payload tag不将标记存储在其表示中，那这是不可能的。

相反，我们可以做的是将运行时标记表示与其有效负载数据分开。

type family Payload (tag :: Tag) where
   Payload 'A = Int
   Payload 'B = Double
   Payload 'C = Bool

现在，Payload 'A正是一个Int. 然而，我们失去了 write 的能力foo，因为标签在运行时不再沿着有效负载存储。我们可以这样写：

-- singleton, could be auto-generated using the singletons library
data STag (tag :: Tag) where
    SA :: STag 'A
    SB :: STag 'B
    SC :: STag 'C

bar :: STag tag -> Payload tag -> Int
bar PA i = i
bar PB _ = 1
bar PC _ = 2

请注意我们实际上是如何将标记添加为参数的，因为我们确实需要在运行时将其表示出来。

Answer 2

你可以这样做：

data family Payload (tag :: Tag)
newtype instance Payload A = PA Int
newtype instance Payload B = PB Double
newtype instance Payload C = PC Bool

这满足了实际具有不同于Int, Double, 的类型Bool以及具有 newtype 的操作语义的要求。当然，您付出的代价是您将无法通过模式匹配来确定哪个是哪个。但是您可以使用类型类或通过显式传递标签来恢复这些东西（这在幕后基本上是相同的）；例如：

class Foo (t :: Tag) where foo :: Payload t -> Int
instance Foo A where foo (PA i) = i
instance Foo B where foo (PB _) = 2
instance Foo C where foo (PC _) = 3