Haskell 中何时使用存在类型与依赖对？

Question

什么时候需要使用专门的存在类型与依赖对（也称为依赖和或西格玛类型）？

这是一个例子。

以下是长度索引列表和依赖类型的复制函数。参见 for how to implement replicateVect. The following is using the singletons 图书馆：

data Vect :: Type -> Nat -> Type where
  VNil :: Vect a 0
  VCons :: a -> Vect a n -> Vect a (n + 1)

replicateVect :: forall n a. SNat n -> a -> Vect a n

有（至少）两种可能的方法来创建采用正常 Natural, instead of a singleton SNat.

的复制函数

一种方法是为 Vect 创建一个专门的存在类型。我称其为 SomeVect，遵循 singletons:

的约定

data SomeVect :: Type -> Type where
  SomeVect :: forall a n. Vect a n -> SomeVect a

replicateExistentialVect :: forall a. Natural -> a -> SomeVect a
replicateExistentialVect nat a =
  case toSing nat of
    SomeSing sNat -> SomeVect $ replicateVect sNat a

另一种方法是使用依赖对。这使用来自 singletons:

的 Sigma 类型

replicateSigmaVect :: forall n a. Natural -> a -> Sigma Nat (TyCon (Vect a))
replicateSigmaVect nat a =
  case toSing nat of
    SomeSing sNat -> sNat :&: replicateVect sNat a

这些函数看起来非常相似。使用 replicateExistentialVect 和 replicteSigmaVect 也很相似：

testReplicateExistentialVect :: IO ()
testReplicateExistentialVect =
  case replicateExistentialVect 3 "hello" of
    SomeVect vect -> print vect

testReplicateSigmaVect :: IO ()
testReplicateSigmaVect =
  case replicateSigmaVect 3 "hello" of
    _ :&: vect -> print vect

可以找到完整代码here。

这引出了我的问题。

我什么时候应该使用专门的存在类型（如 SomeVect）与依赖对（如 Sigma）？
有没有函数可以只能用一个或另一个来写？
是否有使用其中一种或另一种更容易编写的函数？

Answer 1

When should I use a specialized existential type (like SomeVect) vs. a dependent pair (like Sigma)?

这个问题有点难回答，因为：

Sigma本身就是一种特殊的存在类型。
有无数种方法可以创建专门的存在类型——SomeVect 和 Sigma 只是这种现象的两个例子。

尽管如此，确实感觉 Sigma 与 GHC 中存在类型的其他编码方式有微妙的不同。让我们试着找出究竟是什么让它与众不同。

首先，让我们写出 Sigma 的定义：

    data Sigma (s :: Type) :: (s ~> Type) -> Type where
      (:&:) :: forall s (t :: s ~> Type) (x :: s).
               Sing x -> Apply t x -> Sigma s t

为了比较，我还将定义一个 "typical" 存在类型：

    data Ex :: (s -> Type) -> Type where
      MkEx :: forall s (t :: s -> Type) (x :: s).
              t x -> Ex t

让我们回顾一下两者之间的区别：

Sigma s t 有两个类型参数，而 Ex t 只有一个。这并不是一个非常显着的差异，事实上，您可以只使用一个参数来编写 Sigma：
```
data Sigma :: (s ~> Type) -> Type where
  (:&:) :: forall s (t :: s ~> Type) (x :: s).
           Sing x -> Apply t x -> Sigma t
```
或 Ex 使用两个参数：
```
data Ex (s :: Type) :: (s -> Type) -> Type where
  MkEx :: forall s (t :: s -> Type) (x :: s).
          t x -> Ex s t
```
我选择在 Sigma 中使用两个参数的唯一原因是为了更接近地匹配其他语言中依赖对的表示，例如 Idris's DPair。它也可能使 Sigma s t 和 ∃ (x ∈ s). t(x) 之间的类比更清楚。
更重要的是，Sigma 的最后一个参数 s ~> Type 不同于 Ex 的参数 s -> Type。特别是 (~>) 和 (->) 类型之间的区别。后者，(->)就是我们熟悉的函数箭头，而前者(~>)，就是singletons.
中那种去函数化符号
什么是去功能化符号，为什么它们需要自己的种类？它们在论文 Promoting Functions to Type Families in Haskell 的第 4.3 节中进行了解释，但我将在此处尝试提供一个浓缩版本。本质上，我们希望能够编写如下类型族：
```
type family Positive (n :: Nat) :: Type where
  Positive Z     = Void
  Positive (S _) = ()
```
并且能够使用类型Sigma Nat Positive。但这行不通，因为您不能部分应用像 Positive 这样的类型族。幸运的是，去功能化技巧让我们可以解决这个问题。使用以下定义：
```
data TyFun :: Type -> Type -> Type

type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
```
我们可以为 Positive 定义一个 去功能化符号 让我们部分地应用它：
```
data PositiveSym0 :: Nat ~> Type
type instance Apply PositiveSym0 n = Positive n
```
现在，在 Sigma Nat PositiveSym0 类型中，第二个字段的类型是 Apply PositiveSym0 x，或者只是 Positive x。因此，(~>) 在某种意义上比 (->) 更通用，因为它让我们可以使用 比 (->) 更多的 类型。

(如果有帮助，可以把(~>)看成是无法匹配的那种函数，如Richard Eisenberg's thesis第4.2.4节所述，而 (->) 是一种 可匹配的 函数。）
虽然 MkEx 构造函数只有一个字段，但 (:&:) 构造函数有一个附加字段（Sing x 类型）。有两个原因。一是根据定义，存储这个额外字段是使 Sigma 成为依赖对的部分原因，这使我们能够通过 projSigma1 函数检索它。另一个原因是，如果你把Sing x字段去掉：
```
data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s (t :: s ~> Type) (x :: s).
           Apply t x -> Sigma s t
```
那么这个定义需要 AllowAmbiguousTypes，因为 x 类型变量不明确。这可能很繁琐，所以有一个明确的 Sing x 字段可以避免这种情况。

既然我已经完成了冗长的解释，让我尝试实际回答您的问题：

When should I use a specialized existential type (like SomeVect) vs. a dependent pair (like Sigma)?

我认为这最终是个人品味的问题。 Sigma 很好，因为它非常通用，但您可能会发现定义专门的存在类型会使您的代码更易于理解。（但也请参阅下面的注意事项。）

Are there any functions that can only be written with one or the other?

我想我之前的 Sigma Nat PositiveSym0 示例将算作您不能用 Ex 做的事情，因为它需要利用 (~>) 类型。另一方面，您也可以定义：

data SomePositiveNat :: Type where
  SPN :: Sing (n :: Nat) -> Positive n -> SomePositiveNat

所以您在技术上不需要 (~>) 来执行此操作。

另外，我不知道有什么方法可以为 Ex 写一个 projSigma1 等价物，因为它没有存储足够的信息来写这个。

另一方面，Sigma s t 要求类型 s 有一个 Sing 实例，所以如果没有，Sigma 可能是不会工作。

Are there any functions that are significantly easier to write with one or the other?

当您迫切需要使用 (~>) 类型的东西时，使用 Sigma 会更轻松，因为那是它的闪光点。如果你的类型可以只使用 (->) 种类，那么使用像 Ex 这样的 "typical" 存在类型可能会更方便，否则你必须以 TyCon 举起类似 s -> Type 的东西到 s ~> Type。

此外，如果能够方便地检索 Sing x 类型的字段很重要，您可能会发现 Sigma 更容易使用。

Haskell 中何时使用存在类型与依赖对？

When to use existential type vs. dependent pair in Haskell?

haskell

singleton

dependent-type

existential-type

type-level-computation