getting_started.html.erb

<%= header(:getting_started) %>
      <div class="row">
        <div class="col-md-12">
          <h1>Getting started</h1>
          <ul>
            <li><a href="#hello-world">Write a Hello World</a></li>
            <li><a href="#examples">More examples</a></li>
            <li><a href="#concurrency">Use concurrency</a></li>
            <li><a href="#effects">The effects system</a></li>
            <li><a href="#use-cases">Verification by use cases</a></li>
          </ul>
          <p>To install the <a href="http://coq.io/">Coq.io</a> library, enable the Coq OPAM repository:</p>
          <pre>opam repo add coq-released https://coq.inria.fr/opam/released</pre>
          <p>and run:</p>
          <pre>opam install -j4 -v coq-io-system</pre>
          This will install the main library <a href="https://github.com/coq-io/io"><code>coq-io</code></a> and some basic effects <a href="https://github.com/coq-io/system"><code>coq-io-system</code></a> to interact with your operating system.

          <h2 id="hello-world">Write a Hello World</h2>
          Open your favorite <a href="https://coq.inria.fr/">Coq</a> editor and type:
          <pre>Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.

Import ListNotations.
Import C.Notations.

(** The classic Hello World program. *)
Definition hello_world (argv : list LString.t) : C.t System.effect unit :=
  System.log (LString.s "Hello world!").</pre>
          <p>We load some libraries and write the <code>hello_world</code> program by calling the <code>System.log</code> function to print a message on the terminal. The return type of the program is <code>C.t System.effect unit</code>, which means this is an <em>impure</em> computation with the <em>system</em> effect and returning a value of type <code>unit</code>. The impure computations are the computations which are not purely functional, in the sense they do some effects, like IO or modifying a state variable. The system effect is an effect we use to do IO with the system. The command-line arguments are given by the list of strings <code>argv</code>, but are not used here.</p>

          <p>To compile the <code>hello_world</code> program to generate an <a href="https://ocaml.org/">OCaml</a> file <code>main.ml</code>, add the lines:</p>
          <pre>Definition main := Extraction.launch hello_world.
Extraction "extraction/main" main.</pre>
          <p>We compile and run <code>main.ml</code> with:</p>
          <pre>ocamlbuild main.native -use-ocamlfind -package io-system
./main.native</pre>
          <p>This should display <code>Hello world!</code> on the terminal.</p>

          <h2 id="examples">More examples</h2>
          <p>The full documentation of the <a href="https://github.com/coq-io/system"><code>coq-io-system</code></a> library is available on <a href="http://coq-io.github.io/doc/system/2.3.0/toc.html">v2.3.0</a>.</p>

          <h3>Your name</h3>
          <p>The following program reads a name on the command-line and answers "hello" to this name:</p>
          <pre>(** Ask for the user name and answer hello. *)
Definition your_name (argv : list LString.t) : C.t System.effect unit :=
  do! System.log (LString.s "What is your name?") in
  let! name := System.read_line in
  match name with
  | None => ret tt
  | Some name => System.log (LString.s "Hello " ++ name ++ LString.s "!")
  end.</pre>
          <p>We see here how to compose impure computations in sequence with the <code>do!</code> and <code>let!</code> keywords. The construct:</p>
          <pre>let! x := e1 in e2</pre>
          <p>executes <code>e1</code>, assigns the result to <code>x</code> and then executes <code>e2</code>. The <code>do!</code> is a syntactic sugar for a <code>let!</code> without a variable <code>x</code>, so for the case of <code>e1</code> returning the <code>unit</code> value. We use the <code>System.read_line</code> function which reads a new line on the standard input. If the <code>read_line</code> operation fails, we returns the pure value <code>tt</code> of type <code>unit</code> using the <code>ret</code> operator, else we print the user name on the terminal. We run this program as before by compilation to OCaml.</p>

          <h3>Cat</h3>
          <p>This program opens a file and displays its content:</p>
          <pre>(** Display the content of a file. *)
Definition cat (argv : list LString.t) : C.t System.effect unit :=
  match argv with
  | [_; file_name] =>
    let! content := System.read_file file_name in
    match content with
    | None => System.log (LString.s "Cannot read the file.")
    | Some content => System.log content
    end
  | _ => System.log (LString.s "Expected one parameter.")
  end.</pre>
        <p>It is analogous to the <code>cat</code> Unix command. It uses the command-line argument to get the file name to display, and then read the file with <code>System.read_file</code>.</p>

          <h3>Uname</h3>
          <p>This program wrap the <code>uname</code> command to display the operating system kind and the type of machine:</p>
          <pre>Require Import Coq.ZArith.ZArith.

(** A wrapper for the `uname` command. *)
Definition uname (argv : list LString.t) : C.t System.effect unit :=
  let! os := System.eval [LString.s "uname"; LString.s "-o"] in
  let! machine := System.eval [LString.s "uname"; LString.s "-m"] in
  match (os , machine) with
  | (Some (0%Z, os, _), Some (0%Z, machine, _)) =>
    do! System.log (LString.s "OS: " ++ LString.trim os) in
    System.log (LString.s "Machine: " ++ LString.trim machine)
  | _ => ret tt
  end.</pre>
          <p>We use the function <code>System.eval</code> to evaluate a command and get its status code and output. If the two <code>uname</code> calls are successful, we retrieve the OS and machine names and display them. The <code>0%Z</code> stands for the zero in the type <code>Z</code> of the relative integers. A null value means by convention that the commands were successful.</p>

          <h2 id="concurrency">Use concurrency</h2>
          <p>In order not to freeze, interactive programs usually need to run many IO operations in parallel. Consider for example an application which must keep a reactive user interface while doing slow network operations.</p>
          <p>To run two operations in parallel, we use the <code>join</code> operator:</p>
          <pre>join : C.t E A -> C.t E B -> C.t E (A * B)</pre>
          <p>with <code>join x y</code> concurrently computing the couple of results for the computations <code>x</code> and <code>y</code>.</p>
          <p>In the following program we concurrently run two sleep operations of 4 and 2 seconds:</p>
          <pre>(** Do two sleep operations. *)
Definition double_sleep (argv : list LString.t) : C.t System.effect unit :=
  let! _ : unit * unit :=
    join
      (let! _ := System.eval [LString.s "sleep"; LString.s "4"] in
      System.log (LString.s "Task of 4 seconds ended."))
      (let! _ := System.eval [LString.s "sleep"; LString.s "2"] in
      System.log (LString.s "Task of 2 seconds ended.")) in
  ret tt.</pre>
          <p>The output is:</p>
          <pre>Task of 2 seconds ended.
Task of 4 seconds ended.</pre>
          <p>and the total execution time is 4 seconds. If the sleeps were done sequentially:</p>
          <pre>(** Do two sleep operations (sequential). *)
Definition double_sleep_seq (argv : list LString.t) : C.t System.effect unit :=
  let! _ := System.eval [LString.s "sleep"; LString.s "4"] in
  do! System.log (LString.s "Task of 4 seconds ended.") in
  let! _ := System.eval [LString.s "sleep"; LString.s "2"] in
  System.log (LString.s "Task of 2 seconds ended.").</pre>
          <p>the execution time would be of 6 seconds and the output:</p>
          <pre>Task of 4 seconds ended.
Task of 2 seconds ended.</pre>

          <h2 id="effects">The effects system</h2>
          <p>What is the definition of a computation with IO and how does this work?</p>

          <h3>Effects</h3>
          <p>An effect describes a set of IO or impure operations. An effect is declared by an element of type <code>Effect.t</code>:</p>
          <pre>Module Effect.
  Record t := New {
    command : Type;
    answer : command -> Type }.
End Effect.</pre>
          <p>This record contains a type of <code>command</code>, a set of operations to communicate with the outer world, and a dependent type of <code>answer</code>, the type of answers given by the system to a command.</p>
          <p>For example, for an effect with <code>print</code> and <code>read_line</code> operations to communicate with the command-line, the declaration could be:</p>
          <pre>Inductive command : Type :=
| Print (message : LString.t)
| ReadLine.

Definition answer (c : command) : Type :=
  match c with
  | Print _ => unit
  | ReadLine => LString.t
  end.

Definition effect : Effect.t :=
  Effect.New command answer.</pre>
          <p>A command is a <code>Print message</code> or a <code>ReadLine</code>. The answer for a <code>Print</code> is of type <code>unit</code>, the answer for a <code>ReadLine</code> is of type <code>LString.t</code>. Notice that we only declare the effect, the definition of how to actually execute it is given latter during compilation. Most effects are declared this way, with a sum type for the command type. A composition of two effects is made up by combining their command sum types.</p>

          <h3>Computations</h3>
          <p>The computations are used to write programs with IO by assembling pure Coq expressions with external calls to the system. A computation returning a value of type <code>A</code> with the effect <code>E</code> lives in the inductive type <code>C.t E A</code>:</p>
          <pre>Module C.
  Inductive t (E : Effect.t) : Type -> Type :=
  | Ret : forall (A : Type) (x : A), t E A
  | Call : forall (command : Effect.command E), t E (Effect.answer E command)
  | Let : forall (A B : Type), t E A -> (A -> t E B) -> t E B
  | Choose : forall (A : Type), t E A -> t E A -> t E A
  | Join : forall (A B : Type), t E A -> t E B -> t E (A * B).
End C.</pre>
          <p>A computation can be:</p>
          <ul>
            <li><code>Ret e</code>: the pure expression <code>e</code>;</li>
            <li><code>Call c</code>: the call of the command <code>c</code>, waiting for an answer of type <code>answer c</code> from the system;</li>
            <li><code>Let e1 e2</code>: the sequential composition and binding of <code>e1</code> and <code>e2</code>. The term <code>e2</code> is a function, applied to the result of the computation <code>e1</code>. We used the notation <code>let! x := e1 in e2</code> for <code>Let e1 (fun x => e2)</code>;</li>
            <li><code>Choose e1 e2</code>: either <code>e1</code> or <code>e2</code>. The way the choice is made is not specified. In practice, it can be the first computation to terminate;</li>
            <li><code>Join e1 e2</code>: the couple of computations <code>e1</code> and <code>e2</code>, concurrently executed.</li>
          </ul>
          <p>As for the definition of <code>Effect.t</code>, this definition is abstract: nothing is said about the implementation of these five primitives till compilation. The main advantage is that we do not need to introduce any axioms to reason about IO.</p>
          <p>The <a href="https://www.haskell.org/">Haskell</a> user can recognize here the definition of a monad, with the <em>return</em> being the <code>Ret</code> and the <em>bind</em> being the <code>Let</code>:</p>
          <pre>Ret : A -> C.t E A
Let : C.t E A -> (A -> C.t E B) -> C.t E B</pre>
          <p>As you can see, it is possible to lift a pure expression of type <code>A</code> to a computation of type <code>C.t E A</code> with the <code>Ret</code> constructor, but it is impossible to do the reverse. The only way to access the result of a computation is by providing a function returning another computation, using the constructor <code>Let</code>. This corresponds to the intuition that a program containing a program with IO is also a program with IO, so the property of being with IO is hereditary.</p>

          <h3>Compilation</h3>
          <p>In order to be executed, the computations are compiled into OCaml programs with IO. This compilation is done by customizing the <a href="https://coq.inria.fr/refman/Reference-Manual025.html">extraction mechanism</a> used to compile pure Coq expressions to pure OCaml programs. The effects and computation primitives are extracted to explicit <a href="http://ocsigen.org/lwt/">Lwt</a> constructs. Lwt is a popular library for asynchronous IO in OCaml. This compilation phase is not formally verified.</p>

          <h2 id="use-cases">Verification by use cases</h2>
          <p>How to exploit the Coq system to verify our programs?</p>
          <p>A popular technique to specify interactive programs with a lot of IO is to define a set of <a href="https://en.wikipedia.org/wiki/Use_case">use cases</a>. Basically, a use case is a scenario of execution of the program, defined as a list of interaction steps between the program and its external world.</p>

          <h3>Use cases</h3>
          <p>Let us take the previous example of <code>your_name</code>:</p>
          <pre>(** Ask for the user name and answer hello. *)
Definition your_name (argv : list LString.t) : C.t System.effect unit :=
  do! System.log (LString.s "What is your name?") in
  let! name := System.read_line in
  match name with
  | None => ret tt
  | Some name => System.log (LString.s "Hello " ++ name ++ LString.s "!")
  end.</pre>
          <p>This program is very simple, but the techniques we will describe can apply to any program with IO, like a web application, a system script, ...</p>
          <p>A use case for a valid execution is:</p>
          <ul>
            <li>the program displays "What is your name?" on the terminal;</li>
            <li>the program asks to read a new line;</li>
            <li>the user answers by the string <em>name</em>;</li>
            <li>the program displays a message containing the string <em>name</em>.</li>
          </ul>
          <p>This use case is parametrized by a string <em>name</em>. To validate the use case, we could write a test program interacting with <code>your_name</code>, answering the <em>name</em> string to the <code>read_line</code> request and checking that the program outputs are as expected. The limitation of this method is that we can only test a finite number of <em>name</em> values, instead of all the possible strings.</p>

          <h3>Runs</h3>
          <p>To cover all the use case instances, <a href="http://coq.io/">Coq.io</a> introduces the notion of <em>run</em>. A run describes one execution of a computation, by programming the behavior of the computation's environment in a particular execution. Said otherwise, a run contains two programs: the computation itself and its environment, with typing rules ensuring that the environment answers to each request of the computation.</p>
          <p>A run is of type <code>Run.t e v</code>, where <code>e</code> is a computation and <code>v</code> is the expected result of the computation. We formally define the type <code>Run.t</code> by:</p>
          <pre>Module Run.
  Inductive t : forall {E : Effect.t} {A : Type}, C.t E A -> A -> Type :=
  | Ret : forall {E A} (x : A), t (C.Ret (E := E) A x) x
  | Call : forall E (c : Effect.command E) (answer : Effect.answer E c),
    t (C.Call (E := E) c) answer
  | Let : forall {E A B} {c_x : C.t E A} {x : A} {c_f : A -> C.t E B} {y : B},
    t c_x x -> t (c_f x) y -> t (C.Let A B c_x c_f) y
  | ChooseLeft : forall {E A} {c_x1 c_x2 : C.t E A} {x1 : A},
    t c_x1 x1 -> t (C.Choose A c_x1 c_x2) x1
  | ChooseRight : forall {E A} {c_x1 c_x2 : C.t E A} {x2 : A},
    t c_x2 x2 -> t (C.Choose A c_x1 c_x2) x2
  | Join : forall {E A B} {c_x : C.t E A} {x : A} {c_y : C.t E B} {y : B},
    t c_x x -> t c_y y -> t (C.Join A B c_x c_y) (x, y).
End Run.</pre>
          <p>Seemingly complex, this definition follows the one of the computations adding the definition of an environment. You do not need to read this definition carefully, you just need to get the intuition that:</p>
          <ul>
            <li>the run of <code>C.Ret e</code> is the computation <code>e</code> with an empty environment;</li>
            <li>the run of <code>C.Call c</code> is this call together with an environment given by an answer to this call;</li>
            <li>the run of <code>C.Let e1 e2</code> is a sequence of a run of <code>e1</code> and of a run of <code>e2</code>;</li>
            <li>the run of <code>C.Choose e1 e2</code> is either a run of <code>e1</code> or a run of <code>e2</code>;</li>
            <li>the run of <code>C.Join e1 e2</code> is the run of <code>e1</code> and a run of <code>e2</code>. Even if these two runs may actually interact, we are only interested in their projections on <code>e1</code> and <code>e2</code>.</li>
          </ul>
          <p>A use case can be formalized by a set of runs, with one run per instance of the use case. For our <code>your_name</code> example, we will define a set of runs <code>run_your_name_ok</code> parametrized by the variable <code>name</code> to formalize our use case.</p>

          <h3>A symbolic debugger</h3>
          <p>To give a run for a computation by directly writing its definition is quite cumbersome. Instead, we exploit the tactic mode of Coq to define a run by interacting with the computation like in a <em>debugger</em>. The breakpoints of this debugger are the constructors of the computation. By stepping through the beakpoints, you will provide a well-typed answer for each call of the computation.</p>
          <p>Let's start by declaring <code>run_your_name_ok</code>:</p>
          <pre>Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
  : Run.t (your_name argv) tt.</pre>
          <p>This run is parametrized by the program arguments <code>argv</code> and the user name <code>name</code>. This is a run of type <code>Run.t (your_name argv) tt</code>, running the program <code>your_name</code> with the parameters <code>argv</code> and expecting the unit value <code>tt</code> as a final answer. The Coq system answers us:</p>
          <pre>1 subgoals
argv : list LString.t
name : LString.t
______________________________________(1/1)
Run.t (your_name argv) tt</pre>
          <p>This means that we must define our run, and that we are at the beginning of the program <code>your_name</code>. This program starts with a <code>do! e1 in e2</code>, which corresponds to the constructor <code>C.Let</code> applied to <code>e1</code> and <code>fun _ => e2</code>. We step into this <code>C.Let</code> by applying the <code>Run.Let</code> constructor:</p>
          <pre>apply Run.Let.</pre>
          <p>but get an error:</p>
          <pre>Error: Cannot infer the implicit parameter x of Let.</pre>
          <p>Coq needs to know the expected result of the left-hand side of the <code>C.Let</code>. We know it must be <code>tt</code>, but we let Coq infer this value with <code>eapply</code>:</p>
          <pre>eapply Run.Let.</pre>
          <p>We get two subgoals, one for each side of the <code>C.Let</code>:</p>
          <pre>2 subgoal
argv : list LString.t
name : LString.t
______________________________________(1/2)
Run.t (log (LString.s "What is your name?")) ?29
______________________________________(2/2)
Run.t
  (let!name0 : option LString.t := read_line
   in match name0 with
      | Some name1 => log (LString.s "Hello " ++ name1 ++ LString.s "!")
      | None => ret tt
      end) tt</pre>
          <p>The library <a href="https://github.com/coq-io/system"><code>coq-io-system</code></a> provides a run <code>Run.log_ok</code> for the logging of a string <code>s</code>. This run executes the computation <code>System.log s</code> checking that the printed string is <code>s</code>. We apply this run:</p>
          <pre>apply (Run.log_ok (LString.s "What is your name?")).</pre>
          <p>and get one remaining goal:</p>
          <pre>1 subgoals
argv : list LString.t
name : LString.t
______________________________________(1/1)
Run.t
  (let!name0 : option LString.t := read_line
   in match name0 with
      | Some name1 => log (LString.s "Hello " ++ name1 ++ LString.s "!")
      | None => ret tt
      end) tt</pre>
          <p>Like for the <code>do!</code>, we step into the <code>let!</code> with a:</p>
          <pre>eapply Run.Let.</pre>
          <p>to get:</p>
          <pre>2 subgoal
argv : list LString.t
name : LString.t
______________________________________(1/2)
Run.t read_line ?38
______________________________________(2/2)
Run.t
  match ?38 with
  | Some name0 => log (LString.s "Hello " ++ name0 ++ LString.s "!")
  | None => ret tt
  end tt</pre>
          <p>The variable <code>?38</code>, the result of <code>read_line</code>, is unknown at this point. We run the <code>read_line</code> command by using the <code>Run.read_line_ok</code> run with the parameter <code>name</code> to answer the name of the user:</p>
          <pre>apply (Run.read_line_ok name).</pre>
          <p>We get:</p>
          <pre>1 subgoals
argv : list LString.t
name : LString.t
______________________________________(1/1)
Run.t
  match Some name with
  | Some name0 => log (LString.s "Hello " ++ name0 ++ LString.s "!")
  | None => ret tt
  end tt</pre>
          <p>The variable <code>?38</code> has been replaced by <code>Some name</code>. Once again, we use the run <code>Run.log_ok</code> to run a <code>System.log</code>:</p>
          <pre>apply (Run.log_ok (_ ++ name ++ _)).</pre>
          <p>The values of the underscores <code>_</code> are automatically inferred by Coq:</p>
          <pre>No more subgoals.</pre>
          <p>We conclude:</p>
          <pre>Defined.</pre>
          <p>The full definition of the run is then:</p>
          <pre>Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
  : Run.t (your_name argv) tt.
  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  eapply Run.Let. apply (Run.read_line_ok name).
  apply (Run.log_ok (_ ++ name ++ _)).
Defined.</pre>
          <p>This run is the Coq formalization of our use case for the valid executions of the computation <code>your_name</code>.</p>
          <p>As another example, here is the formalization of the use case in which the <code>System.read_line</code> command fails (because of a terminal error for instance):</p>
          <pre>Definition run_your_name_error (argv : list LString.t)
  : Run.t (your_name argv) tt.
  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  eapply Run.Let. apply Run.read_line_error.
  apply Run.Ret.
Defined.</pre>

          <h3>Validate a use case</h3>
          <p>Once a use case has been formalized, we would like to formally verify it. There is actually... nothing to do, because we know that our runs must be valid since they are well-typed. If we have tried to define an invalid run like:</p>
          <pre>Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
  : Run.t (your_name argv) tt.
  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name? blabla#@!"))
  eapply Run.Let. apply (Run.read_line_ok name).
  apply (Run.log_ok (_ ++ name ++ _)).
Defined.</pre>
          <p>we would have gotten an error at definition time:</p>
          <pre>Error: Impossible to unify
 "Run.t (log (LString.s "What is your name? blabla#@!")) tt" with
 "Run.t (log (LString.s "What is your name?")) ?29".</pre>

          <div id="disqus_thread"></div>
          <script type="text/javascript">
              /* * * CONFIGURATION VARIABLES * * */
              var disqus_shortname = 'coq-io';

              /* * * DON'T EDIT BELOW THIS LINE * * */
              (function() {
                  var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true;
                  dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js';
                  (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq);
              })();
          </script>
          <noscript>Please enable JavaScript to view the <a href="https://disqus.com/?ref_noscript" rel="nofollow">comments powered by Disqus.</a></noscript>
        </div>
      </div>
<%= footer %>