實施半羣在伊德里斯

Question

我試圖實現Semigroup接口，用於伊德里斯簡單依賴對，取決於對但這並不編譯：

Semigroup (n ** Vect n f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

與錯誤

Type mismatch between 
    ty 
and 
    Nat 

但是這樣編譯：

myPair:Type -> Type 
myPair f = (n ** Vect n f) 

Semigroup (myPair f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

爲什麼？什麼是完成這個最好的方法？

Answer 1

伊德里斯FAQ：

如果您在以小寫字母開頭，並沒有施加任何參數的類型使用的名稱，然後將伊德里斯把它作爲一個隱含的約束參數。

一種方法來解決這一問題將是擺脫一些語法糖，並明確綁定n這樣的：

Semigroup (DPair Nat (\n => Vect n f)) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

另一種方法是使用一個大寫字母爲向量長度：

Semigroup (N ** Vect N f) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

這裏，N沒有得到約束在Semigroup實施，這使得DPair語法糖正如我們在第一個變體中所做的一樣，踢入並綁定N。

至於myPair的例子，它編譯，因爲這個例子基本上等於上面的例子DPair。如果你剛剛取出糖，一切都變得清晰：

myPair:Type -> Type 
myPair f = DPair Nat (\n => Vect n f)