Note on 2021-02-08
- how do you implement typeclasses?
- first, let’s see what Agda and Lean docs says
- one thing really really bugs me is why Agda requires the type of the instance argument be of a certain shape
{Γ} → C(args), but Lean doesn’t seems require this
- another thing is how Agda’s stdlib and Lean’s stdlib differs in type signatures for function e.g.
List.filter in Agda the property is implicit arg, and the decision procedure is explicit arg, in Lean the property is explicit arg, and the decision procedure is instance arg. I like how lean does it
- Canonical Structures in Coq is packed records
-