Idris中的多参数子类

Question

受到这篇博文和这段代码的启发,我想我会在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

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

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为确定参数，即足以找到实现的类型类的参数。这必须发生在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即在 之前放置 a where。

除此之外，您还必须做的一件事是限定idin的使用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

另请参阅这个reddit 线程，它可能在未来有所启发。