CODEWITHSUNDEEP
dependent-typeidris
Turion
Turion

Reputation: 6146

Defining categories in Idris

I'm trying to define verified categories internal to Idris types, but my approach doesn't type check.

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 is the type of objects, mor a b is the type of morphisms from a to b. There are the right unit and associativity laws still to come, but already my definition for l doesn't work. It says:

 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)

I find that confusing. unit a has type mor a a, f has type mor a b, why doesn't comp (unit a) f have type mor a b as well?

Upvotes: 4

Views: 141

Answers (1)

Turion
Turion

Reputation: 6146

It only works if I explicitly give the implicit parameters:

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 points out in this issue, why. The reason is that there is no restriction on mor a b and mor b c being the actually same type. For example, mor could be a constant function. In that cases, the type checker can't infer a and b just from mor a b, which leads to the error message.

If one had the restriction that mor be an injective function (as will probably be done for class arguments in the future), it would be possible to infer a and b and no longer necessary to give the arguments implicitly.

Upvotes: 4

Related Questions