在Idris中定義類別

Question

我在嘗試定義Idris類型內部的已驗證類別，但我的方法沒有鍵入檢查。

class Cat ob (mor : ob -> ob -> Type) where 
    comp : {a : ob} -> {b : ob} -> {c : ob} -> mor a b -> mor b c -> mor a c 
    unit : (a : ob) -> mor a a 
    l  : {a,b : ob} -> {f : mor a b} -> (comp (unit a) f) = f 

ob是對象的類型，mor a b是態射的從a到b類型。 還有合適的單位和相關法律，但我的定義l不起作用。它說：

When elaborating type of constructor of Main.Cat: 
When elaborating an application of comp: 
     Can't unify 
       mor a13 b14 (Type of f) 
     with 
       mor b14 c (Expected type) 

我覺得很困惑。 unit a有類型mor a a,f有類型mor a b，爲什麼comp (unit a) f類型mor a b以及？

class Cat ob (mor : ob -> ob -> Type) where 
    comp : {a : ob} -> {b : ob} -> {c : ob} -> mor a b -> mor b c -> mor a c 
    unit : (a : ob) -> mor a a 
    l  : {a,b : ob} -> {f : mor a b} -> (comp {a=a} {b=a} {c=b} (unit a) f) = f 

埃德溫·布雷迪在this issue，爲什麼指出：

Answer 1

如果我明確給出了隱含參數，它纔會起作用。原因是mor a b和mor b c是實際上相同的類型沒有限制。例如，mor可能是一個常量函數。在這種情況下，類型檢查器無法從mor a b推斷出a和b，這會導致出現錯誤消息。

如果一個人有這樣的mor是一個射功能（如將可能是類參數在將來做）的限制，有可能推斷a和b，不再需要隱含提供的參數。