[Agda] Raw algebraic structures in the standard library

[Matthew Daggitt]

Thanks Jacques, that's a great explanation of their function and explains a
lot. I have to confess I haven't seen any programs that do such "raw"
computation, but I can see why they would be useful. Hmm maybe the
algebraic structures with just equality axioms need to be added as another
level of between the two existing levels. Maybe "raw", "medium" and
"well-done" is the way to go :)

Sergei, yes if we made the previously proposed change then RawMagma would
be equivalent to Magma but the rest of the hierarchy would diverge.
RawMagma would not be equivalent to Semigroup as it would lack
associativity, likewise RawMonoid would not be equivalent to Monoid. I'm
afraid I don't understand your second question.

On Tue, Aug 6, 2019 at 12:58 AM <mechvel at scico.botik.ru> wrote:

> On 2019-08-04 11:08, 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?
> > Best,
> > Matthew
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
> If you require the axioms of equivalence or/and congruence for _≈_ and
> _∙_ for RawMagma,
> then it will turn out that RawMagma is same as Magma. And further, this
> approach leads to eliminating the Raw structures
> -- ?
>
> I thought that the Raw records are introduced to represent and consider
> the signatures as not provided with any properties besides those induced
> automatically by a non-dependent type signature
> (I never thought of this, is it true that they deal with non-dependent
> types?).
> For example,  foo : Carrier -> Nat  automatically postulates that foo
> returns a member of Nat and not of Bool, and the type checker checks
> this property, and dependent types are not needed for this.
>
> --
> SM
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190808/8cf27011/attachment.html>