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

Question

什么时候需要使用专门的存在类型与依赖对(也称为依赖和或 sigma 类型)？

这是一个例子。

以下是长度索引列表和依赖类型的复制函数。见 this other question如何实现 replicateVect .以下是使用 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 的复制函数。 , 而不是单例 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

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

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

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

为了比较，我还将定义一个“典型”的存在类型:

    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 field :

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场避免了这一点。

说完我冗长的解释，让我尝试实际回答您的问题:

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

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

2. 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

所以你在技术上不需要 (~>)去做这个。

另外，我不知道写一个 projSigma1 的方法。等效于 Ex ，因为它没有存储足够的信息来编写这个。

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

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

您可以更轻松地使用 Sigma当您迫切需要使用带有 (~>) 的东西时善良，因为那是它闪耀的地方。如果您的类型可以逃脱 (->)类，使用“典型”的存在类型可能更方便，例如 Ex , 因为否则你必须以 TyCon 的形式引入噪声举起某种东西 s -> Type至 s ~> Type .

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