0 | module System.Future
 1 |
 2 | %default total
 3 |
 4 | -- Futures based Concurrency and Parallelism
 5 |
 6 | export
 7 | data Future : Type -> Type where [external]
 8 |
 9 | %foreign "scheme:blodwen-make-future"
10 | prim__makeFuture : {0 a : Type} -> (() -> a) -> Future a
11 |
12 | %foreign "scheme:blodwen-await-future"
13 | prim__awaitFuture : {0 a : Type} -> Future a -> a
14 |
15 | export %inline -- inlining is important for correct context in codegens
16 | fork : Lazy a -> Future a
17 | fork l = prim__makeFuture $ \_ => force l
18 |
19 | export %inline -- inlining is important for correct context in codegens
20 | await : Future a -> a
21 | await f = prim__awaitFuture f
22 |
23 | public export
24 | Functor Future where
25 |   map func future = fork $ func (await future)
26 |
27 | public export
28 | Applicative Future where
29 |   pure v = fork v
30 |   funcF <*> v = fork $ (await funcF) (await v)
31 |
32 | public export
33 | Monad Future where
34 |   join = map await
35 |   v >>= func = join . fork $ func (await v)
36 |
37 | export
38 | performFutureIO : HasIO io => Future (IO a) -> io (Future a)
39 | performFutureIO = primIO . prim__io_pure . map unsafePerformIO
40 |
41 | export
42 | forkIO : HasIO io => IO a -> io (Future a)
43 | forkIO a = performFutureIO $ fork a
44 |