doc(init/category/cont): add docs and test

library/init/category/cont.lean

@@ -10,13 +10,19 @@ prelude
 import init.category.alternative init.category.combinators init.category.lift
 universes u v w
 
+/-- An implementation of [ContT](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html#t:ContT) -/
 structure cont_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
 (run : (α → m ρ) → m ρ)
 
 attribute [pp_using_anonymous_constructor] cont_t
 
+/-- An implementation of [MonadCont done right](https://wiki.haskell.org/MonadCont_done_right) -/
 class monad_cont (m : Type u → Type v) :=
-(call_cc {α β : Type u} : ((α → m β) → m α) → m α)
+/- Call a function with the current continuation (cc) as its argument, which can be called to
+   exit the function from anywhere inside it. -/
+(call_cc {α : Type u} : ((∀ {β}, α → m β) → m α) → m α)
+
+export monad_cont (call_cc)
 
 @[reducible] def cont (ρ α : Type u) : Type u := cont_t ρ id α
 
@@ -33,10 +39,18 @@ section
   instance : monad (cont_t ρ m) :=
   { pure := @pure, bind := @bind }
 
-  protected def call_cc {α β : Type u} (f : (α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
-  ⟨λ cc, (f (λ a, ⟨λ _, cc a⟩)).run cc⟩
+  protected def call_cc {α : Type u} (f : (∀ {β}, α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
+  ⟨λ cc, (f (λ _ a, ⟨λ _, cc a⟩)).run cc⟩
 
   instance : monad_cont (cont_t ρ m) :=
   ⟨@call_cc⟩
+
+  protected def lift [_root_.monad m] {α : Type u} (x : m α) : cont_t ρ m α :=
+  ⟨λ cc, x >>= cc⟩
+
+  instance [_root_.monad m] : has_monad_lift m (cont_t ρ m) :=
+  ⟨@cont_t.lift _⟩
+
+  -- there is NO instance of `monad_functor` for `cont_t`
 end
 end cont_t

tests/lean/run/cont.lean

@@ -0,0 +1,17 @@
+import system.io
+
+-- count the even numbers from 0 to 7 in a horrible, imperative way
+def cont_example : cont_t unit (state_t ℕ io) ℕ :=
+do call_cc $ λ break,
+    (list.range 10).mmap' $ λ i,
+      call_cc $ λ continue, do {
+        when (i % 2 = 0) $
+          continue (),
+        when (i > 7) $
+          break (),
+        modify (+1) >> pure ()
+      },
+   get
+
+#eval do ((), 4) ← (cont_example.run (λ _, pure ())).run 0,
+         pure ()