|
| 1 | +:NewDefs |
| 2 | +:NoJS |
| 3 | + |
| 4 | + |
| 5 | +// * A monadic effect type, covariant in base type and effect type |
| 6 | +class Effectful[out A, out E](value: A) { |
| 7 | + fun flatMap[B](f: A => Effectful[B, E]): Effectful[B, E] = |
| 8 | + f(value) |
| 9 | +} |
| 10 | +fun pure[A](a: A): Effectful['a, 'e] = Effectful(a) |
| 11 | +//│ class Effectful[A, E](value: A) { |
| 12 | +//│ fun flatMap: forall 'B. (f: A -> Effectful['B, E],) -> Effectful['B, E] |
| 13 | +//│ } |
| 14 | +//│ fun pure: forall 'a. (a: 'a,) -> Effectful['a, nothing] |
| 15 | + |
| 16 | +// * Some effect tags |
| 17 | +module IO |
| 18 | +module Block |
| 19 | +//│ module IO |
| 20 | +//│ module Block |
| 21 | + |
| 22 | +// * Some example functions |
| 23 | +fun println(x: anything): Effectful[(), IO] |
| 24 | +fun readLine: Effectful[Str, IO | Block] |
| 25 | +//│ fun println: (x: anything,) -> Effectful[(), IO] |
| 26 | +//│ fun readLine: Effectful[Str, Block | IO] |
| 27 | + |
| 28 | + |
| 29 | +// * Define NonBlocking as an effectful computation that does not block (using type-level difference `\`) |
| 30 | +type NonBlocking[out A, out E] = Effectful[A, E \ Block] |
| 31 | +//│ type NonBlocking[A, E] = Effectful[A, E & ~Block] |
| 32 | + |
| 33 | +// * Example use of NonBlocking in an annotation; the type arguments are inferred |
| 34 | +fun f(x) = x : NonBlocking |
| 35 | +//│ fun f: forall 'a 'b. NonBlocking['a, 'b] -> NonBlocking['a, 'b] |
| 36 | + |
| 37 | + |
| 38 | +// * the `listener` callback should be non-blocking |
| 39 | +fun onMousePressed(listener) = |
| 40 | + fun l(e) = listener(e) : NonBlocking |
| 41 | + l(0).flatMap of a => l(1).flatMap of b => pure of () |
| 42 | +//│ fun onMousePressed: forall 'a. ((0 | 1) -> NonBlocking[anything, 'a]) -> Effectful[(), 'a & ~Block] |
| 43 | + |
| 44 | + |
| 45 | +// * OK: `println` does not block |
| 46 | +onMousePressed(event => println("Clicked!")) |
| 47 | +//│ Effectful[(), IO & ~Block] |
| 48 | + |
| 49 | +// * NOT OK: `readLine` blocks |
| 50 | +:e |
| 51 | +onMousePressed(event => readLine.flatMap(println)) |
| 52 | +//│ ╔══[ERROR] Type mismatch in application: |
| 53 | +//│ ║ l.51: onMousePressed(event => readLine.flatMap(println)) |
| 54 | +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
| 55 | +//│ ╟── type `Block` does not match type `~Block` |
| 56 | +//│ ║ l.24: fun readLine: Effectful[Str, IO | Block] |
| 57 | +//│ ╙── ^^^^^ |
| 58 | +//│ Effectful[(), IO & ~Block] | error |
| 59 | + |
| 60 | + |
| 61 | +class Event |
| 62 | +class MouseEvent: Event |
| 63 | +module Register |
| 64 | +//│ class Event |
| 65 | +//│ class MouseEvent: Event |
| 66 | +//│ module Register |
| 67 | + |
| 68 | +fun onMousePressed(listener) = |
| 69 | + fun l(e: MouseEvent) = listener(e) : Effectful[(), 'e \ Block \ Register] |
| 70 | + () |
| 71 | +//│ fun onMousePressed: (MouseEvent -> Effectful[(), ~Block & ~Register]) -> () |
| 72 | + |
| 73 | +// def onMouseClick ( f : Event -> Unit \ { ef - Register }): Unit \ { Register } |
| 74 | +fun onMouseClick(f: Event -> Effectful[(), 'e \ Register]): Effectful[(), Register] |
| 75 | +//│ fun onMouseClick: (f: Event -> Effectful[(), ~Register],) -> Effectful[(), Register] |
| 76 | + |
| 77 | +onMouseClick of ev => pure of () |
| 78 | +//│ Effectful[(), Register] |
| 79 | + |
| 80 | +:e |
| 81 | +onMouseClick of ev => |
| 82 | + onMouseClick(ev => pure of ()).flatMap of _ => |
| 83 | + pure of () |
| 84 | +//│ ╔══[ERROR] Type mismatch in application: |
| 85 | +//│ ║ l.81: onMouseClick of ev => |
| 86 | +//│ ║ ^^^^^^^^^^^^^^^^^^^^^ |
| 87 | +//│ ║ l.82: onMouseClick(ev => pure of ()).flatMap of _ => |
| 88 | +//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
| 89 | +//│ ║ l.83: pure of () |
| 90 | +//│ ║ ^^^^^^^^^^^^^^ |
| 91 | +//│ ╟── type `Register` does not match type `~Register` |
| 92 | +//│ ║ l.74: fun onMouseClick(f: Event -> Effectful[(), 'e \ Register]): Effectful[(), Register] |
| 93 | +//│ ╙── ^^^^^^^^ |
| 94 | +//│ Effectful[(), Register] | error |
| 95 | + |
| 96 | + |
0 commit comments