[Agda] Raw algebraic structures in the standard library

[Jacques Carette]

On 2019-08-04 4:08 a.m., Matthew Daggitt wrote:

> Dear all,
>  This is a question for anyone who uses the raw algebraic structures 
> from the standard library. Currently `RawMagma`, `RawMonoid`, 
> `RawRing` etc. contain no axioms whatsoever. We're not entirely 
> convinced this is the right approach as without proofs that _≈_ is an 
> equivalence, and that _∙_ is congruent with respect to it then it is 
> impossible to do any reasoning at all about them. In order to make 
> them more useful we're considering changing their definitions so that 
> they include the equality axioms above.
>
> Basically the question is does anyone have a use case for the raw 
> structures in which the equality axioms would be problematic to provide?


My understanding (which is perhaps wrong) is that the whole point of the 
Raw* structures is to do Haskell-like computations, where one is visibly 
not carrying around any extra proof baggage, 'by construction'. These 
computations work in a 'trust me' environment.

Ideally one would work with Magma, Monoid, Ring, etc, but without 
knowing for sure that all proofs will be considered irrelevant [so that 
they don't interfere with computation time], it's tempting to just 
hand-erase all those pesky proofs, just to be sure.

In other words, you're not supposed to reason with the Raw* structures. 
You just compute with them. And if the answer is wrong, well, you get 
what you deserve, as you skipped the proofs. [If you get a wrong answer 
from a computation that was induced from building a RawMonoid from a 
Monoid, and some kind of proper 'function' similarly obtained by a 
forgetful morphism, *that* would be a serious bug].

Jacques

PS: I consider the human-written Raw* structures to be a hack for 
efficiency [possibly strongly needed]; to me, these should be produced 
by an 'erase' meta-program applied to structures and morphisms. 
Eventually, even that ought to disappear, when some meta-theorem can be 
"proved" that this is not even necessary. That may not be soon.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190805/e3fdade6/attachment.html>