[Agda] Raw algebraic structures in the standard library

[Matthew Daggitt]

>
> I think I included the raw structures to make it possible to use
> structures that do not support all the laws, or to avoid having to prove
> all the laws. For instance, I don't think it is possible (ignoring bugs)
> to prove the monad laws for the TC monad (with propositional equality as
> the equality relation).
>

Thanks for the example! Of course, it would so happen that with
propositional equality then anything would trivially still fulfil the
proposed new definition of the `Raw` structures. Nonetheless I think I'm
convinced that maybe we need a separate set of structures rather than
simply changing the existing ones. Thanks all for the input.

On Sat, Aug 17, 2019 at 6:08 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 05/08/2019 17.38, Jacques Carette wrote:
> > 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.
>
> Typically one computes with the carrier type, not the full structure.
>
> I think I included the raw structures to make it possible to use
> structures that do not support all the laws, or to avoid having to prove
> all the laws. For instance, I don't think it is possible (ignoring bugs)
> to prove the monad laws for the TC monad (with propositional equality as
> the equality relation).
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190820/4ea2e821/attachment.html>