在 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？

Answer 1

只有在我明确给出隐式参数时它才有效:

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

Edwin Brady 在 this issue 中指出了原因。原因是没有限制 mor a b 和 mor b c 实际上是同一类型。例如，mor 可以是一个常量函数。在这种情况下，类型检查器无法仅从 mor a b 推断出 a 和 b，这会导致出现错误消息。

如果限制 mor 是单射函数（将来可能会对 class 参数进行限制），则可以推断出 a 和b 并且不再需要隐式给出参数。

在 Idris 中定义类别

Defining categories in Idris

dependent-type

idris