爲什麼Idris將Data.Vect的參數排序爲size然後是item-type？正如標題所說，

。在我熟悉的其他依賴系統（Agda和Coq）中，矢量類型定義爲Vect : Type -> Nat -> Type。把參數放在索引之前對我來說是有意義的，無論如何，它似乎是向量類型的標準。爲什麼伊德里斯使用Vect : Nat -> Type -> Type？爲什麼Idris將Data.Vect的參數排序爲size然後是item-type？正如標題所說，

來源

2017-05-11 Zyzzyva

參數和指數之間的Idris沒有可觀察到的差異。具有類型參數最後一個對於Functor (Vect n)實例很方便。

來源

2017-05-11 14:11:02

對於接口實例！哈！是的，這現在很合理。謝謝！ – Zyzzyva

前段時間，Idris使用了'Vect：Type - > Nat - > Type'，但它在[commit]（https://github.com/idris-lang/Idris-dev/commit/61d39dabbf63237671a9661064e6b0478add62e4）以下提交消息：「Swap Vect參數因此，現在更好編寫Functor，Applicative等的類型類實例。 –

爲什麼Idris將Data.Vect的參數排序爲size然後是item-type？正如標題所說，

回答

相關問題