From cae4381319e7a3d6882c860446aadab722850938 Mon Sep 17 00:00:00 2001
From: Yuchen <lighght@umich.edu>
Date: Mon, 14 Oct 2024 23:27:58 -0400
Subject: [PATCH] example: free monad

---
 lang/lib/exec/alg.toml  |  3 +-
 lang/lib/exec/free.zy   | 90 +++++++++++++++++++++++++++++++++++++++++
 lang/lib/exec/proj.toml |  1 +
 3 files changed, 93 insertions(+), 1 deletion(-)
 create mode 100644 lang/lib/exec/free.zy

diff --git a/lang/lib/exec/alg.toml b/lang/lib/exec/alg.toml
index 9e5b4190..b7512e31 100644
--- a/lang/lib/exec/alg.toml
+++ b/lang/lib/exec/alg.toml
@@ -7,8 +7,9 @@ srcs = [
 deps = []
 bins = [
     # "alg.zy",
-    "algtrans.zy",
+    # "algtrans.zy",
     # "motrans.zy",
+    "free.zy",
 ]
 
 std = "NoStd"
diff --git a/lang/lib/exec/free.zy b/lang/lib/exec/free.zy
new file mode 100644
index 00000000..8a22deec
--- /dev/null
+++ b/lang/lib/exec/free.zy
@@ -0,0 +1,90 @@
+codata Kont (R: CType) (A: VType) where
+  | .run : U (A -> R) -> R
+end
+
+def ! kont (R: CType) : Monad (Kont R) =
+  comatch
+  | .return A a -> fn .run k ->
+    ! k a
+  | .bind A A' m f -> fn .run k ->
+    do~ ! m .run; fn a ->
+    ! f a .run k
+  end
+end
+
+data Err where
+  | +Msg : String
+end
+
+data Empty where end
+
+codata Handlers (R: CType) (K: CType) where
+  | .eff :
+       U (String -> U (Bool -> R) -> R) // print : String ~> Bool
+    -> U (Err -> U(Empty -> R) -> R) // fail : Err ~> Empty
+    -> U (Unit -> U(Bool -> R) -> R) // flip : Unit ~> Bool
+    -> K
+end
+
+codata Free (H: CType -> CType -> CType) (A: VType) where
+  | .run : forall (R: CType) . H R (U (A -> R) -> R)
+end
+
+def ! free : Monad (Free Handlers) =
+  comatch
+  | .return A a ->
+    fn .run R -> fn .eff print fail flip k -> ! k a
+  | .bind A A' m f -> fn .run R -> fn .eff print fail flip k' ->
+    ! m .run (R) .eff print fail flip { fn a ->
+      ! f a .run (R) .eff print fail flip k'
+    }
+  end
+end
+
+def ! print (s: String) : Free Handlers Bool =
+  fn .run R -> fn .eff print fail flip -> ! print s
+end
+
+def ! fail (e: Err) : Free Handlers Empty =
+  fn .run R -> fn .eff print fail flip -> ! fail e
+end
+
+def ! flip : Free Handlers Bool =
+  fn .run R -> fn .eff print fail flip -> ! flip ()
+end
+
+def ! print-os (s: String) (k: U (Bool -> OS)) : OS =
+  do~ ! write_line s;
+  ! k +True()
+end
+
+def ! print-str (s: String) (k: U (Bool -> Ret String)) : Ret String =
+  do s' <- ! k +True();
+  ! str_append s s'
+end
+
+def ! fail-os (e: Err) (_: U (Empty -> OS)) : OS =
+  match e
+  | +Msg(s) -> ! panic s
+  end
+end
+
+def ! flip-os (_: Unit) (kb: U (Bool -> OS)) : OS =
+  do~ ! random_int; fn i ->
+  do b <- ! mod i 2;
+  ! if~ (OS) { ! int_eq b 0 } { ! kb +True() } { ! kb +False() }
+end
+
+main
+  let m = {
+    do~ ! free .bind (Bool) (Unit) { ! print "a" }; fn _ ->
+    do~ ! free .bind (Bool) (Unit) { ! print "b" }; fn _ ->
+    do~ ! free .bind (Bool) (Unit) { ! flip }; fn b ->
+    do~ ! free .bind (Bool) (Unit) {
+      ! if (Free Handlers Bool) b { ! print "+" } { ! print "-" }
+    }; fn _ ->
+    ! free .return (Unit) ()
+  } in
+  do~ ! m .run (OS) .eff print-os fail-os flip-os; fn _ ->
+  ! exit 0
+end
diff --git a/lang/lib/exec/proj.toml b/lang/lib/exec/proj.toml
index b31f6e6f..bd76ceef 100644
--- a/lang/lib/exec/proj.toml
+++ b/lang/lib/exec/proj.toml
@@ -34,6 +34,7 @@ bins = [
     "explosion.zy",
     "fn-opt.zy",
     "forall.zy",
+    "free.zy",
     "hash.zy",
     "ifz.zy",
     "interpreter.zydeco",