search

ShapeOfMatter / MultiChor

Type-safe and efficient choreographies for Haskell, with multiply-located values, multi-cast, and location-set polymorphism.
Other
8 stars 0 forks source link

EPP should not be defined for non-participants #24

Open ShapeOfMatter opened 4 months ago

ShapeOfMatter commented 4 months ago

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.