Порядок аргументов типа в индексированных векторах

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 порядок параметров не имеет значения, поэтому использование заказа, который хорошо работает с каррированием, является хорошей идеей.

В 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 

Но я не уверен, что дополнительная нагрузка на читателях коды стоит.