NOTE: effect type system

This note will not be very complete, but might become a series.

1. Effect as interface

The first case, use maybe to implement raise effect.

fun raise-maybe( action : () -> <raise|e> a ) : e maybe<a>
  with handler
    return(x)      Just(x)   // normal return: wrap in Just
    ctl raise(msg) Nothing   // exception: return Nothing directly
  1. <raise|e> ensure it's able to handle the effect other than raise
  2. maybe became the underlying implementation of effect raise
  3. return(x) lift the x : a into this monoid
  4. ctl should be something like abort in delimited continuation, but the type is ensured, rather than depends on context

2. Polymorphic effect

fun map : (xs : list<a>, f : (a) -> e b) -> e list<b>
  match xs
    Cons(x,xx) -> Cons( f(x), map(xx,f) )
    Nil        -> Nil

3. Current question

  1. How about

    fun foo() : <state<int>,state<int>,state<int>> int
  2. How to implement concurrency

Date: 2022-10-18 Tue 00:00

Author: Lîm Tsú-thuàn