Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #4
Closed
Open
Issue created Oct 24, 2015 by Ralf Jung@jungOwner

Re-do the basics: Cofe's and (CM)RA's

Slim down the algebraic hierarchy to contain only Cofe's, RA's and CMRA's, all as unbundled typeclasses and bundled canonical structures. Instead of a general notion of monotone function, we only really need one functor that maps a CMRA to monotone, step-indexed predicates over that CMRA. Maybe call that uPred? THat's kind of what it is, though it's not the same uPred that we had originally - that one could only deal with RA's.

Then we don't need the notion of a canonical partial order on a type - often, it's not even clear which one that should be. This also gives us the opportunity to define the metric and order on that uPred such that we can have "own(a) => valid(a)" as opposed to right now, where we have "own(a) \vs valid(a)". It's not entirely clear yet though if that latter part will actually work out without significant pain.

Assignee
Assign to
Time tracking