何时在Haskell中使用存在类型与依赖对?
什么时候想要使用专门的存在类型与依赖对(也称为依赖和或西格玛类型)?
这是一个例子. 以下是长度索引列表和依赖类型的复制函数.有关如何实现replicateVect的信息,请参见this other question.以下是使用 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 有(至少)两种可能的方法来创建一个复制函数,它采用普通的 一种方法是为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 另一种方法是使用依赖对.这使用了来自单身的 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)? 解决方法
回答这个问题有点棘手,因为: > 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 什么是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节所述,而( – >)是可匹配函数的种类.) 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字段可以避免这种情况. 现在我已经完成了冗长的解释,让我试着回答你的问题:
我认为这最终是个人品味的问题. Sigma非常好,因为它非常简洁,但您可能会发现定义一个专门的存在类型会使您的代码更容易理解. (但也请看下面的警告.)
我想我早期的Sigma Nat PositiveSym0示例将被视为Ex无法做到的事情,因为它需要利用(?>)类型.另一方面,你也可以定义: data SomePositiveNat :: Type where SPN :: Sing (n :: Nat) -> Positive n -> SomePositiveNat 所以你在技术上不需要(?>)这样做. 另外,我不知道为Ex编写projSigma1等价物的方法,因为它没有存储足够的信息以便能够编写它. 另一方面,Sigma s t要求有一个Sing实例,所以如果没有,那么Sigma可能不会起作用.
当您迫切需要使用具有(?>)种类的东西时,您将更容易使用Sigma,因为这是它闪耀的地方.如果你的类型只能使用( – >)类型,那么使用像Ex这样的“典型”存在类型可能会更方便,因为否则你必须以 此外,如果能够方便地检索Sing x类型的字段,您可能会发现Sigma更容易使用. (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |