Sync with unshared/manuscripts/2020.exteqaxiom before submission.

2020.Extensional equality preservation and verified generic programming/About.lidr

@@ -106,7 +106,7 @@ The proof uses pattern matching, which is straightforward here because
 %endif
 %
 In a similar way, one can prove that |(=)| is an equivalence relation:
-Reflexivity is directly implemented by |Refl|, while symmetry and
+reflexivity is directly implemented by |Refl|, while symmetry and
 transitivity can be proven by pattern matching.
 
 
@@ -160,9 +160,10 @@ but not the converse, normally referred to as \emph{function extensionality}:
 
 When working with functions, extensional equality is often the notion of
 interest and libraries of formalized mathematics typically provide
-definitions like |<=>| and basic results like |IEqImplEE|, see for
-example |homot| and |eqtohomot| in Part A of the UniMath library \citep{UniMath}
-or |eqfun| in Coq \citep{CoqProofAssistant}.
+definitions like |<=>| and basic results like |IEqImplEE|.
+%
+See for example |homot| and |eqtohomot| in Part A of the UniMath
+library \citep{UniMath} or |eqfun| in Coq \citep{CoqProofAssistant}.
 
 In reasoning about generic programs in the style of the Algebra of
 Programming \citep{DBLP:books/daglib/0096998,mu2009algebra} and, more
@@ -200,7 +201,7 @@ two-argument version of extensional equality preservation:
 
 > compPresEE  :  {A, B, C : Type} -> {g, g' : B -> C} -> {f, f' : A -> B} ->
 >                g <=> g' -> f <=> f' -> g . f <=> g' . f'
-> compPresEE {g} {g'} {f} {f'} gExtEq fExtEq x  =
+> compPresEE {g} {g'} {f} {f'} gExtEq {-"\ "-} fExtEq {-"\ "-} x  =
 >    (  (g . f) x    )  ={ Refl }=
 >    (  g (f x)      )  ={ cong (fExtEq x) }=
 >    (  g (f' x)     )  ={ gExtEq (f' x) }=
@@ -209,8 +210,8 @@ two-argument version of extensional equality preservation:
 
 The right hand side is a chain of equal expressions connected by the
 |={| proofs |}=| of the individual steps within special braces and
-ending in |QED|, see ``Preorder reasoning'' in
-\citep{idrisdocs}.
+ending in |QED|, see ``Preorder reasoning'' in the documentation by
+\citet{idrisdocs}.
 %
 The steps with |Refl| are just for human readability, they could be
 omitted as far as Idris is concerned.
@@ -243,10 +244,10 @@ This paper is also about ADTs and generic programming.
 %
 More specifically, we show how to exploit the notion of extensional
 equality preservation to inform the design of ADTs for generic
-programming and embedded domain-specific languages (DSL).
+programming and embedded domain-specific languages (DSLs).
 %
 This is exemplified in sections \ref{section:functors} and
-\ref{section:monads} for ADTs for functors and monads but we conjecture
+\ref{section:monads} with ADTs for functors and monads but we conjecture
 that other abstract data types, e.g. for applicatives and arrows, could
 also profit from a design informed by the notion of preservation of
 extensional equality.
@@ -285,8 +286,8 @@ of important research for the last thirty years.
 Since Hofmann's seminal work \citep{hofmann1995extensional}, setoids
 have been the established, but also often dreaded (who coined the
 expression \emph{``setoid hell''}?)  means to deal with extensional
-concepts in intensional type theory, see also section
-\ref{section:relatedwork}.
+concepts in intensional type theory (see also section
+\ref{section:relatedwork}).
 %
 Eventually, the study of Martin-Löf's equality type has lead to the
 development of Homotopy Type Theory and Voevodsky's Univalent
@@ -326,11 +327,11 @@ These can be type-checked with Idris 1.3.2 and are available at
 %, see \texttt{README.md} in the paper's folder.
 
 %
-In the next section we present a motivating example from monadic
-dynamical systems, in section~\ref{section:functors} we explore
-extensional equality preservation for functors and in section
-\ref{section:monads} for monads.
-%
-We continue with dynamical systems applications in section~\ref{section:applications}
-and finish with related work (section~\ref{section:relatedwork}) and
-conclusions (section~\ref{section:conclusions}).
+% In the next section we present a motivating example from monadic
+% dynamical systems, in section~\ref{section:functors} we explore
+% extensional equality preservation for functors and in section
+% \ref{section:monads} for monads.
+% %
+% We continue with dynamical systems applications in section~\ref{section:applications}
+% and finish with related work (section~\ref{section:relatedwork}) and
+% conclusions (section~\ref{section:conclusions}).

2020.Extensional equality preservation and verified generic programming/Applications.lidr

@@ -141,6 +141,7 @@ As for |flowLemma2|, proving the representation lemma is straightforward
 but crucially relies on associativity of Kleisli composition and thus, as
 seen in section \ref{section:monads}, on preservation of extensional
 equality:
+\pagebreak
 
 % > reprLemma f Z mx =
 % >   ( (repr (flow f Z))    mx )  ={ Refl }=
@@ -150,7 +151,7 @@ equality:
 % >   ( flowDet (repr f) Z   mx )  QED
 
 > reprLemma f Z      mx = Fat.pureRightIdKleisli id mx
-
+>
 > reprLemma f (S m)  mx =
 >   ( repr (flow f (S m)) mx )               ={ Refl }=
 >   ( (id >=> flow f (S m)) mx )             ={ Refl }=
@@ -166,11 +167,11 @@ Notice also the application of |kleisliLeapfrog| to deduce |(id >=>
 flow f m) ((id >=> f) mx)| from |((id >=> f) >=> flow f m) mx|.
 %
 If we had formulated the theory in terms of bind instead of Kleisli
-composition, the two expressions would be intensionally equal.
+composition, the two expressions would have been intensionally equal.
 
 \paragraph*{Flows and trajectories.}
 %
-The last application of preservation of extensional
+Our last application of preservation of extensional
 equality in the context of dynamical systems theory is a result about
 flows and trajectories.
 %
@@ -188,7 +189,7 @@ is an |M|-structure containing just |[x]|.
 To compute the trajectories for |S n| steps, we first bind the outcome
 of a single step |f x : M X| into |trj f n|.
 %
-This results in an |M|-structure of vectors of length |S n|.
+This results in an |M|-structure of vectors of length |n|.
 %
 Finally, we prepend these possible trajectories with the initial state
 |x|.
@@ -284,4 +285,4 @@ induction.
 %
 As in the |flowTrjLemma| discussed above, |map| preserving extensional
 equality turns out to be pivotal in applying the induction hypothesis,
-see \citep{brede2020} for details.
+see \citet{brede2020} for details.

2020.Extensional equality preservation and verified generic programming/Conclusions.lidr

@@ -12,7 +12,7 @@
 \label{section:conclusions}
 
 In dependently typed programming in the context of Martin-Löf type
-theories \citep{nordstrom1990programming, martinlof1984}, the problem of
+theories \citep{martinlof1984, nordstrom1990programming}, the problem of
 how to specify abstract data types for verified generic programming is
 still not well understood.
 %

2020.Extensional equality preservation and verified generic programming/Example.lidr

@@ -81,17 +81,16 @@ With |compPresIE| from section~\ref{section:about}, one can implement
 %
 The base case is trivial
 
-> flowLemma f Z = Refl
+> flowLemma f     Z     =  Refl
 
 For readability, we spell out the proof sketch for the induction step in
 full:
 
-> flowLemma f  (  S n)  =
->   ( flowL f (S n) )     ={ Refl }=
->   ( flowL f n . f )     ={ compPresIE (flowLemma f n) Refl }=
->   ( flowR f n . f )     ={ flowRLemma f n }=
->   ( f . flowR f n )     ={ Refl }=
->   ( flowR f (S n) )     QED
+> flowLemma f  (  S n)  =  ( flowL f (S n) )     ={ Refl }=
+>                          ( flowL f n . f )     ={ compPresIE (flowLemma f n) Refl }=
+>                          ( flowR f n . f )     ={ flowRLemma f n }=
+>                          ( f . flowR f n )     ={ Refl }=
+>                          ( flowR f (S n) )     QED
 
 First, we apply the definition of |flowL| to deduce |flowL f (S n) =
 flowL f n . f|.
@@ -109,15 +108,22 @@ associativity and preservation of intensional equality again.
 
 < flowRLemma : {X : Type} -> (f : X -> X) -> (n : Nat) -> flowR f n . f = f . flowR f n
 
-> flowRLemma f     Z     =          Refl
-> flowRLemma f  (  S n)  =
->   ( flowR f (S n) . f )       ={  Refl }=
->   ( (f . flowR f n) . f )     ={  compAssociative f (flowR f n) f }=
->   ( f . (flowR f n . f) )     ={  compPresIE Refl (flowRLemma f n) }=
->   ( f . (f . flowR f n) )     ={  Refl }=
->   ( f . flowR f (S n) )       QED
+> flowRLemma f     Z     =  Refl
+> flowRLemma f  (  S n)  =  ( flowR f (S n) . f )       ={  Refl }=
+>                           ( (f . flowR f n) . f )     ={  compAssociative f (flowR f n) f }=
+>                           ( f . (flowR f n . f) )     ={  compPresIE Refl (flowRLemma f n) }=
+>                           ( f . (f . flowR f n) )     ={  Refl }=
+>                           ( f . flowR f (S n) )       QED
 
 \end{joincode}
+% > flowRLemma f     Z     =          Refl
+% > flowRLemma f  (  S n)  =
+% >   ( flowR f (S n) . f )       ={  Refl }=
+% >   ( (f . flowR f n) . f )     ={  compAssociative f (flowR f n) f }=
+% >   ( f . (flowR f n . f) )     ={  compPresIE Refl (flowRLemma f n) }=
+% >   ( f . (f . flowR f n) )     ={  Refl }=
+% >   ( f . flowR f (S n) )       QED
+%
 
 \noindent
 Let's summarize: we have considered the special case of deterministic
@@ -152,18 +158,15 @@ on a set |X| are functions of type |X -> M X| where |M| is a monad.
 %
 When |M| is the identity monad, one recovers the deterministic case.
 %
-%%For |M| equal to |List| one has non-deterministic systems and |M| equal
-%%to the finite probability distribution monads |Dist|
-%%\citep{10.1017/S0956796805005721} or |SimpleProb|
-%%\citep{2017_Botta_Jansson_Ionescu} formalizes the notion of stochastic
-%%systems.
 When |M| is |List| one has non-deterministic systems, and finite
-probability monads (e.g. |Dist| \citep{10.1017/S0956796805005721} or
-|SimpleProb| \citep{ionescu2009, 2017_Botta_Jansson_Ionescu}) capture the notion of
-stochastic systems.
+probability monads
+%*TODO: perhaps cite (e.g. |Dist| \citep{10.1017/S0956796805005721} or |SimpleProb| \citep{ionescu2009, 2017_Botta_Jansson_Ionescu})
+capture the notion of stochastic systems.
+%
+\nocite{10.1017/S0956796805005721,ionescu2009, 2017_Botta_Jansson_Ionescu}
 %
-Other monads encode other notions of uncertainty, see
-\citep{ionescu2009,giry1981}.
+%Other monads encode other notions of uncertainty, see \citep{ionescu2009,giry1981}.
+\nocite{ionescu2009,giry1981}
 
 One can extend the flow (and, as we will see in
 section~\ref{section:applications}, other elementary operations) of
@@ -171,15 +174,15 @@ deterministic systems to the general, monadic case by replacing |id|
 with |pure| and function composition with Kleisli composition (|>=>|):
 %PJ: The repeated type signature is a bit disturbing. Perhaps use |using|?
 
-> flowMonL :  {X : Type} -> {M : Type -> Type} -> Monad M =>
->             (X -> M X) -> Nat -> (X -> M X)
-> flowMonL f     Z     =  pure
-> flowMonL f  (  S n)  =  flowMonL f n >=> f
+> flowMonL  :  {X : Type} -> {M : Type -> Type} -> Monad M =>
+>              (X -> M X) -> Nat -> (X -> M X)
+> flowMonL {-"\,"-}  f     Z     =  pure
+> flowMonL           f  (  S n)  =  flowMonL f n >=> f
 >
-> flowMonR :  {X : Type} -> {M : Type -> Type} -> Monad M =>
->             (X -> M X) -> Nat -> (X -> M X)
-> flowMonR f     Z     =  pure
-> flowMonR f  (  S n)  =  f >=> flowMonR f n
+> flowMonR  :  {X : Type} -> {M : Type -> Type} -> Monad M =>
+>              (X -> M X) -> Nat -> (X -> M X)
+> flowMonR           f     Z     =  pure
+> flowMonR           f  (  S n)  =  f >=> flowMonR f n
 
 Notice, however, that now the implementations of |flowMonL| and
 |flowMonR| depend on |(>=>)|, which is a monad-specific operation.
@@ -193,11 +196,12 @@ What do we know about Kleisli composition \emph{in general}?
 %
 We discuss this question in the next two sections but let us
 anticipate that, if we require functors to preserve the extensional
-equality of arrows (in addition to identity and composition)
-and Kleisli composition to fulfil the specification
-
+equality of arrows (in addition to identity and composition) and
+Kleisli composition to fulfil the specification
+%
+\vspace*{-2ex}
 \begin{center}
-\begin{tikzcd}[row sep=large, column sep=large]
+\begin{tikzcd}[column sep=large]
   |M C|
 & |M (M C)|  \arrow[l, "|join|"]
 & |M B|      \arrow[l, "|map g|"]
@@ -210,20 +214,6 @@ and Kleisli composition to fulfil the specification
 > kleisliSpec  :  {A, B, C : Type} -> {M : Type -> Type} -> Monad M =>
 >                 (f : A -> M B) -> (g : B -> M C) -> (f >=> g) <=> join . map g . f
 
-% \begin{minipage}{0.4\textwidth}
-% \begin{tikzcd}[row sep=large, column sep=large]
-% |A|    \arrow[r, "|f|"] \arrow[d, "|f>=>g|"] & |M B| \arrow[d, "|map g|"] \\
-% |M C|                                        & |M (M C)| \arrow[l, "|join|"]
-% \end{tikzcd}
-% \end{minipage}
-%
-% \begin{tikzcd}[row sep=large, column sep=large]
-%   |A|       \arrow[r, "|f|"] \arrow[rrr, bend left=30, "|f>=>g|"]
-% & |M B|     \arrow[r, "|map g|"]
-% & |M (M C)| \arrow[r, "|join|"]
-% & |M C|
-% \end{tikzcd}
-%
 then we can derive preservation of extensional equality
 
 > kleisliPresEE  :  {A, B, C : Type} -> {M : Type -> Type} -> Monad M =>
@@ -240,8 +230,8 @@ From these premises, we can prove the \emph{extensional} equality of
 |flowMonL| and |flowMonR| using a similar lemma as in the deterministic case:
 %
 
-> flowMonRLemma  :  {X : Type} -> {M : Type -> Type} -> Monad M =>
->                   (f : X -> M X) -> (n : Nat) -> (flowMonR f n >=> f) <=> (f >=> flowMonR f n)
+> flowMonRLem  :  {X : Type} -> {M : Type -> Type} -> Monad M =>
+>                 (f : X -> M X) -> (n : Nat) -> (flowMonR f n >=> f) <=> (f >=> flowMonR f n)
 
 First, notice that the base case of the lemma requires computing
 evidence that |pure >=> f| is extensionally equal to |f >=> pure|.
@@ -262,7 +252,7 @@ Kleisli composition: for |f : A -> M B| we have
 
 %endif
 
-> flowMonRLemma f Z x =
+> flowMonRLem f Z x =
 >   ( (flowMonR f Z >=> f) x )    ={ Refl }=
 >   ( (pure >=> f) x )            ={ pureLeftIdKleisli f x }=
 >   ( f x )                       ={ sym (pureRightIdKleisli f x) }=
@@ -273,15 +263,15 @@ As we will see in subsection \ref{def:pureLeftIdKleisli},
 |pureLeftIdKleisli| and |pureRightIdKleisli| are either ADT axioms or
 theorems, depending of the formulation of the monad ADT.
 %
-The induction step of |flowMonRLemma| relies on preservation of
+The induction step of |flowMonRLem| relies on preservation of
 extensional equality and on associativity of Kleisli composition:
 
-> flowMonRLemma f  (  S n) x =
+> flowMonRLem f  (  S n) x =
 >  let rest = flowMonR f n in
 >   ( (flowMonR f (S n) >=> f) x )      ={ Refl }=
 >   ( ((f >=> rest) >=> f) x )          ={ kleisliAssoc f rest f x }=
 >   ( (f >=> (rest >=> f)) x )          ={ kleisliPresEE  f f            (rest >=> f) (f >=> rest)
->                                                         (\ v => Refl)  (flowMonRLemma f n) x     }=
+>                                                         (\ v => Refl)  (flowMonRLem f n) x     }=
 >   ( (f >=> (f >=> rest)) x )          ={ Refl }=
 >   ( (f >=> flowMonR f (S n)) x )      QED
 
@@ -293,16 +283,16 @@ Finally, the extensional equality of |flowMonL| and |flowMonR|
 > flowMonLemma f Z x = Refl
 >
 > flowMonLemma f (S n) x =
->  let  fLn = flowMonL f n
->       fRn = flowMonR f n in
+>  let  fLn  = flowMonL  f n
+>       fRn  = flowMonR  f n  in
 >   ( flowMonL f (S n) x )       ={ Refl }=
 >   ( (fLn >=> f) x )            ={ kleisliPresEE  fLn fRn             f f
 >                                                  (flowMonLemma f n)  (\v => Refl) x }=
->   ( (fRn >=> f) x )            ={ flowMonRLemma f n x }=
+>   ( (fRn >=> f) x )            ={ flowMonRLem f n x }=
 >   ( (f >=> fRn) x )            ={ Refl }=
 >   ( flowMonR f (S n) x )       QED
 
-follows from |flowMonRLemma| and, again, preservation of extensional equality.
+follows from |flowMonRLem| and, again, preservation of extensional equality.
 
 \paragraph*{Discussion.} Before we turn to the next section, let us discuss one
 objection to what we have just done.
@@ -326,8 +316,9 @@ these would make our monad interface impossible (or at least very
 hard) to implement.
 %
 In general, we cannot rely on |f >=> g| to be intensionally equal to
-|join . map g . f| (or, for that matter, to be intensionally equal to
-|\a => f a >>= g|).
+|join . map g . f|.
+% we haven't introduced bind yet...
+%(or, for that matter, to be intensionally equal to |\a => f a >>= g|).
 
 In designing ADTs and formulating generic results, we have to be careful
 not to impose too strong proof obligations on implementors.

2020.Extensional equality preservation and verified generic programming/Functors.lidr

@@ -32,7 +32,7 @@ $\mathcal{D}$ (often both denoted by |F|) such that for each arrow |f
 : A -> B| in $\mathcal{C}$ there is an arrow |F f : F A -> F B| in
 $\mathcal{D}$.
 %
-For an introduction to category theory, see \citep{pierce_basic_1991}.
+For an introduction to category theory, see \citet{pierce_basic_1991}.
 %
 The arrow map preserves identity arrows and arrow composition.
 %
@@ -172,26 +172,24 @@ proof looks as follows:
 %  {-" below=\the\belowdisplayskip"-}
 
 > mapListPresEE :  {A, B : Type} -> (f, g : A -> B) -> f <=> g -> mapList f <=> mapList g
-> mapListPresEE f g fEEg [] = Refl
-> mapListPresEE f g fEEg (a :: as) =
->   ( mapList f (a :: as) )          ={ Refl }=
->   ( f a :: mapList f as )          ={ cong {f = (::{-"~"-} mapList f as)} (fEEg a) }=
->   ( g a :: mapList f as )          ={ cong (mapListPresEE f g fEEg as) }=
->   ( g a :: mapList g as )          ={ Refl }=
->   ( mapList g (a :: as) )          QED
+> mapListPresEE f g fEEg []         =      Refl
+> mapListPresEE f g fEEg (a :: as)  =  {-"\,"-}
+>   ( mapList f (a :: as) )            ={  Refl }=
+>   ( f a :: mapList f as )            ={  cong {f = (::{-"~"-} mapList f as)} (fEEg a) }=
+>   ( g a :: mapList f as )            ={  cong (mapListPresEE f g fEEg as) }=
+>   ( g a :: mapList g as )            ={  Refl }=
+>   ( mapList g (a :: as) )            QED
 
 In general the proofs have a very simple structure: they use the |f
-<=> g| arguments to transform the arguments of type |A| expected by
-the constructors into arguments of type |B|, and otherwise only use
-the induction hypotheses.
+<=> g| arguments at the ``leaves'', and otherwise only use the
+induction hypotheses.
 %
-They can also be written as dependent folds, but this results in less
-readable proofs.
+%They can also be written as dependent folds, but this results in less
+%readable proofs.
 %
-(With a suitable universe of codes for types, or a library for
+With a suitable universe of codes for types, or a library for
 parametricity proofs, these proofs can be automated using
-datatype-generic programming.)
-%
+datatype-generic programming.
 
 %if False
 We can write |mapListPresEE| in a more condensed form using Idris'
@@ -240,13 +238,13 @@ This is a common pattern for proofs of |mapPresEE|.
 %endif
 
 Let's now turn to a type constructor that is not an instance of
-|VeriFunctor|, namely |Reader E| for some environment |E : Type|.
+our |VeriFunctor|, namely |Reader E| for some environment |E : Type|.
 
 > Reader : Type -> Type -> Type
 > Reader E A = E -> A
 >
-> mapReader : {A, B, E : Type} -> (A -> B) -> Reader E A -> Reader E B
-> mapReader f r = f . r
+> mapR : {A, B, E : Type} -> (A -> B) -> (Reader E A -> Reader E B)
+> mapR f r = f . r
 
 If we try to implement preservation of extensional equality we end up with
 
@@ -258,18 +256,17 @@ If we try to implement preservation of extensional equality we end up with
 
 %endif
 
-> mapReaderPresEE :  {A, B : Type} -> (f, g : A -> B) ->
->                    f <=> g -> mapReader f <=> mapReader g
-> mapReaderPresEE f g fEEg r  =
->   ( mapReader f r)        ={ Refl }=
+> mapRPresEE :  {A, B : Type} -> (f, g : A -> B) -> f <=> g -> mapR f <=> mapR g
+> mapRPresEE f g fEEg r  =
+>   ( mapR f r)             ={ Refl }=
 >   ( f . r )               ={ whatnow1 r }=     -- here we need |f = g| to proceed
 >   ( g . r )               ={ Refl }=
->   ( mapReader g r)        QED
+>   ( mapR g r)             QED
 
 Notice the question mark in front of |whatnow1r|. This introduces an
 unresolved proof step and allows us to ask Idris to help us implementing
 this step, see ``Elaborator Reflection -- Holes'' in \citep{idrisdocs}.
-Among others, we can ask about the
+Among other things, we can ask about the
 type of |whatnow1r|. Perhaps not surprisingly, this turns out to be |f
 . r = g . r|.
 
@@ -278,9 +275,6 @@ all |e : E|, we cannot deduce |f . r = g . r| without extensionality.
 %
 Thus |Reader E| does not implement the |VeriFunctor| interface, but it
 is ``very close''.
-%
-\footnote{By a similar argument, |mapPresEE| does not hold for the
-  continuation monad.}
 %if False
 
 > (<==>) : {A, B, C : Type} -> (f, g : A -> B -> C) -> Type
@@ -290,13 +284,16 @@ is ``very close''.