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

EPP should not be defined for non-participants #24

Open
ShapeOfMatter opened this issue May 2, 2024 · 1 comment
Open

EPP should not be defined for non-participants #24

ShapeOfMatter opened this issue May 2, 2024 · 1 comment
Labels
enhancement New feature or request

Comments

@ShapeOfMatter
Copy link
Owner

Consider the choreography

asdf :: Choreo '["a", "b"] (CLI m) Int
asdf = do x <- a `_locally` getInput "Enter a number"
                 x' <- (a `introAnd` a, x) ~> a @@ b @@ nobody
                 naked refl x'

I think I've written that so it's totally valid, but what happens if we try to project it to "c"? x' will be Empty, so naked can't work.

Since we need to determine at Haskell-Runtime which party we're projecting to, I don't think we can use our existing GDP approach on epp; i don't yet know how to fix this.

@ShapeOfMatter
Copy link
Owner Author

My current idea is to re-write EPP to take a Member p census arg instead of a LocTm. For this to happen elegantly, we should first refactor Located so it can have an instance of TestEquality for Member. (although... having such an instance will require deciding how to handle a census that contains the same party twice.)

Then we can recover the old behavior with some kind of forLocs wrapper maybe?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant