Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Missing Monoid for Maybe and Add Point #845

Closed
gallais opened this issue Jul 22, 2019 · 6 comments
Closed

Missing Monoid for Maybe and Add Point #845

gallais opened this issue Jul 22, 2019 · 6 comments

Comments

@gallais
Copy link
Member

gallais commented Jul 22, 2019

For Maybe: empty is nothing and append is the first-just.

For Add.Point, empty is nothing and append is assuming the set we added a point to is a semigroup.

@gallais gallais changed the title Missing Monoid for Maybe Missing Monoid for Maybe and Add Point Jul 22, 2019
@lexvanderstoep
Copy link
Contributor

I'm planning to have a go at this issue. Could you explain what the first-just operator refers to?

@gallais
Copy link
Member Author

gallais commented Jul 25, 2019

Maybe is typically used for representing errors. As a consequence the sensible
notion of monoid is one where unit is nothing and multiplication is the function
which returns the first (left to right) value to be a just.

@lexvanderstoep
Copy link
Contributor

lexvanderstoep commented Jul 25, 2019

If I'm not mistaken, it seems to be that the _<|>_ operator is the first-just operator. The corresponding monoid is <|>-isMonoid in Data.Maybe.Properties.

Boarders added a commit to Boarders/agda-stdlib that referenced this issue Apr 17, 2022
Boarders added a commit to Boarders/agda-stdlib that referenced this issue Apr 17, 2022
Boarders added a commit to Boarders/agda-stdlib that referenced this issue Jul 3, 2022
Boarders added a commit to Boarders/agda-stdlib that referenced this issue Jul 3, 2022
@andreasabel andreasabel mentioned this issue Aug 27, 2023
@jamesmckinna
Copy link
Contributor

So... should this issue now be closed, since #1751 and @lexvanderstoep 's observation above?
Notwithstanding my own concerns under #1957 and the abandoned (for the time being) #1958 and #1963 , which we might revisit in the future...

@JacquesCarette
Copy link
Contributor

It feels like there is nothing left to do for this particular issue, so that keeping it open does not help us?

@jamesmckinna
Copy link
Contributor

@JacquesCarette i agree, but had been leaving this open for someone to reach the same conclusion...
... I think this falls under a time when issues weren't linked for automatic closure when PRs were merged addressing them. I've wasted some time on issues that seemed open, but were in fact already 'morally' closed... so let's do this here...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants