訂單的類型參數

看來傳統的依賴性類型編程來定義訂單的類型參數

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。

是否有一些常見約定的重要原因？還是僅僅是人們碰巧用於不基於類型類的語言？

來源

2016-09-28 dfeuer

對於它的價值，你不是第一個在這方面遇到的問題。 [這]（https://blog.jle.im/entry/fixed-length-vector-types-in-haskell-2015.html）文章（這使得你提到的大多數類的實例）也有'Vec：：Nat - > Type - > Type'。 – Alec

'Type - > Nat - > Type'只是數學（'³³'等等）和不識字的語言（'std :: array '）中常見的順序。 Currying是Haskell命令有用的原因。 – leftaroundabout

[This]（http://stackoverflow.com/a/40252235/3072788）如果'Nat'沒有出現在最後的位置，那麼帶'Bump'的技巧是不可能的。 – Alec

我認爲這不僅僅是傳統的，而是與某些依賴類型語言中的參數與索引相關。例如，Agda和Coq都要求參數在數據類型定義中的索引之前出現。我們會寫

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

在Agda，因爲我們希望Set參數被視爲一個參數。如果我們將交換參數順序寫

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

相反，Set參數將被視爲一個指標。當然，我們仍然將它用作構造函數簽名中的參數，但Agda類型檢查器會錯過它作爲參數的信息。

在Haskell中，參數順序無關緊要，因此使用一個適合柯里化的順序是一個好主意。

在阿格達，我有時會使用下面的變通，以獲得正確的討好：

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

但我不知道該代碼的讀者的額外負擔是值得的。

來源

2016-09-29 01:27:35 Toxaris

就是這樣，是的。令人煩惱的往往也是。在Haskell中，我把這個長度放在第一位......或者將它推廣到索引集上的funxtors。 – pigworker

你知道嗎？爲什麼Agda表現得如此？檢查每個參數是參數還是索引（如GHC所做的）是否太昂貴？ – dfeuer

@dfeuer我想GHC不必生成一個歸納類型的關聯歸納原理，但Agda必須。以上，可以選擇「A」作爲參數或索引，每個選項都會生成不同的歸納原理。我認爲，Agda沒有「正確」的選擇，所以最好讓用戶決定。 – chi

訂單的類型參數

回答

相關問題