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

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中,我有时会使用以下方法来解决问题:

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

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