Skip to content

Conversation

@ajrouvoet
Copy link
Contributor

This PR adds monotone predicate monads (re #508).
Contains:

  • The RawMPMonad interface
  • Various monads (Identity, Reader, Error, State, Heap) that instantiate that interface.
  • A means to program with those monads using strength in Agda.
  • A useful property for Any

I believe that in order to program with these things one needs to employ instance search
to construct Closed witnesses.
We should discuss where the necessary/useful instances should be defined.
Currently they are a bit scattered throughout the Category.Monad.Monotone.* modules.

Preconditions for the Heap instance in commit 3176534 are 2 pending PRs:

@ajrouvoet
Copy link
Contributor Author

ajrouvoet commented Nov 23, 2018

@gallais remarked that merge conflicts might be imminent with this PR depending on other pending PRs. If that is the case, I can prepare a new PR then.

@MatthewDaggitt
Copy link
Collaborator

remarked that merge conflicts might be imminent with this PR depending on other pending PRs. If that is the case, I can prepare a new PR then.

Merged Prefix in, so feel free to bring this up-to-date.

@MatthewDaggitt MatthewDaggitt removed this from the v0.18 milestone Jan 12, 2019
@MatthewDaggitt
Copy link
Collaborator

This PR hasn't aged well, there's lot of junk got merged in over time. @ajrouvoet I might take you up on your offer of a new PR (if you still want this in) and close this one.

@MatthewDaggitt MatthewDaggitt added status: won't-merge Decided against merging the PR in. and removed status:not-ready-yet labels Apr 23, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

addition status: won't-merge Decided against merging the PR in.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants