Facts about refactoring

Stream: lean4

[Pieter Collins]

What is known about typeclass refactoring in Lean?

My impression is that refactoring can be done so that users (but not makers) of a typeclass are unaffected as long as the typeclass has the same fields and implements the same preexisting superclasses. Is this a known fact about the system, or known cases where it does not hold?

However, it seems that refactoring changes typeclass constructors .mk, and that this means refactoring will break code that makes a refactored class. Is this the case? Are there any workarounds (like providing custom constructors)?

It looks like if class C (α) extends A α, one can add a new typeclass class B (α) extends A α and instance B_of_C {α} : C α → B α works to inject a class between two others; does this do the trick?

Without non-breaking refactoring / additions, I would be concerned about the library becoming brittle (ossification), with early decisions being locked-in; is this happening in practice?

[Pieter Collins]

Haskell typeclass refactoring is breaking, which makes any refactoring of the standard library problematic. Around 2014 they were refactoring their Functor hierarchy to make Applicative a superclass of Monad. However, since users must explicitly declare instances of all superclasses, this meant a breaking change for all Monad users, and it was a big effort to phase the changes so that users could adapt code gradually; maybe they even had to change the compilers. See https://wiki.haskell.org/Functor-Applicative-Monad_Proposal for details. There were proposals for default superclass instances http://repetae.net/recent/out/classalias.html, with an implementation in the Strathclyde Haskell Enhancement preprocessor https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/superclass.html.

[Jovan Gerbscheid]

What is your question exactly?

In the particular case of Applicative and Monad, the current design in Lean has Monad extend Applicative, but users can still declare Monad instances in a way that doesn't mention Applicative. So Lean is a lot more convenient than Haskell in that regard.

[Anne Baanen]

I understand your specific question as: can we turn a class C extends A into class C extends B without breaking all instance : C where ... declarations? And the answer is yes (and the same holds for structure declarations in general), as long as the non-implicit non-autoparam fields remain the same.

For implicit fields: instance synthesis and unification can be used to fill in the fields, and in particular instances often fill in the new fields in such an extends-based refactor.

A good example of adding fields using autoparams is exponentiation in docs#Monoid. In the source code we can see the fields are defined to have default values, but they can be overridden explicitly in specific instances, either for defeq or for optimizing the implementation.

[Johan Commelin]

https://arxiv.org/abs/2202.05360 "Formalized functional analysis with semilinear maps" is a good example of a highly nontrivial factor that was performed "in flight" without disrupting the ecosystem significantly.