shttpd/coq/S/Lucid/Arrow.v

(* Copyright © 2019 Ariadne Devos
   SPDX-License-Identifier: GPL-2.0 or GPL-3.0 *)

Require Import Coq.Classes.Equivalence.
Require Import Coq.Relations.Relations.

(* Arrows are generalisations of functions.
   They can be composed like functions, but
   are looser. They may have certain side-effects,
   or be reversible.

   A few different arrows are used in S²:
   Gallina functions, Gallina functions over
   subset types abstracted over their predicate,
   stateful arrows, the pre- post- and frame-
   conditions of stateful arrows. *)

(* Define concepts by formulating rewrite rules *)

(* First, very general. Sequential and parallel composition,
   with possibly arbitrary limitations on data values and
   no lifting from Gallina functions. These restrictions
   may be useful for reification. The semantics of parallel
   composition are intentionally left mostly undefined. *)

Record arrow_info := {
  (* D: the set of data types *)
  D : Type;
  (* D2: the product of two data types *)
  D2 : D -> D -> D;
  (* the arrow type, from an input to an output. *)
  Arr : D -> D -> Type;
}.

(* Operations common to all arrows.

   Note that data values cannot be reordered, cloned or deleted.
   This may be important performance-wise in some applications
   (e.g. array values, quantum computing, reversible computing).

   Also note that there is no lifting funtion from Gallina
   to Arr i. This is because one might to reason by reification,
   or extract or manipulate a program to let it run on bare
   software. If lifting is allowable, see `arrow_lift_ops`.

   Another difference from Haskell: the parallel composition
   operator, might, in fact, be parallel (including interleaving).
   Or it might just always be in a particular order. *)
Record arrow_ops (i : arrow_info) := {
  (* the identity, do-nothing arrow *)
  idA : forall A, Arr i A A;
  (* reassociate data values (1) *)
  assocA_r : forall A B C, Arr i (D2 i (D2 i A B) C) (D2 i A (D2 i B C));
  (* reassociate data values (2) *)
  assocA_l : forall A B C, Arr i (D2 i A (D2 i B C)) (D2 i (D2 i A B) C);
  (* sequential composition *)
  seqA : forall A B C, Arr i A B -> Arr i B C -> Arr i A C;
  (* parallel composition,
     not necessarily executed in any particular order
     (possibly even interleaved) *)
  parA : forall A B C D, Arr i A B -> Arr i C D -> Arr i (D2 i A C) (D2 i B D);
  (* are two arrows considered equivalent? *)
  eqvA : forall A B, relation (Arr i A B);
}.

Arguments idA { _ } a { _ }.
Arguments assocA_r { _ } a A B C.
Arguments assocA_l { _ } a A B C.
Arguments seqA { _ } a { _ _ _ }.
Arguments parA { _ } a { _ _ _ _ }.
Arguments eqvA { _ } a { _ _ }.

Record arrow_lawful i o := {
  (* the equivalence relation is, in fact, an equivalence *)
  equivA : forall A B, Equivalence (eqvA (i := i) o (A := A) (B := B));
  (* the reassociations cancel each other *)
  seqA_assocA_rl : forall A B C, eqvA o (seqA o (assocA_r o A B C) (assocA_l o A B C)) (idA o);
  seqA_assocA_lr : forall A B C, eqvA o (seqA o (assocA_l o A B C) (assocA_r o A B C)) (idA o);
  (* TODO: monoid laws *)
  (* the identity arrow can be deleted from the left in case of sequential composition *)
  seqA_idA_l : forall A B (k : Arr i A B), eqvA o (seqA o (idA o) k) k;
  seqA_idA_r : forall A B (k : Arr i A B), eqvA o (seqA o k (idA o)) k;
  (* sequential composition is associative *)
  seqA_assoc : forall A B C D (k : Arr i A B) (l : Arr i B C) (m : Arr i C D),
    eqvA o (seqA o (seqA o k l) m) (seqA o k (seqA o l m));
  (* there are no rules for parallel composition in
     the general case *)
}.

Arguments equivA { _ _ } a _ _.

Record arrow_basic := {
  basicA_info : arrow_info;
  basicA_ops : arrow_ops basicA_info;
  basicA_laws : arrow_lawful basicA_info basicA_ops
}.

Coercion basicA_info : arrow_basic >-> arrow_info.
Coercion basicA_ops : arrow_basic >-> arrow_ops.
Coercion basicA_laws : arrow_basic >-> arrow_lawful.

(* Sequence three arrows *)
Definition seqA3 (i : arrow_basic) A B C D (x : Arr i A B) (y : Arr i B C) (z : Arr i C D) : Arr i A D
  := seqA i x (seqA i y z).
Arguments seqA3 _ { _ _ _ _ }.