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

我不知道为什么（并且很想知道！）但是如果您在VerifiedCategory 中明确指定id 和comp 的所有隐式参数，它就会起作用。弄清楚它是非常丑陋和乏味的，但是这种类型检查：

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
-- ...

即通过在where 之前添加| hom。

除此之外，您必须做的一件事是限定id 在VerifiedCategory 中的使用，否则无论出于何种原因，它都会被解释为隐式参数：

  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 线程，该线程可能会在未来有所启发。