4

我正在尝试定义 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呢？

4

1 回答 1

4

只有当我明确给出隐式参数时它才有效：

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 在这个问题上指出了为什么。原因是没有限制mor a b并且mor b c实际上是相同的类型。例如，mor可以是一个常数函数。在这种情况下，类型检查器无法推断a并且b只能 from mor a b，这会导致错误消息。

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

于 2015-05-10T12:16:12.810 回答