b54541f · 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

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

69 Nil : Env m Nil

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

71−

71+

72data EffElem : Effect -> Type ->

73 List EFFECT -> Type where

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

129

130-- ------------------------------------------------- [ The Language of Effects ]

131||| Definition of a language of effectful programs.

132−|||

132+|||

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

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

135||| @ ce Function to compute a new list of allowed side-effects.

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

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

141 Eff a xs xs'

142− ebind : Eff a xs xs' ->

142+ ebind : Eff a xs xs' ->

143 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

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

145 (eff : e t a b) ->

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

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

150

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

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

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

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

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

154

155−(>>=) : Eff a xs xs' ->

155+(>>=) : Eff a xs xs' ->

156 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

157−(>>=) = ebind

157+(>>=) = ebind

158

159-- namespace SimpleBind

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

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

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

162−-- (>>=) = ebind

162+-- (>>=) = ebind

163

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

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

182

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

184

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

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

186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)

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

188 arg <- v

205

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

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

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

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

209eff env (prog `ebind` c) k

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

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

248

249

250-- --------------------------------------------------------- [ Running Effects ]

251−

252−||| Run an effectful program

251+||| Run an effectful program.

252+|||

253+||| The content (`m`) in which to run the program is taken from the

254+||| environment in which the program is called. The `env` argument is

255+||| implicit and initialised automatically.

256+|||

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

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

258+run : Applicative m => {default MkDefaultEnv env : Env m xs}

259+ -> (prog : Eff a xs xs') -> m a

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

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

255

261

262+||| Run an effectful program in the identity context.

263+|||

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

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

266+|||

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

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

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

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

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

258

270

271+||| Run an effectful program in a given context `m` with a default value for the environment.

272+|||

273+||| This is useful for when there is no default environment for the given context.

274+|||

275+||| @env The environment to use.

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

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

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

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

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

261

279

280+||| Run an effectful program with a given default value for the environment.

281+|||

282+||| A helper function useful for when the given context is 'pure' and there is no default environment.

283+|||

284+||| @env The environment to use.

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

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

286+runPureInit : (env : Env id xs) -> (prog : Eff a xs xs') -> a

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

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

264

288

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

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

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

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

267

291

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

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

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

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

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

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

271

295