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

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

完整的代码可以在这里找到.

---

这让我想到了我的问题.

1. 我应该何时使用专门的存在类型(如SomeVect)与依赖对(如Sigma)？
2. 是否有任何功能只能用一个或另一个写？
3. 是否有任何功能使用其中一个更容易编写？

Answer 1

1. 我应该何时使用专门的存在类型(如SomeVect)与依赖对(如Sigma)？

回答这个问题有点棘手,因为:

1. Sigma 它本身就是一种专门的存在类型.
2. 创建专门的存在类型的方法有很多种 - 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

让我们回顾一下两者之间的差异:

1. 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中DPair.它也许可以在两者之间进行类比Sigma s t和? (x ? s). t(x)更清晰.

2. 更重要的是,这种Sigma最后的论证,与论证s ~> Type的种类不同Ex,s -> Type.特别是,差异在于(~>)和(->)种类之间.后者(->)是熟悉的功能箭头,而前者(~>)则是中的功能化符号singletons.

   什么是defunctionalization符号,为什么他们需要自己的类型？它们在Haskell的"将函数添加到类型族 "一文的第4.3节中进行了解释,但我将尝试在此处给出一个精简版本.从本质上讲,我们希望能够编写类型系列,如:

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

   并且能够使用该类型Sigma Nat Positive.但这不起作用,因为你无法部分应用类似的类型系列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,让我们部分地应用它:

   data PositiveSym0 :: Nat ~> Type
   type instance Apply PositiveSym0 n = Positive n
   

   现在,在类型中Sigma Nat PositiveSym0,第二个字段是类型Apply PositiveSym0 x,或者只是Positive x.因此,(~>)在某种意义上说比一般更通用(->),因为它让我们使用更多的类型(->).

   (如果它有帮助,可以将其(~>)视为一种无法匹配的函数,如Richard Eisenberg的论文第4.2.4节所述,而(->)它是一种可匹配的函数.)

3. 虽然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. 我应该何时使用专门的存在类型(如SomeVect)与依赖对(如Sigma)？

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

2. 是否有任何功能只能用一个或另一个写？

我想我之前的Sigma Nat PositiveSym0例子将被视为你无法做到的事情Ex,因为它需要利用这种(~>)类型.另一方面,你也可以定义:

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

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

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

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

3. 是否有任何功能使用其中一个更容易编写？

Sigma当您迫切需要使用某种东西时,您将更容易使用(~>),因为这是它闪耀的地方.如果你的类型可以逃脱只是一个(->)样,它可能是使用一个"典型的"生存型像更方便Ex,因为否则你必须在形式引入的噪声TyCon解除样的东西s -> Type来s ~> Type.

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