索引向量中类型参数的顺序 [英] Order of type arguments in indexed vectors

问题描述

在传统的依赖类型编程中，定义

 数据Vec :: Type  - > Nat  - >键入其中
无:: Vec a'Z 
缺点:: a  - > Vec a n  - > Vec a（'s n）
  

然而，在Haskell中， Functor ， Applicative ，可折叠，可穿透， Eq1 ， Ord1 等等，类似于将参数翻转为 Vec :: Nat - >类型 - >键入。

常规约定有一些重要原因吗？或者仅仅是人们碰巧使用的不是基于类型类的语言？

解决方案

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

 数据Vec（A：Set）：Nat  - >在Agda中设置... 
  

，因为我们希望 Set 参数作为参数处理。如果我们交换参数顺序并写入



 数据Vec：Nat  - >设置 - >设置... 
  

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

在Haskell中，参数顺序无关紧要，所以使用一个适合柯里化的订单是一个好主意。

在Agda中，我有时使用以下解决方法来获取curry right：

  data Vec'（A：Set）：Nat  - >设置
 
 Vec：Nat  - >设置 - >设置
 Vec n A = Vec'A n 
 
 { - ＃DISPLAY Vec'A n = Vec n A＃ - } 
 
 data Vec'A where 
零：Vec零A 
缺点：{n：Nat}  - > A  - > Vec n A  - > Vec（succ n）A 
  

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

It seems conventional in dependently-typed programming to define

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

In Haskell, however, the Functor, Applicative, Foldable, Traversable, Eq1, Ord1, etc., classes seem to make a good case for flipping the arguments around, to Vec :: Nat -> Type -> Type.

Is there some important reason for the usual convention? Or is it just what people happen to use in languages not based substantially on type classes?

解决方案

I think this is not just conventional, but related to parameters vs. indexes in some dependently-typed languages. For example, Agda and Coq both require that parameters come before indexes in data type definitions. We would write

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

in Agda, because we want the Set argument to be treated as a parameter. If we would swap the argument order and write

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

instead, the Set argument would be treated as an index. We would still use it as a parameter in the constructor signatures, of course, but the Agda type checker would miss the information that it is a parameter.

In Haskell, the parameter order doesn't matter, so using an order that works well with currying is a good idea.

In Agda, I sometimes use the following work-around to get the currying right:

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

But I'm not sure the extra burden on the readers of the code is worth it.

这篇关于索引向量中类型参数的顺序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！