haskell - 索引向量中类型参数的顺序

Question

在依赖类型编程中定义

data Vec :: Type -> Nat -> Type where
  Nil :: Vec a 'Z
  Cons :: a -> Vec a n -> Vec a ('S n)

然而，在 Haskell 中， Functor , Applicative , Foldable , Traversable , Eq1 , Ord1等等，类似乎是一个很好的例子，可以将论点翻转到 Vec :: Nat -> Type -> Type。 .

通常的约定有什么重要的原因吗？或者它只是人们碰巧在基本上不基于类型类的语言中使用的东西？

Answer 1

我认为这不仅是传统的，而且与某些依赖类型语言中的参数与索引有关。例如，Agda 和 Coq 都要求参数在数据类型定义中位于索引之前。我们会写

data Vec (A : Set) : Nat -> Set where ...

在 Agda，因为我们想要 Set参数被视为参数。如果我们交换参数顺序并写

data Vec : Nat -> Set -> Set where ...

相反， Set参数将被视为索引。当然，我们仍然会将它用作构造函数签名中的参数，但是 Agda 类型检查器会错过它是参数的信息。

在 Haskell 中，参数顺序无关紧要，因此使用与柯里化(Currying)配合得很好的顺序是个好主意。

在 Agda 中，我有时会使用以下解决方法来获得正确的柯里化(Currying):

data Vec' (A : Set) : Nat -> Set

Vec : Nat -> Set -> Set
Vec n A = Vec' A n

{-# DISPLAY Vec' A n = Vec n A #-}

data Vec' A where
  nil : Vec zero A
  cons : {n : Nat} -> A -> Vec n A -> Vec (succ n) A

但我不确定代码读者的额外负担是否值得。