CODEWITHSUNDEEP
agda
Helmut Grohne
Helmut Grohne

Reputation: 6788

Functor laws in Agda

Traditionally functors in Haskell are supposed to support identity and composition laws. In Agda these laws should be formalized, but the standard library only ships RawFunctors yet (i.e. an fmap without laws). In the process of formalizing functors a few questions arise:

Should functors support congruence in general?

  1. Yes: On arbitrary Setoids or just Relation.Binary.PropositionalEquality.setoid?
  2. Yes: Should a functor take or provide a Function.Equality.Π?
  3. No: Which identity function should the identity law support? All of them (i.e. (id′ : A → A) → id′ ≗ id)?
  4. No: How should a function ask for a functor that supports congruence?
  5. No: What (real world?) functors do not support congruence?

Upvotes: 1

Views: 631

Answers (1)

Helmut Grohne
Helmut Grohne

Reputation: 6788

Partial answer:

Functors on equivalence relations

If a mapping F : Setoid ℓ ℓ → Setoid ℓ ℓ is to be turned into a functor, then congruence does not follow from other laws. For instance, F could map an s with the trivial relation to Relation.Binary.PropositionalEquality.setoid (Carrier s) and set fmap = id. Then, congruence does not hold in general. So as soon as the first equivalence relation is something different from equality, congruence is not a consequence.

Functors on propositional equality

It seems that all congruence proofs have the same structure: induction on the syntax of the fmap function. Thus they fall in the same category as free theorems. Other than something similar to lightweight free theorems, there is no automatic way to obtain such a proof.

More answers welcome.

Upvotes: 2

Related Questions