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

Open union encoding of Eon #319

Closed
wants to merge 5 commits into from
Closed

Open union encoding of Eon #319

wants to merge 5 commits into from

Conversation

newhoggy
Copy link
Collaborator

Changelog

- description: |
    WIP Open union encoding of Eon
# uncomment types applicable to the change:
  type:
  # - feature        # introduces a new feature
  # - breaking       # the API has changed in a breaking way
  # - compatible     # the API has changed but is non-breaking
  # - optimisation   # measurable performance improvements
  # - improvement    # QoL changes e.g. refactoring
  # - bugfix         # fixes a defect
  # - test           # fixes/modifies tests
  # - maintenance    # not directly related to the code
  # - release        # related to a new release preparation
  # - documentation  # change in code docs, haddocks...

Context

This doesn't work.

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • The change log section in the PR description has been filled in
  • New tests are added if needed and existing tests are updated. These may include:
    • golden tests
    • property tests
    • round trip tests
    • integration tests
      See Running tests for more details
  • The version bounds in .cabal files are updated
  • CI passes. See note on CI. The following CI checks are required:
    • Code is linted with hlint. See .github/workflows/check-hlint.yml to get the hlint version
    • Code is formatted with stylish-haskell. See .github/workflows/stylish-haskell.yml to get the stylish-haskell version
    • Code builds on Linux, MacOS and Windows for ghc-8.10.7 and ghc-9.2.7
  • Self-reviewed the diff


relaxEon :: ()
=> Contains as bs
=> IsMember a bs -- This constraing shouldn't be needed
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I remove this constraint, I get the following error:

internal/Cardano/Api/Eon/Core.hs:50:20: error:
    • You require open sum type to contain the following element:
          a
      However, given list can store elements only of the following types:
          bs
    • In the expression: Eon (relaxOpenUnion a)
      In an equation for ‘relaxEon’:
          relaxEon (Eon a) = Eon (relaxOpenUnion a)
   |
50 | relaxEon (Eon a) = Eon (relaxOpenUnion a)
   |                    ^^^^^^^^^^^^^^^^^^^^^^

I know I don't need the constraint because if a ∈ as and as ⊆ bs then it follows that a ∈ bs, but the constraints provided by world-peace library aren't able to infer this.

SubsetNil ->
MemberTail MemberHead
MemberTail mzz ->
case mzz of {}
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

An concrete version of a function I ultimately want to write and I think I might need:

memberSubset :: era ∈ small -> small ⊆ large -> era ∈ large

Copy link

github-actions bot commented Dec 2, 2023

This PR is stale because it has been open 45 days with no activity.

@github-actions github-actions bot added the Stale label Dec 2, 2023
Copy link

github-actions bot commented Feb 1, 2024

This issue was closed because it has been stalled for 60 days with no activity.

@github-actions github-actions bot closed this Feb 1, 2024
newhoggy pushed a commit that referenced this pull request Mar 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant