Last active
August 12, 2019 12:18
-
-
Save jcreedcmu/1e06ad9eec3a54ffcb7401efe8476947 to your computer and use it in GitHub Desktop.
fun with higher order functors
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Plain old ordinary monad *) | |
signature MONAD = sig | |
type 'x t | |
val return: 'x -> 'x t | |
val bind : 'x t -> ('x -> 'y t) -> 'y t | |
end | |
(* | |
Monad indexed by one other type. Not even as fancy as "indexed monads | |
a la Atkey" (for which see | |
http://stackoverflow.com/questions/28690448/what-is-indexed-monad ) | |
*) | |
signature IMONAD = sig | |
type ('a, 'x) t | |
val return: 'x -> ('a, 'x) t | |
val bind : ('a,'x) t -> ('x -> ('a,'y) t) -> ('a,'y) t | |
end | |
(* | |
A monadic computation of a certain shape. It takes an "effect" of | |
(morally) type A -> B and yields a C, except we have to annotate | |
function returns with the monad. | |
*) | |
signature MONADIC = sig | |
type A | |
type B | |
type C | |
functor F(M: MONAD): sig val go: (A -> B M.t) -> C M.t end | |
end | |
(* | |
A data structure that represents a "trace" of sorts - the result of | |
such a computation in a more directly digestible form. We can read | |
off whether it has returned a final value of type 'c, or else invoked | |
the "effect" with a value of type 'a, and a continuation that takes a | |
'b and some more computation to do. | |
*) | |
datatype ('a, 'b, 'c) trace = | |
Val of 'c | |
| Call of 'a * ('b -> ('a, 'b, 'c) trace) | |
signature TRACE = sig | |
type A | |
type B | |
type C | |
val res: (A, B, C) trace | |
end | |
(********************************************************************** | |
The fun thing we can do is convert from actual monadic computations --- | |
things of signature MONADIC --- to traces, by plugging in the | |
continuation monad. | |
***********************************************************************) | |
(* Here is the continuation monad: *) | |
structure Cont: IMONAD = struct | |
type ('a, 'x) t = ('x -> 'a) -> 'a | |
fun return x f = f x | |
fun bind f g h = f (fn x => g x h) | |
end | |
(* And here we do the plugging-in: *) | |
functor Cvt(Comp: MONADIC): TRACE = struct | |
open Comp | |
structure Instantiate = F(struct | |
open Cont | |
type 'x t = ((A, B, C) trace, 'x) t | |
end) | |
val res = Instantiate.go (fn a => fn g => Call (a, g)) Val | |
end | |
(* Here's an example of a monadic computation. It assumes an effect of type int->string *) | |
structure MyComp: MONADIC = struct | |
type A = int; type B = string; type C = string; | |
functor F(M: MONAD) = struct | |
open M | |
(* It calls that effect three times on three different integers and concatenates the outputs *) | |
fun go ext = | |
bind (ext 1) (fn x => | |
bind (ext 2) (fn y => | |
bind (ext 4) (fn z => return (x ^ " " ^ y ^ " " ^ z)))) | |
end | |
end | |
(* Plug stuff together: *) | |
structure Go = Cvt(MyComp) | |
(* | |
Here we can implement an 'effect handler' as an ordinary function that takes a trace as input. | |
Just for an example, we keep a counter s, and a call to the effect is interpreted as | |
"increment the counter by n, and return the stringification of the current value of the counter" | |
*) | |
fun run s (Val x) = x | |
| run s (Call (n, k)) = let val s' = s + n in run s' (k (Int.toString s')) end | |
val out = run 0 Go.res (* yields "1 3 7" *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment