on e35d643 help sign in
Idris-dev/samples/ST/Net/Threads.idr
23 lines 682 B history raw
1module Threads
3import Control.ST
4import System.Concurrency.Channels
5import System
7public export
8interface Conc (m : Type -> Type) where
9 -- 'Fork' sends some resources to the spawned thread, and keeps the rest
10 -- for the parent
11 -- TODO: Note that there is nothing here yet about how the threads
12 -- communicate with each other...
13 fork : (thread : STrans m () thread_res (const [])) ->
14 {auto tprf : SubRes thread_res all} ->
15 STrans m () all (const (kept tprf))
17export
18implementation Conc IO where
19 fork thread
20 = do threadEnv <- dropSub
21 lift $ spawn (do runWith threadEnv thread
22 pure ())
23 pure ()