macabeus/js-proposal-algebraic-effects

How will the effect interact with the ecosystem of TypeScript?

Jack-Works opened this issue · 8 comments

How will the effect interact with the ecosystem of TypeScript?
  • Implicit types and expressions should be enforced
  • Values should be kept in local expressions
  • Effect handling should have proper scope declaration
try {
} handle {
  effect ... // this is a no-no, since effect would become a global such as 'window'
}

maybe this:

try {
} handle (effect) {
}

nowadays, an exception in typescript is enforced to type any. this makes us can't have checked exception features.

This should not happen again in the algebra effect. The function should be implicitly colored by the algebra effect

Following this approach we could have something like that:

try {
  ...
} handle ((effect: TMyType) if effect.value > 10) {
  // here we know that "effect" is a TMyType
}

or

try {
  ...
} handle (effect if effect === 'foo') {
  // here we know that "effect" is 'foo'
}

or

try {
  ...
} handle (effect if isString(effect)) {
  // here we know that "effect" is a string
}

It'll not avoid any anytime, of course:

try {
  ...
} handle (effect if true) {
  // "effect" is any
}

Aren’t MS folks the exact people who came up with the effect language Koka? They certainly have an idea about how, so the question is more about whether they will do it.

On the typing end, it certainly helps to add type-checking to perform/throw, possibly using new keywords like foo(bar: number, f: (x: number) => number) : number throws ValueError performs TrapOverflow | TrapUnderflow handles DivideByZero.

There is, however, no real motivation for error type checking, at least to the extent of polyfilling done by TS since it never needs to be polyfilled. Effects will need polyfilling, so TS has an interest in knowing what causes what and stops what.

(As a part of the possibly wild world, we need a Proxy-like for run time type checking too. We can rethrow with resume with perform effect in a real engine I guess?)

On the typing end, it certainly helps to add type-checking to perform/throw, possibly using new keywords like foo(bar: number, f: (x: number) => number) : number throws ValueError performs TrapOverflow | TrapUnderflow handles DivideByZero.

I think just throws and performs is enough, because handles is not orthogonal to throws.
E.g. if you don't handle some exception in your function, then that exception appears in throws. If you do handle the exception, then it doesn't appear in throws.

So it could be something like this:

apiCall(path: string): Result throws Error performs HTTPRequest

@Artoria2e5 I asked TS guys about that (I think, even before you asked). I was told TS and RiSE teams never communicated, and it's for some reason hard for them to do so.

Typing effects in TS isn't going to be hard due to implementation, but it won't be easy either for other reason . Functions get annotated with yet another place for a type:

const f = (...args: A): R effect E => {};

Typechecker computes intersection type of effects for every call site inside of a function. For example,

declare const f1: () => void effect E1;
declare const f2: () => void effect E2;
const f12 = () => { f1(); f2(); }; // : () => void effect (E1 & E2)

Now throw x can generate a {throw: typeof x} effect (built-in), and React's useContext() can generate a {context: (c: C) => any}. Effects' variance is modelled naturally by TS type system here.

const f = { throw 42; }; // : () => never effect {throw: 42}

try...handle would just Exclude<> handled effects prior to intersection.

@polkovnikov-ph Trying to get my head around this, why does f12 in your example not have the type () => void effect (E1 | E2)? ie. why does the sequential application of effectful functions product an intersection, and not a union, of effects?