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

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

这是一个例子.

以下是长度索引列表和依赖类型的复制函数.有关如何实现replicateVect的信息,请参见this other question.以下是使用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,遵循单身人士的惯例：

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类型：

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)？
>是否有任何功能只能用其中一个写入？
>是否有任何功能使用其中一个更容易编写？

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~>类型,与Ex的论证类型不同,s – >类型.特别地,差异在(~>)和( – >)种类之间.后者( – >)是熟悉的函数箭头,而前者(〜>)是单体中的那种去功能化符号.

什么是defunctionalization符号,为什么他们需要自己的类型？它们在Promoting Functions to Type Families in Haskell号文件的第4.3节中有解释,但我会尝试在这里给出一个精简版本.从本质上讲,我们希望能够编写类型系列,如：

type family Positive (n :: Nat) :: Type where
  Positive Z     = Void
  Positive (S _) = ()

并且能够使用Sigma Nat Positive类型.但这不起作用,因为你不能部分应用类似积极的类型系列.幸运的是,defunctionalization技巧让我们可以解决这个问题.使用以下定义：

data TyFun :: Type -> Type -> Type

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

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

我们可以为Positive定义一个defunctionalization符号,让我们可以部分应用它：

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字段可以避免这种情况.

现在我已经完成了冗长的解释,让我试着回答你的问题：

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

所以你在技术上不需要(〜>)这样做.

另外,我不知道为Ex编写projSigma1等价物的方法,因为它没有存储足够的信息以便能够编写它.

另一方面,Sigma s t要求有一个Sing实例,所以如果没有,那么Sigma可能不会起作用.

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

当您迫切需要使用具有(〜>)种类的东西时,您将更容易使用Sigma,因为这是它闪耀的地方.如果你的类型只能使用( – >)类型,那么使用像Ex这样的“典型”存在类型可能会更方便,因为否则你必须以TyCon的形式引入噪声来提升某种类型的s – >输入到s~>类型.

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