IdrisがData.Vectの引数をsizeとitem-typeの順に並べるのはなぜですか？

Question

タイトルのとおりです。私がよく知っている他の依存システム（AgdaとCoq）では、ベクトルタイプはVect : Type -> Nat -> Typeと定義されています。インデックスの前にパラメータを置くことは意味があり、どんな場合でもベクトル型の標準と思われます。 IdrisはなぜVect : Nat -> Type -> Typeを使用しますか？

Answer 1

Idrisでは、パラメータとインデックスの間には、目に見える違いはありません。型パラメータを持つことは、Functor (Vect n)インスタンスにとって便利です。