Atomic effect variables (?)

[omegametabroccolo]

Currently this is not possible:

alias eff<x::X,e::E> = <console,x|e>

test.kk(1,33): parse error: invalid syntax
  encountered effect variable x when an effect label was expected
    hint: effect variables must be after `|` (e.g `<labels|e>`), or by themselves (e.g. `e`)

@daanx In your paper describing Koka's effect system, you mention that "An extra restriction [of the type system] is that effect constants cannot be type variables, i.e. αk is illegal", but I didn't understand why this restriction is necessary from the rest of the paper.

I'm asking because I'm writing a library to write choreographies (1, 2, 3) in Koka, which essentially let you write distributed systems as monolitic programs. For example, the two_buyer example from (1) could be written like this:

fun two-buyer()
  val b1/title = b1.locally fn(_) input()
  val s/title = b1.comm(s, b1/title)
  val s/price = s.locally fn(un) catalog.get-price(s/title.un)
  val b1/price = s.comm(b1, s/price)
  val b2/price = s.comm(b2, s/price)
  val b1/contribution = b2.comm(b1, b2-budget)
  val b1/decision = b1.locally fn(un) b1/price <= b1/budget + contribution.un

  // enclave restricts the choreography to b1 and s only
  val b1s/decision = b1.share(s, b1/decision)
  enclave(b1, s) fn(un)

    // This shouldn't typecheck, since b2 isn't part of the sub choreography
    // val b2/dummy = b2.locally fn(_) 42

    if b1s/decision.un then
      val s/delivery = s.locally fn(un) catalog.get-delivery(s/title.un)
      val b1/delivery = s.comm(b1, s/delivery)
      b1.locally fn(un) b1/delivery.un
    else
      b1.locally fn(_) Nothing

I have a choreo effect that provides these operations. Since we want to enforce the census (the set of participants involved in a choreography), the effect should be parametrized over it. With atomic effect variables, we could represent the census with a row:

// A value of type a at location(s) l
type at<a,l::E>
  Local(v: a)
  Remote

// l1 and l2 are phantom types representing single participants (locations). k is a location container, for which we can compute actual values. For the two-buyer example, we could have defined:
//
// struct container<l::X>
//   name: string
//
// type buyer1 :: X
// val b1: container<buyer1> = Container("buyer1")
// ...
//
// choreo itself is private, the commented choreo<...> annotations are exposed by the public interface
alias choreo = <choreo-div<l,k,e>,div|e>
div effect choreo-div<l :: E, k :: X -> V, e :: E>
  // ...
  fun locally(l1: k<l1>, sub: (forall<t> at<t,<l1|_>> -> t) -> choreo<<l1>,k,e> a): /* choreo<<l1|_>,k,e> */ at<a,<l1>>
  fun enclave(l1: k<l1>, l2: k<l2>, sub: (forall<t> at<t,<l1,l2|_>> -> t) -> choreo<<l1,l2>,k,e> a): /* choreo<<l1,l2|_>,k,e> */ at<a,<l1,l2>>
  // ...

In the two-buyer example, enclave would enforce that only b1 and s can be involved in the sub choreography since its census row is closed (doing anything with b2 would be a type error, which is what we want), while the enclave itself is allowed to run within a choreography that involves more participants thanks to its open census row.

My current implementation uses phantom tuples to represent the census instead of phantom rows. I had to overload locally and enclave many times to describe in which contexts they can be used (i.e. a choreo<(l1,l2),...)> enclave is valid inside a choreo<(l2,_,l1),...> context, you can imagine the combinatorial explosion as censuses get bigger), but I just realized that I was just enumerating row extensions / reorderings manually. Maybe there are other solutions I didn't think of, but with atomic effect variables, rows would be a perfect fit.

(I glossed over a lot of details, especially related to choreographic programming, I'm happy to answer questions :))

[omegametabroccolo]

With a (hacky) patch to the compiler, the following example typechecks and enforces everything I want:

// khor.kk
module khor

type at<a :: V, c :: E>
  Local(v: a)
  Remote

pub alias khor<c :: E, k :: X -> V, e :: E> = <khor-div<c,k,e>,div|e>
div effect khor-div<c :: E, k :: X -> V, e :: E>
  fun local1(l1: k<l1>, sub: (forall<w,c0> at<w,<l1|c0>> -> w) -> khor<<l1>,k,e> a): at<a,<l1>>
  fun local2(l1: k<l1>, l2: k<l2>, sub: (forall<w,c0> at<w,<l1,l2|c0>> -> w) -> khor<<l1,l2>,k,e> a): at<a,<l1,l2>>
  fun local3(l1: k<l1>, l2: k<l2>, l3: k<l3>, sub: (forall<w,c0> at<w,<l1,l2,l3|c0>> -> w) -> khor<<l1,l2,l3>,k,e> a): at<a,<l1,l2,l3>>
  fun comm1(s: k<s>, r1: k<r1>, x: at<a,<s|c0>>): at<a,<s,r1|c0>>
  fun comm2(s: k<s>, r1: k<r1>, r2: k<r2>, x: at<a,<s|c0>>): at<a,<s,r1,r2|c0>>

pub fun local1/local(l1: k<l1>, sub: (forall<w,c0> at<w,<l1|c0>> -> w) -> khor<<l1>,k,e> a): khor<<l1|_>,k,e> at<a,<l1>> { local1(l1,sub) }
pub fun local2/local(l1: k<l1>, l2: k<l2>, sub: (forall<w,c0> at<w,<l1,l2|c0>> -> w) -> khor<<l1,l2>,k,e> a): khor<<l1,l2|_>,k,e> at<a,<l1,l2>> { local2(l1,l2,sub) }
pub fun local3/local(l1: k<l1>, l2: k<l2>, l3: k<l3>, sub: (forall<w,c0> at<w,<l1,l2,l3|c0>> -> w) -> khor<<l1,l2,l3>,k,e> a): khor<<l1,l2,l3|_>,k,e> at<a,<l1,l2,l3>> { local3(l1,l2,l3,sub) }
pub fun comm1/comm(s: k<s>, r1: k<r1>, x: at<a,<s|c0>>): khor<<s,r1|_>,k,e> at<a,<s,r1|c0>> { comm1(s,r1,x) }
pub fun comm2/comm(s: k<s>, r1: k<r1>, r2: k<r2>, x: at<a,<s|c0>>): khor<<s,r1,r2|_>,k,e> at<a,<s,r1,r2|c0>> { comm2(s,r1,r2,x) }

// two-buyer.kk
import khor

struct loc<l :: X>
  name: string

type buyer1 :: X
type buyer2 :: X
type seller :: X
val buyer1: loc<buyer1> = Loc("buyer1")
val buyer2: loc<buyer2> = Loc("buyer2")
val seller: loc<seller> = Loc("seller")

// two-buyer is inferred to be a choreography between a buyer1, a buyer2 and a seller
fun two-buyer()

  // Only buyer1 can unwrap and use b1/title, since it computes the title locally
  val b1/title = buyer1.local fn(_) "Control structures in programming languages"

  // This gets rejected by the type checker, since buyer1 hasn't sent the title to the seller yet
  // val s/price = seller.local fn(uw) { b1/title.uw.ignore; 30 }

  // Both buyer1 and seller can use s/title
  val s/title = buyer1.comm(seller, b1/title)

  // This shows that the seller can now unwrap s/title as a regular string (even if we don't actually use it to compute the price here)
  val s/price = seller.local fn(uw) { s/title.uw.ignore; 30 }

  // The seller sends the price to buyer1 and buyer2, who can both use it locally
  val b1b2/price = seller.comm(buyer1, buyer2, s/price)
  val b2/b2-contribution = buyer2.local fn(uw) b1b2/price.uw / 2
  val b1/b2-contribution = buyer2.comm(buyer1, b2/b2-contribution)

  // b1/b2-contribution is located at <buyer1,buyer2>, b1b2/price is located at <buyer1,buyer2,seller>. Both contain buyer1, uw can unwrap them
  val b1/decision = buyer1.local fn(uw) b1b2/price.uw <= b1/b2-contribution.uw + (b1b2/price.uw - 10)
  val b1s/decision = buyer1.comm(seller, b1/decision)
  
  // buyer2 isn't involved in the choreography anymore, we restrict the census to just buyer1 and seller
  local(buyer1, seller) fn(b1s/uw)

    // buyer2 *can't* be involved in the sub-choreography
    // buyer2.local fn(_) trace("impossible!")
    
    // Since the sub-choreography only involves buyer1 and seller, we can unwrap b1s/decision as a regular boolean. Both of them can follow the conditional!
    if b1s/decision.b1s/uw then
      val s/delivery = seller.local fn(s/uw) { s/title.s/uw.ignore; "Tomorrow" }
      val b1/delivery = seller.comm(buyer1, s/delivery)
      buyer1.local fn(b1/uw) Just(b1/delivery.b1/uw)
    else
      // For some reason, the result of at least one of the branches has to be bound to a variable before being returned
      val b1/nothing = buyer1.local fn(_) Nothing
      b1/nothing

I don't know if the patch is sound or if there is a way to make it sound, but it would sure make the khor module pretty neat :)

[omegametabroccolo]

After reading Extensible records with scoped labels I think I understand the problem a bit better.

Atomic effects correspond to labels, effect rows correspond to extensible records. Permutations are only allowed between distinct labels while equal labels follow some sort of stack discipline: if we add a label to a record that already contains it, we "mask" the previous label, and if we remove this new label we get the original label back. This corresponds to how effects and handlers behave at runtime: the order in which we install handlers for different effects doesn't matter, while the order does have an impact for equal effects (i.e. when we need to find the innermost handler when performing an effect).

I think the issue is that we can't know if two label (~ atomic effect) variables will be distinct or equal once instantiated, hence row equality (which relies on permutations) becomes messy.

If this is the only problem preventing your extensible records from allowing label variables, I think we can relax this restriction for effect rows? Every atomic effect in a row has kind X, swapping two equal atomic effects would effectively be a no-op, so we could allow arbitrary permutations (and atomic effect variables!) for rows.

[TimWhiting]

Interesting thought. I think the issue though is that even effects with variables <eff<a>,eff<b>> has kind <X,X> (you can see this as <(V -> X)(V), (V -> X)(V)> which reduces to <X,X> with typical type application).

[omegametabroccolo]

Could you explain how that would be a problem? If a and b end up being equal then eff<a> and eff<b> would also be equal, which corresponds the no-op case, but I'm having a hard time wrapping my head around the "a and b end up being distinct" case.

[TimWhiting]

Your statement here is wrong

If this is the only problem preventing your extensible records from allowing label variables, I think we can relax this restriction for effect rows? Every atomic effect in a row has kind X, swapping two equal atomic effects would effectively be a no-op, so we could allow arbitrary permutations (and atomic effect variables!) for rows

We cannot know if two atomic variables are equal or not without knowing what they actually are. So we cannot allow permutations of them.

[omegametabroccolo]

We cannot know if two atomic variables are equal or not without knowing what they actually are.

Say we have a row with atomic effect variables <l1,l2|e>. If they end up being distinct then the effect system allows us to swap them (<exn,console|e> ~> <console,exn|e>) . If they end up being equal, swapping them would just be an identity (<exn::X,exn::X|e> ~> <exn::X,exn::X|e>) which I think is safe, even though this is not true for extensible records (<l: string, l: int|r> ~/> <l: int, l: string|r>- note that both ls can have different types, while exns both have kind X) or installed handlers (with handler1 with handler2 f() ~/> <with handler2 with handler1 f()>).

Maybe I'm just missing something, but the idea is that even if we don't know if two atomic effect variables will be equal or not, it is always safe to swap them, as long as the permutation only happens in the effect type.

[TimWhiting]

But we can't swap two unknown variables: <l1::X,l2::X|e> != <l2::X,l1::X|e> where we can if we know what l1 / l2 are. l1 could be eff<a> and l2 could be eff<b> with a != b. Swapping them naively would cause the evidence for the handlers to be in the wrong order and the one for eff<a> would try to handle for eff<b> and vice versa -> and since a != b, there would be a segfault most likely. You could ask why not just swap the evidence as well. But that poses other difficulties. If a == b, then do we swap or not if we have both in the row. How do we know if the type is the same or needs swapping with duplicates? This matters, because it isn't just a presence of a handler that we want, but we want the effects to go to the right handler.

By the way, if you are interested in something like labels / rows, but for data and not handlers take a look at https://github.com/koka-community/type-level. It needs more documentation, but there are a few examples of what you can do.

[daanx]

Hi @omegametabroccolo , thanks for showing choreograpies :-) The fundamental reason to not allow atomic (label) effect variables is that unification than becomes difficult. For example, we may have to unify a row type <a,b> and a row type <div,exn> and now we cannot decide whether a~=div or a~=row (and same for b).

The usual way people resolve such issues is to delay the unification and make it a constraint (as a type class constraint), and generate a type like <a,b>~<div,exn> => () -> <a,b> () for example. However, that means we need to still find a way to solve such constraints nicely (and also be able to decide if a user annotation implies a certain contraint set). I remember studying this idea for a record system with first-class labels and as I remember solving such equations can quickly become very hard -- I can't find my old (rejected) submission anymore though :-( If I find it I'll post it here as it has many fun examples that show the issues.

(now, this doesn't mean we can't allow some restricted form of this for your case? Or perhaps you can use special parameterized effects to achieve what you need? or perhaps allow it through implicits constraints like hdiv?)

[TimWhiting]

Sorry if I came across too negative. I think there is definitely an opportunity to handle some of the issues pointed out by Daan and myself and in the various papers now that we have implicit constraints. I was just trying to say why it requires more work than just the "simple" fix.

[omegametabroccolo]

@TimWhiting No worries! Thank you for taking time to discuss the matter, my patch was just an experiment anyway :)

@daanx I'd love to read about first-class labels! Also, did you have something in mind when suggesting "special parametrized effects"?

I'm guessing the choreography example mostly works because every atomic effect variable that appears inside a row also appears in another position where it will be instantiated at the call site, e.g. in local1 we have at<a,<l1>>, but we also have l1: k<l1> - when we call b1.local ..., l1 is instantiated to buyer1 before any unification between rows, which dodges the issue (we would have problems writing choreographies that are polymorphic over their census though).

I tried my hand at writing a row-has implicit constraint, where row-has<r,p> makes the row r contain p:

struct loc<l :: X>

type alice :: X
type bob :: X
type carol :: X

val alice: loc<alice> = Loc
val bob: loc<bob> = Loc
val carol: loc<carol> = Loc

effect census<c :: E> {}

fun loc1/participate(l1: loc<l1>, ?l1/row-has: row-has<c,l1>): census<c> () ()
fun loc2/participate(l1: loc<l1>, l2: loc<l2>, ?l1/row-has: row-has<c,l1>, ?l2/row-has: row-has<c,l2>): census<c> () ()

// forall<e>. () -> (census<<bob,alice|e>>) ()
fun alice-and-bob()
  participate(alice,bob)

// forall<e>. () -> (census<<bob,alice,carol|e>>) ()
fun alice-and-bob-and-carol()
  participate(carol)
  alice-and-bob()

// We get census polymorphism by passing row-has evidence around
fun swap-roles-poly(l1: loc<l1>, l2: loc<l2>, ?l1/row-has: row-has<c,l1>, ?l2/row-has: row-has<c,l2>): census<c> ()
  participate(l2,l1,l2/row-has,l1/row-has)

  // This fails, maybe we shouldn't just return True in canResolveRowHasConstraint?
  // participate(l2,l1)

However, this has some problems. First, I'm not sure if the idea is sound or if the implementation is correct, I mostly copied it from the hdiv implementation. Also, this doesn't let us express closed rows containing variables (like <l1,l2>), which are needed for choreographies.

@HeikoRibberink We discussed atomic effect variables on Discord a while ago, could you explain how you wanted to use them? I think that could help us thinking about what we actually want.

[HeikoRibberink]

Interesting discussion; I don't think my original problem will be very useful, but I'll share it anyway.

I'm trying to handle effect operations on a different thread than they were issued on, via async streams.

My approach to this requires a user-defined handler that transforms the effect operation and payload into a unique value, and a function that can issue the same effect operation using that value.
This boils down to a single type class, generalizable.
Originally, I tried to quantize this type class over individual effect variables:

effect<a,r> ctl general(x : a) : r

struct generalizable<x::X,a::V,r::V>
  generalize : (action : () -> <x|e> b) -> <general<a,r>|e> b
  specify : (action : () -> <general<a,r>|e> b) -> <x|e> b)

But I realized that its also possible and in practice more useful to talk about two effect rows instead of the one-variable difference between these two:

struct generalizable<e::E,f::E,a::V,r::V>
  generalize : (action : () -> e b) -> <general<a,r>|f> b
  specify : (action : () -> <general<a,r>|f> b) -> e b