Order of type arguments in indexed vectors

Question

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?

Answer 1

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.