Skip to content

initial+terminal algebras #1902

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

Merged
merged 14 commits into from
Feb 28, 2023
Merged

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jan 7, 2023

Refactored Algebra.Construct.Zero into

  • Algebra.Construct.Initial
  • Algebra.Construct.Terminal

and fixed up the public (re-)imports of the second into Algebra.Construct.Zero (for backwards compatibility), while deprecating the occurrences of the non-initial terminal algebras in favour of their counterparts in Algebra.Construct.Terminal.

Also: amended Algebra.Module.Construct.Zero with commented-out hooks for the various Raw bundles associated with module-like algebras, pending the resolution of issue #1828

One wrinkle: I wanted to abstract out all the common structure, so i did that in each module via an additional private module, that nevertheless is opened into order to make the definitions (transparently) visible. But I may have got my private/public modifiers a bit mixed up. My concern is whether by making the internal modules private, I somehow fail to transparently export the definitions inside the publicly exported (raw) bundles, so that no actually reasoning is possible with them. But barring this wrinkle (fixable by removing the private modifiers), I think this one is now ready to go.

@JacquesCarette
Copy link
Contributor

Very nice!

A few remarks:

  • instead of the private/public thing you do, in Construct.Terminal you can define
    rawMagma = record { Carrier = ⊤ ; _≈_ = \ _ _ -> ⊤} and then everywhere else rawX = record { rawMagma } and you'll get the same thing.
  • for Construct.Initial, there are other 'weird' / 'exotic' equivalence relations on other than the one you give, and I think all of them will still "work". That's likely overkill though.

I don't think you need to change anything for this PR. You can if you think the result will be improved, but it's really unclear if that would indeed be the case.

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jan 8, 2023

Many thanks for the review and the suggestions regarding modularisation. I really wanted a DRY solution to all the repetition of the basic record structure, but I find the concrete syntax and semantics of these things hard to get my head round. Ideally I would have liked to reify the private module 𝕆ne as a record, and then 'paste it in-place', but I couldn't work out how to do that.

UPDATED: now everything in the module Terminal is definable as record { 𝕆ne } as I had hoped (but not quite understood previously)

As for defns of initial algebras on the empty carrier, I hope the present ones suffice. I wasn't really sure I could think of other ones which short-cut so much (though that's as nothing to the gain from eta-expansion of the unit type in the terminal case...)

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jan 10, 2023

Re; rationale for the PR.

EDITED: moved this to a distinct issue #1906, which can be tracked and closed by this (or similar) PR. Hopefully that makes my intentions a bit clearer.

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Jan 10, 2023
… branch/PR

Revert "`CHANGELOG`"

This reverts commit e54f2a7.
@jamesmckinna
Copy link
Contributor Author

Modulo discussion of @MatthewDaggitt 's concerns about deprecation/backwards compatibility, I think this is ready to go. But I'd like to clarify those issues before starting work on a PR towards fixing #1907

@MatthewDaggitt
Copy link
Contributor

Okay once the two outstanding conversations have been resolved, I'm happy to merge this.

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Feb 23, 2023

Final tweaks to remove private modifiers on the internal modules, and I was able to use them to construct all the other stuff as originally intended... including the Zero module.

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

Successfully merging this pull request may close these issues.

3 participants