Copatterns and left-programming

[wenkokke]

Currently, PLFA uses lots of records to encapsulate definitions of, e.g., isomorphisms, embeddings, etc. This means lots of programming that looks like:

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

This is a bad style of programming in Agda, known as right programming – or, putting loads of function abstraction and pattern matching logic on the right-hand side of an equality symbol.

In order to shy students away from right programming, and towards left programming, I would like to rewrite the book to use copatterns wherever possible.

[sebeaumont]

FWIW I let Agda case split a few proofs in Connectives and it simplified at least two of them so as not to need funext and in this case the eta identity for product also. I think some explanation on this would be important, as to why left is better than right, which I guess is down to Adga's amazing pattern matching/elimination? Here's an example that Agda wrote for me ;-) BTW as s self studier I am learning so much from this fantastic book so thanks for all the work in making it!

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× ._≃_.to f = ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩
→-distrib-× ._≃_.from ⟨ g , h ⟩ = λ x → ⟨ g x , h x ⟩
→-distrib-× ._≃_.from∘to f = refl
→-distrib-× ._≃_.to∘from ⟨ g , h ⟩ = refl

[wenkokke]

@sebeaumont The view from the left by Conor McBride and James McKinna might be a great starting point:

http://strictlypositive.org/view.ps.gz

[sebeaumont]

@wenkokke Thanks for the reference. 👍