rowscript / rowscript

RowScript programming language, making a better browser world
https://rows.ro
MIT License
107 stars 1 forks source link

Effect types #153

Closed anqurvanillapy closed 4 months ago

anqurvanillapy commented 6 months ago

Users suggest that we need to treat the effects in a disciplined way, especially these:

Consider using Koka's row polymorphic effect types.

anqurvanillapy commented 6 months ago

Polymorphic effects.

Koka:

foo : ∀ u . (() → <exn | u> (), () → <exn | u> ()) → <exn | u> ()

RowScript:

foo
  : {u : row}
  → (args : ((args: unit) → u unit) * ((args : unit) → u unit) * unit)
  → {auto p : (exn: effect) keyof u}
  → u unit
anqurvanillapy commented 6 months ago

Duplicate effects.

Koka:

catch : ∀ a u . (() → <exn | u> a, exception → u a) → u a

RowScript:

catch
  : {a : type}
  → {u : row}
  → {v : row}
  → (args : ((args: unit) → u a) * ((args : exception * unit) → v a) * unit)
  → {auto p : u = v + (exn : effect)}
  → v a
anqurvanillapy commented 6 months ago

Eh, the basic Koka effects that could be used in RowScript are only exn... and yes the effects are extensible in Koka, but how could users define their own domain-specific effects?

The basic effects in RowScript should be:

anqurvanillapy commented 5 months ago

Koka's async effect is still being worked on and entirely based on the paper Structured Asynchrony with Algebraic Effects, where an async runtime is encoded directly using algebraic effects.

I personally don't like this approach since it's all "encoded", it brings the burden to the user if one really wants to dive in.

I prefer using its type signature and doing a simple CPS transformation for codegen, and then the effect performing (i.e. await) could be directly translated into JavaScript's native await. And with CPS resolve, we could implement the wait function in the paper for simulating things like Go's time.Sleep.

Interestingly, the type signature is pretty much like "call/cc".

effect async {
  fun await( initiate : (result⟨a⟩ → io ()) → io ()) : result⟨a⟩
}

The most general Haskell version callCC:

newtype Cont r a = Cont {runCont :: (a -> r) -> r}
callCC :: ((forall b. a -> Cont r b) -> Cont r a) -> Cont r a

There should be 3 basic constructs for users:

anqurvanillapy commented 5 months ago

The type signature of Koka's await looks like call/cc, but the semantics should not be related to it since it confuses our users. And we need to introduce a new syntax for the continuation-passing version of RowScript's await.

For now, we would have these asynchronous constructs in RowScript, which are super versatile:

And the sugars:

anqurvanillapy commented 5 months ago

Next we need to consider the CPS for await, await { ... } and Await.{all, any, race}.

anqurvanillapy commented 4 months ago

Notice that the await(expr0, expr1, ...) syntax, it's a direct call to interface method __await_let__:

interface AsyncLet {
    __await_let__<Args>(...: Args): Args;
}

So the arguments would actually be the resolved results, not the executor list. The ability of fine-grained executor control is not available in this syntax.

If we really need to have this support, e.g.:

await(
  { resolve(42) },
  { resolve(69) }
);

We actually need much dependent types magic like List<type> as input and the function signature as the output (i.e. larget elimination), and then generate the function in compile time, which is quite annoying.