9edaf2e · Idris-dev · git.iko.soy

10%access public

11-- ----------------------------------------------------------------- [ Effects ]

12||| The Effect type describes effectful computations.

13−|||

13+|||

14||| This type is parameterised by:

15||| + The input resource.

16||| + The return type of the computation.

28||| underlying computation context `m` for execution.

29class Handler (e : Effect) (m : Type -> Type) where

30 ||| How to handle the effect.

31− |||

31+ |||

32 ||| @ r The resource being handled.

33 ||| @ eff The effect to be applied.

34 ||| @ k The continuation to pass the result of the effect

35− covering handle : (r : res) -> (eff : e t res resk) ->

35+ covering handle : (r : res) -> (eff : e t res resk) ->

36 (k : ((x : t) -> resk x -> m a)) -> m a

37

38||| Get the resource type (handy at the REPL to find out about an effect)

48syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

49

50-- The state transition is dependent on a result `b`, a bound variable.

51−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]

52 = eff inst (\b => outst)

53

54--- A simple state transition

69 data Env : (m : Type -> Type) -> List EFFECT -> Type where

70 Nil : Env m Nil

71 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

72−

72+

73data EffElem : Effect -> Type ->

74 List EFFECT -> Type where

75 Here : EffElem x a (MkEff a x :: xs)

130

131-- ------------------------------------------------- [ The Language of Effects ]

132||| Definition of an Effect.

133−|||

133+|||

134||| @ m The computation context

135||| @ x The return type of the result.

136||| @ es The list of allowed side-effects.

142 value : a -> Eff m a xs (\v => xs)

143 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->

144 Eff m a xs xs'

145− ebind : Eff m a xs xs' ->

145+ ebind : Eff m a xs xs' ->

146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

147 callP : (prf : EffElem e a xs) ->

148 (eff : e t a b) ->

151 liftP : (prf : SubList ys xs) ->

152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

153 newInit : Handler e m =>

154− res ->

154+ res ->

155 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

156 Eff m a xs (\v => xs')

157 catch : Catchable m err =>

158 Eff m a xs xs' -> (err -> Eff m a xs xs') ->

159 Eff m a xs xs'

160

161− (:-) : (l : ty) ->

161+ (:-) : (l : ty) ->

162− Eff m t [x] xs' -> -- [x] (\v => xs) ->

162+ Eff m t [x] xs' -> -- [x] (\v => xs) ->

163 Eff m t [l ::: x] (\v => map (l :::) (xs' v))

164

165−(>>=) : Eff m a xs xs' ->

165+(>>=) : Eff m a xs xs' ->

166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

167−(>>=) = ebind

167+(>>=) = ebind

168

169-- namespace SimpleBind

170−-- (>>=) : Eff m a xs (\v => xs) ->

170+-- (>>=) : Eff m a xs (\v => xs) ->

171-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'

172−-- (>>=) = ebind

172+-- (>>=) = ebind

173

174||| Run a subprogram which results in an effect state the same as the input.

175staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)

192

193syntax pureM [val] = with_val val (pure ())

194

195−(<$>) : Eff m (a -> b) xs (\v => xs) ->

195+(<$>) : Eff m (a -> b) xs (\v => xs) ->

196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

197(<$>) prog v = do fn <- prog

198 arg <- v

215

216eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

217eff env (value x) k = k x env

218−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

218+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

219eff env (prog `ebind` c) k

220 = eff env prog (\p', env' => eff env' (c p') k)

221eff env (callP prf effP) k = execEff env prf effP k

263

264

265new : Handler e m =>

266− {default default r : res} ->

266+ {default default r : res} ->

267 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

268 Eff m a xs (\v => xs')

269new {r} e = newInit r e

270

271-- --------------------------------------------------------- [ Running Effects ]

272

273−||| Run an effectful program

273+||| Run an effectful program.

274+|||

275+||| The content (`m`) in which to run the program is taken from the environment in which the program is called.

276+||| The `env` argument is implicit and initialised automatically.

277+|||

278+||| @prog The effectful program to run.

274−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a

279+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a

275run {env} prog = eff env prog (\r, env => pure r)

280run {env} prog = eff env prog (\r, env => pure r)

276

281

282+||| Run an effectful program in the identity context `id`.

283+|||

284+||| A helper function useful for when the given context is 'pure'.

285+||| The `env` argument is implicit and initialised automatically.

286+|||

287+||| @prog The effectful program to run.

277−runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a

288+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a

278runPure {env} prog = eff env prog (\r, env => r)

289runPure {env} prog = eff env prog (\r, env => r)

279

290

291+||| Run an effectful program with a default value for the environment context.

292+|||

293+||| This is useful for when no default value exists for a given resource type.

294+|||

295+||| @val The default value for the resource type.

296+||| @prog The effectful program to run.

280−runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a

297+runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a

281runInit env prog = eff env prog (\r, env => pure r)

298runInit env prog = eff env prog (\r, env => pure r)

282

299

300+||| Run an effectful program in the identity context `id` with a given default value for the environment context.

301+|||

302+||| A helper function useful for when the given context is 'pure'.

303+|||

304+||| @val The default value for the resource type.

305+||| @prog The effectful program to run.

283−runPureInit : Env id xs -> Eff id a xs xs' -> a

306+runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a

284runPureInit env prog = eff env prog (\r, env => r)

307runPureInit env prog = eff env prog (\r, env => r)

285

308

286runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

309runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a

287runWith inj env prog = eff env prog (\r, env => inj r)

310runWith inj env prog = eff env prog (\r, env => inj r)

288

311

289−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

312+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->

290 m (x : a ** Env m (xs' x))

313 m (x : a ** Env m (xs' x))

291runEnv env prog = eff env prog (\r, env => pure (r ** env))

314runEnv env prog = eff env prog (\r, env => pure (r ** env))

292

315

297mapE f (x :: xs) = [| f x :: mapE f xs |]

320mapE f (x :: xs) = [| f x :: mapE f xs |]

298

321

299

322

300−mapVE : Applicative m =>

323+mapVE : Applicative m =>

301− (a -> {xs} Eff m b) ->

324+ (a -> {xs} Eff m b) ->

302− Vect n a ->

325+ Vect n a ->

303 {xs} Eff m (Vect n b)

326 {xs} Eff m (Vect n b)

304mapVE f [] = pure []

327mapVE f [] = pure []

305mapVE f (x :: xs) = [| f x :: mapVE f xs |]

328mapVE f (x :: xs) = [| f x :: mapVE f xs |]