Theory IO

theory IO
  imports
    Main
    "HOL-Library.Monad_Syntax"
begin

section‹IO Monad›
text ‹
  Inspired by Haskell.
  Definitions from 🌐‹https://wiki.haskell.org/IO_inside›
›

subsection‹Real World›
text ‹
  We model the real world with a fake type.

  WARNING:
    Using low-level commands such as ⬚‹typedecl› instead of high-level ⬚‹datatype› is dangerous.
    We explicitly use a ⬚‹typedecl› instead of a ⬚‹datatype› because we never want to instantiate
    the world. We don't need a constructor, we just need the type.

  The following models an arbitrary type we cannot reason about.
  Don't reason about the complete world! Only write down some assumptions about parts of the world.
›
typedecl real_world (‹🌐›)

text‹
  For examples, see 🗏‹HelloWorld_Proof.thy›.
  In said theory, we model ▩‹STDIN› and ▩‹STDOUT› as parts of the world and describe how this part
  of the wold can be affected. We don't model the rest of the world. This allows us to reason about
  ▩‹STDIN› and ▩‹STDOUT› as part of the world, but nothing more.
›


subsection‹IO Monad›
text ‹
  The set of all functions which take a \<^typ>‹🌐› and return an \<^typ>‹'α› and a \<^typ>‹🌐›.

  The rough idea of all IO functions is the following: You are given the world in its current state.
  You can do whatever you like to the world. You can produce some value of type \<^typ>‹'α› and you
  have to return the modified world.

  For example, the ▩‹main› function is Haskell does not produce a value, therefore, ▩‹main› in
  Haskell is of type ▩‹IO ()›. Another example in Haskell is ▩‹getLine›, which returns ▩‹String›.
  It's type in Haskell is ▩‹IO String›. All those functions may also modify the state of the world.
›

typedef 'α io = "UNIV :: (🌐 ⇒ 'α × 🌐) set"
proof -
  show "∃x. x ∈ UNIV" by simp
qed

text ‹
  Related Work:
  ∗‹Programming TLS in Isabelle/HOL› by Andreas Lochbihler and Marc Züst uses a partial function
  (‹⇀›).
  ⬚‹
    typedecl real_world
    typedef 'α io = "UNIV :: (🌐 ⇀ 'α × 🌐) set" by simp
  ›
  We use a total function. This implies the dangerous assumption that all IO functions are total
  (i.e., terminate).
›

text ‹
  The ⬚‹typedef› above gives us some convenient definitions.
  Since the model of \<^typ>‹'α io› is just a mode, those definitions should not end up in generated
  code.
›
term Abs_io ― ‹Takes a \<^typ>‹(🌐 ⇒ 'α × 🌐)› and abstracts it to an \<^typ>‹'α io›.›
term Rep_io ― ‹Unpacks an \<^typ>‹'α io› to a \<^typ>‹(🌐 ⇒ 'α × 🌐)››


subsection‹Monad Operations›
text‹
  Within an \<^typ>‹'α io› context, execute \<^term>‹action⇩₁› and \<^term>‹action⇩₂› sequentially.
  The world is passed through and potentially modified by each action.
›
definition bind :: "'α io ⇒ ('α ⇒ 'β io) ⇒ 'β io" where [code del]:
  "bind action⇩₁ action⇩₂ = Abs_io (λworld⇩₀.
                                  let (a, world⇩₁) = (Rep_io action⇩₁) world⇩₀;
                                      (b, world⇩₂) = (Rep_io (action⇩₂ a)) world⇩₁
                                  in (b, world⇩₂))"

text ‹
  In Haskell, the definition for ▩‹bind› (▩‹>>=›) is:
  ▩‹
    (>>=) :: IO a -> (a -> IO b) -> IO b
    (action1 >>= action2) world0 =
       let (a, world1) = action1 world0
           (b, world2) = action2 a world1
       in (b, world2)
  ›
›

hide_const (open) bind
adhoc_overloading bind IO.bind

text ‹Thanks to ⬚‹adhoc_overloading›, we can use monad syntax.›
lemma "bind (foo :: 'α io) (λa. bar a) = foo ⤜ (λa. bar a)"
  by simp


definition return :: "'α ⇒ 'α io" where [code del]:
  "return a ≡ Abs_io (λworld. (a, world))"

hide_const (open) return

text ‹
  In Haskell, the definition for ▩‹return› is::
  ▩‹
    return :: a -> IO a
    return a world0  =  (a, world0)
  ›
›


subsection‹Monad Laws›
lemma left_id:
  fixes f :: "'α ⇒ 'β io" ― ‹Make sure we use our \<^const>‹IO.bind›.›
  shows "(IO.return a ⤜ f) = f a"
  by(simp add: return_def IO.bind_def Abs_io_inverse Rep_io_inverse)

lemma right_id:
  fixes m :: "'α io" ― ‹Make sure we use our \<^const>‹IO.bind›.›
  shows "(m ⤜ IO.return) = m"
  by(simp add: return_def IO.bind_def Abs_io_inverse Rep_io_inverse)
    
lemma bind_assoc:
  fixes m :: "'α io" ― ‹Make sure we use our \<^const>‹IO.bind›.›
  shows "((m ⤜ f) ⤜ g) = (m ⤜ (λx. f x ⤜ g))"
  by(simp add: IO.bind_def Abs_io_inverse Abs_io_inject fun_eq_iff split: prod.splits)


subsection‹Code Generator Setup›
text ‹
  We don't expose our \<^const>‹IO.bind› definition to code.
  We use the built-in definitions of the target language (e.g., Haskell, SML).
›
code_printing constant IO.bind ⇀ (Haskell) "_ >>= _"
                                  and (SML) "bind"
            | constant IO.return ⇀ (Haskell) "return"
                                    and (SML) "(() => _)"

text‹SML does not come with a bind function. We just define it (hopefully correct).›
code_printing code_module Bind ⇀ (SML) ‹
fun bind x f () = f (x ()) ();
›
code_reserved SML bind return
  
text‹
  Make sure the code generator does not try to define \<^typ>‹'α io› by itself, but always uses
  the one of the target language.
  For Haskell, this is the fully qualified Prelude.IO.
  For SML, we wrap it in a nullary function.
›
code_printing type_constructor io ⇀ (Haskell) "Prelude.IO _"
                                     and (SML) "unit -> _"


text‹
In Isabelle, a \<^typ>‹string› is just a type synonym for \<^typ>‹char list›.
When translating a \<^typ>‹string› to Haskell, Isabelle does not use Haskell's ▩‹String› or 
▩‹[Prelude.Char]›. Instead, Isabelle serializes its own
  ▩‹data Char = Char Bool Bool Bool Bool Bool Bool Bool Bool›.
The resulting code will look just ugly.

To use the native strings of Haskell, we use the Isabelle type \<^typ>‹String.literal›.
This gets translated to a Haskell ▩‹String›.

A string literal in Isabelle is created with \<^term>‹STR ''foo'' :: String.literal›.
›

text‹
  We define IO functions in Isabelle without implementation.
  For a proof in Isabelle, we will only describe their externally observable properties.
  For code generation, we map those functions to the corresponding function of the target language.

  Our assumption is that our description in Isabelle corresponds to the real behavior of those
  functions in the respective target language.

  We use ⬚‹axiomatization› instead of ⬚‹consts› to axiomatically define that those functions exist,
  but there is no implementation of them. This makes sure that we have to explicitly write down all
  our assumptions about their behavior. Currently, no assumptions (apart from their type) can be
  made about those functions.
›
axiomatization
  println :: "String.literal ⇒ unit io" and
  getLine :: "String.literal io"

text ‹A Haskell module named ▩‹StdIO› which just implements ▩‹println› and ▩‹getLine›.›
code_printing code_module StdIO ⇀ (Haskell) ‹
module StdIO (println, getLine) where
import qualified Prelude (putStrLn, getLine)
println = Prelude.putStrLn
getLine = Prelude.getLine
›                              and (SML) ‹
(* Newline behavior in SML is odd.*)
fun println s () = TextIO.print (s ^ "\n");
fun getLine () = case (TextIO.inputLine TextIO.stdIn) of
                  SOME s => String.substring (s, 0, String.size s - 1)
                | NONE => raise Fail "getLine";
›

code_reserved Haskell StdIO println getLine
code_reserved SML println print getLine TextIO

text‹
  When the code generator sees the functions \<^const>‹println› or \<^const>‹getLine›, we tell it to use
  our language-specific implementation.
  ›
code_printing constant println ⇀ (Haskell) "StdIO.println"
                              and (SML) "println"
            | constant getLine ⇀ (Haskell) "StdIO.getLine"
                              and (SML) "getLine"


text‹Monad syntax and \<^const>‹println› examples.›
lemma "bind (println (STR ''foo''))
            (λ_.  println (STR ''bar'')) =
       println (STR ''foo'') ⤜ (λ_. println (STR ''bar''))"
  by simp 
lemma "do { _ ← println (STR ''foo'');
            println (STR ''bar'')} =
      println (STR ''foo'') ⪢ (println (STR ''bar''))"
  by simp



subsection‹Modelling Running an \<^typ>‹'α io› Function›
text‹
  Apply some function \<^term>‹iofun :: 'α io› to a specific world and return the new world
  (discarding the result of \<^term>‹iofun›).
›
definition exec :: "'α io ⇒ 🌐 ⇒ 🌐" where
  "exec iofun world = snd (Rep_io iofun world)"

text‹Similar, but only get the result.›
definition eval :: "'α io ⇒ 🌐 ⇒ 'α" where
  "eval iofun world = fst (Rep_io iofun world)"

text‹
  Essentially, \<^const>‹exec› and \<^const>‹eval› extract the payload \<^typ>‹'α› and \<^typ>‹🌐›
  when executing an \<^typ>‹'α io›.
›
lemma "Abs_io (λworld. (eval iofun world, exec iofun world)) = iofun"
  by(simp add: exec_def eval_def Rep_io_inverse)

lemma exec_Abs_io: "exec (Abs_io f) world = snd (f world)"
  by(simp add: exec_def Abs_io_inverse)


lemma exec_then:
    "exec (io⇩₁ ⪢ io⇩₂) world = exec io⇩₂ (exec io⇩₁ world)"
  and eval_then:
    "eval (io⇩₁ ⪢ io⇩₂) world = eval io⇩₂ (exec io⇩₁ world)"
  by (simp_all add: exec_def eval_def bind_def Abs_io_inverse split_beta)

lemma exec_bind:
    "exec (io⇩₁ ⤜ io⇩₂) world = exec (io⇩₂ (eval io⇩₁ world)) (exec io⇩₁ world)"
  and eval_bind:
    "eval (io⇩₁ ⤜ io⇩₂) world = eval (io⇩₂ (eval io⇩₁ world)) (exec io⇩₁ world)"
  by(simp_all add: exec_def eval_def bind_def Abs_io_inverse split_beta)

lemma exec_return:
    "exec (IO.return a) world = world"
  and
    "eval (IO.return a) world = a"
  by (simp_all add: exec_def eval_def Abs_io_inverse return_def)


end