Commutative semiring of decidable types

[conal]

For a project I’m working on, I needed something like a commutative semiring of decidable types. I defined the following existential wrapper to get the homogeneity required by the algebraic structures and bundles:

record Decides : Set (suc ℓ) where
  constructor decides
  field
    {prop} : Set ℓ
    dec : Dec prop

It was fairly easy from there to define structures and bundles up through commutative semirings.

Is this functionality already in agda-stdlib? A quick search for “IsMonoid” didn’t turn up anything obvious.

If this functionality isn’t already in agda-stdlib and if it sounds appealing to others, I’d be happy to package it in a PR, welcoming suggestions for its improvement in the process.

Comments?

[MatthewDaggitt]

Hi Conal, (Typing on my phone so forgive the lack of unicode!) Assuming that I've understood what your trying to do correctly, I don't believe that functionality currently exists in the standard library. If it did then it would under 'Algebra.Construct'... If we were going to add it, I'd be tempted to generalise this to the lifting of any algebraic structure with operators that preserve a given predicate P (Dec in your case) to an algebraic structure over the dependant pair of the original element + the instance of P. Not only would that be more general but then we could then use the \Sigma type rather than defining Decides. You could of course define Decides in terms of the \Sigma and with a little bit of renaming recover most of the behaviour of your custom record type. Now that I think about it, that'd actually be useful in some of my own code! Cheers, Matthew

…

On Fri, 22 Jan 2021, 08:29 Conal Elliott, ***@***.***> wrote: For a project I’m working on, I needed something like a commutative semiring of decidable types. I defined the following existential wrapper to get the homogeneity required by the algebraic structures and bundles: record Decides : Set (suc ℓ) where constructor decides field {prop} : Set ℓ dec : Dec prop It was fairly easy from there to define structures and bundles up through commutative semirings. Is this functionality already in agda-stdlib? A quick search for “IsMonoid” didn’t turn up anything obvious. If this functionality isn’t already in agda-stdlib and if it sounds appealing to others, I’d be happy to package it for a PR, welcoming suggestions for its improvement in the process. Comments? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1404>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAP26EVDSZ3IEB7E44HDPJLS3DBEZANCNFSM4WNW2GGQ> .

[conal]

Thanks for the reply, Matthew. I like this advice very much. There is another quite similar construction in my project, and hopefully I can unify them with the sort of generalization you’re suggesting.