I’m dumb

Okay maybe I’m not dumb, but I do suffer from a problem. I tend to implement the first solution to a problem that I think of instead of trying to think of a better solution. For instance, consider the problem of coming up with a structure to implement a category as a type. The first thought I had was that a category was a pair of Objects and Morphisms where Morphisms have a domain and range, etc. So I would implement it as follows in Coq:

Record Category : Type := category {
  Object : Type
  Morphism : Type
  Domain : Morphism -> Object
  Range : Morphism -> Object
  Id : Object -> Morphism
  Compose : (f:Morphism)(g:Morphism)->(Range g)=(Domain f)->Morphism
  rangeId : (a:Object)(Range (Id a))=a
  domainId : (a:Object)(Domain (Id a))=a
  …
}

Much more is omitted. However a much better approach which is more along the lines of the definition given, and similar to how they have been implemented in Coq, is to make Morphism a function from two objects to a type.

Record Category : Type := category {
  Object : Type
  Morphism : Object -> Object -> Type
  Id : (A:Object)(Morphism A A)
  Compose : (A,B,C:Object)(Morphism B C) -> (Morphism A B) -> (Morphism A C)
  idLeft : (A,B:Object)(f:(Morphism A B))(Compose (Id B) f)=f
  idRight : (A,B:Object)(f:(Morphism A B))(Compose f (Id A))=f
  assoc : (A,B,C,D:Object)(f:(Morphism A B))(g:(Morphism B C))(h:(Morphism C D))
        (Compose h (Compose g f))=(Compose (Compose h g) f)
}

This definition is shorter, cleaner, and for whatever reason, not the first thing I thought of. In this case I probably wouldn’t have gotten very far without correcting myself, but in other cases I can go pretty far before deciding there are better ways of doing things.

Perhaps I should always wait some time before I implement a solution to a problem. I’m not sure that I’d be creative enough after finding a solution to find a better solution. I consider this a big problem.