Idris中的多參數子類

Question

受this blog post和this code的啓發我以爲我會在Idris中使用它的接口（類型類）嘗試一些類別理論。

我定義Category如下，工作正常：

interface Category (obj : Type) (hom : obj -> obj -> Type) where 
    id : {a : obj} -> hom a a 
    comp : {a, b, c : obj} -> hom b c -> hom a b -> hom a c 

然後，在Verified模塊的精神，我想我會定義一個類驗證：

interface Category obj hom => 
      VerifiedCategory (obj : Type) (hom : obj -> obj -> Type) where 
    categoryAssociativity : {a, b, c, d : obj} -> 
          (f : hom c d) -> (g : hom b c) -> (h : hom a b) -> 
          (comp (comp f g) h = comp f (comp g h)) 
    categoryLeftIdentity : {a, b : obj} -> (f : hom a b) -> (comp id f = f) 
    categoryRightIdentity : {a, b : obj} -> (f : hom a b) -> (comp f id = f) 

不幸的是， Idris拒絕該代碼並顯示以下錯誤消息：

When checking type of constructor of CategoryTheory.VerifiedCategory: 
Can't find implementation for Category obj hom 

我做錯了什麼，或者我想用Idris做不到的多參數子類做些什麼？

所有這些代碼都在其自己的模塊中，名爲CategoryTheory，沒有任何導入。

我正在使用Idris v0.12。

Answer 1

我不知道爲什麼（並且很想知道！），但如果您明確指定了所有隱含參數到id和comp,VerifiedCategory，它就會有效。這是很醜陋和繁瑣弄清楚，但這typechecks：

interface Category obj hom => VerifiedCategory (obj : Type) (hom : obj -> obj -> Type) where 
    categoryAssociativity : {a, b, c, d : obj} -> 
          (f : hom c d) -> 
          (g : hom b c) -> 
          (h : hom a b) -> 
          (comp {a = a} {b = b} {c = d} (comp {a = b} {b = c} {c = d} f g) h = comp {a = a} {b = c} {c = d} f (comp {a = a} {b = b} {c = c} g h)) 
    categoryLeftIdentity : {a, b : obj} -> 
         (f : hom a b) -> 
         (comp {a = a} {b = b} {c = b} (id {a = b}) f = f) 
    categoryRightIdentity : {a, b : obj} -> 
          (f : hom a b) -> 
          (comp {a = a} {b = a} {c = b} f (id {a = a}) = f) 

編輯：我剛剛找到另一種方式是明確指定hom爲determining parameter，即類型類的參數足以找到一個實現。這在Category以及在VerifiedCategory發生（我不知道，爲什麼），像這樣：

interface Category (obj : Type) (hom : obj -> obj -> Type) | hom where 
-- ... 

interface Category obj hom => VerifiedCategory (obj : Type) (hom : obj -> obj -> Type) where 
-- ... 

即通過把一個| hom的where之前。你有除了做

一兩件事是有資格的VerifiedCategoryid使用，否則它將被解釋爲出於某種原因隱含參數：

categoryLeftIdentity : {a, b : obj} -> 
         (f : hom a b) -> 
         comp CategoryTheory.id f = f 
    categoryRightIdentity : {a, b : obj} -> 
          (f : hom a b) -> 
          comp f CategoryTheory.id = f 

參見this reddit的線程可能是照亮未來。