<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>On 2019-08-04 4:08 a.m., Matthew Daggitt wrote:<br>
</p>
<blockquote type="cite"
cite="mid:CAH9g8GnFNwJafUroYK2Hz5J+BEwbjjBkeGjJceFk4-AoBPcLbQ@mail.gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<div dir="ltr">Dear all,<br>
<div> 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 <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_≈_ </span>is
an equivalence, and that <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_∙_</span> 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. </div>
<div><br>
</div>
<div>Basically the question is does anyone have a use case for
the raw structures in which the equality axioms would be
problematic to provide?</div>
</div>
</blockquote>
<p><br>
</p>
<p>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. <br>
</p>
<p>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.</p>
<p>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].</p>
<p>Jacques</p>
<p>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.<br>
</p>
</body>
</html>