feat: IO.asTask

src/Init/System/IO.lean

@@ -100,6 +100,21 @@ match e with
 def lazyPure {α : Type} (fn : Unit → α) : IO α :=
 pure (fn ())
 
+/-
+  Fork the world. This implementation is safe because all Lean function are (currently) maximally eta-expanded and
+  values are never lifted out of lambdas, so `Task.mk` is run only after the `RealWorld` token has been applied and the
+  effects of `act` happen no sooner than if `act` had been run directly. We add `noinline` just to be safe that
+  particular callers do not break these assumptions. -/
+@[noinline] unsafe def asTaskUnsafe {α : Type} (act : IO α) : IO (Task (Except IO.Error α)) :=
+pure (Task.mk fun _ => unsafeIO act)
+
+/--
+  Run `act` in a separate `Task`. This is similar to Haskell's [`unsafeInterleaveIO`](http://hackage.haskell.org/package/base-4.14.0.0/docs/System-IO-Unsafe.html#v:unsafeInterleaveIO),
+  except that the `Task` is started eagerly as usual. Thus pure accesses to the `Task` do not influence the impure `act`
+  computation. -/
+@[implementedBy asTaskUnsafe]
+constant asTask {α : Type} (act : IO α) : IO (Task (Except IO.Error α)) := arbitrary _
+
 inductive FS.Mode
 | read | write | readWrite | append
 

tests/lean/run/task_test_io.lean

@@ -0,0 +1,6 @@
+#eval do
+  t1 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "hi";
+  t2 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "ho";
+  IO.ofExcept t2.get;
+  IO.ofExcept t1.get;
+  pure ()