Commit a33c0e8f authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 0ed2486b
% -*-Latex-*-
%if False
> module About
> import Syntax.PreorderReasoning
import LexerFriendlyReasoning -- not yet working as intended
> infix 6 <=>
> %default total
> %auto_implicits off
> %access public export
> Domain : {A, B : Type} -> (A -> B) -> Type
> Domain {A} f = A
%endif
\section{Introduction}
\label{section:about}
This paper is about \emph{extensional equality preservation} in
dependently typed languages like Idris~\citep{idrisbook}, % idristutorial,
Agda~\citep{norell2007thesis} and Coq~\citep{CoqProofAssistant_8_11} that
implement %some version of
Martin-Löf's intensional type
theory \citep{martinlof1984}. % , nordstrom1990programming
%
%% We present our arguments in Idris but the results can be translated to
%% other implementations easily.
We discuss Idris code but the results could be translated to other
languages.
%
Extensional equality is a property of functions, stating that they are
``pointwise equal'':
%
%In Idris, it can be expressed as
%TR: Unfortunately doesn't typecheck without {A} ...
> (<=>) : {A, B : Type} -> (A -> B) -> (A -> B) -> Type
> (<=>) {A} f g = (x : A) -> f x = g x
Note that the definition of extensional equality |(<=>)| depends on another equality |(=)|.
%*PJ: Perhaps remark that it can be defined for dependent functions as well.
% In Agda: (formulation from \citep{DBLP:journals/jfp/AbelCDTW20})
% postulate ext : ∀ {l l'} {A : Set l} {B : A → Set l'} {f g : (a : A) → B a} →
% (∀ (a : A) → f a ≡ g a) → f ≡ g
% ext follows from univalence and can be used in type theories that assume UIP (uniqueness of identity proofs)
\paragraph*{Different flavours of equality.}%\hfill
%
\begin{quote}
``All animals are equal, but some animals are more equal than others'' [Animal Farm, Orwell (1946)]
\end{quote}
There are several kinds of ``equality'' relevant for programming.
%
%{
%format -> = "\rightarrow"
Programming languages usually offer a Boolean equality check operator and in Idris it is written |(==)|, has type |{A : Type} -> Eq A => A -> A -> Bool| and is packaged in the interface |Eq|.
%}
%
This is an ``ad-hoc'' equality, computing whatever the programmer supplies as an implementation.
%
This paper is not about value level Boolean equality.
On the type level, the dependently typed languages we consider in this paper provide
a notion of \emph{intensional equality}, also referred to as an ``equality type'',
which is an inductively defined family of types, usually written infix: |(a=b) : Type| for |a:A| and |b:B|. It has
just one constructor |Refl : a=a|.
%
The resulting notion is not as boring as it may look at first. We have |Refl:a=b| not only if |a| and |b| are identical, but
also if they \emph{reduce} to identical expressions. Builtin reduction rules normally include alpha-conversion (capture-free
renaming of bound variables), beta-reduction (using substitution) and eta-reduction: |f = \x=>f x|.
%
So, for example, we have |Refl: id x = x|.
%
Furthermore, user-defined equations are also used for reduction.
%
A typical example is addition of natural numbers: with |+| defined by pattern matching on the first argument, we have e.g.
|Refl:1+1=2|. However, while for a variable |n:Nat| we have |Refl : 0+n = n|, we do not have |Refl: n+0=n|.
One very useful property of intensional equality is that it is a congruence with respect to any function.
%
In other words, all functions preserve intensional equality.
%
The proof uses pattern matching, which is straightforward here because
|Refl| is the only constructor:
%
< cong : {A, B : Type} -> {f : A -> B} -> {a, a' : A} -> a = a' -> f a = f a'
< cong Refl = Refl
%if False
> checkClaim : (n : Nat) -> 0+n = n
> checkClaim n = Refl
< failClaim : (n : Nat) -> n+0 = n
< failClaim n = Refl
%endif
%
In a similar way, one can prove that |(=)| is an equivalence relation:
Reflexivity is directly implemented by |Refl|, while symmetry and
transitivity can be proven by pattern matching.
\paragraph*{Extensional equality.}
As one would expect, extensional equality is an equivalence relation
> reflEE : {A, B : Type} -> {f : A -> B} -> f <=> f
> symEE : {A, B : Type} -> {f, g : A -> B} -> f <=> g -> g <=> f
> transEE : {A, B : Type} -> {f, g, h : A -> B} -> f <=> g -> g <=> h -> f <=> h
>
> reflEE = \x => Refl
> symEE p = \x => sym (p x)
> transEE p q = \x => trans (p x) (q x)
In general, we can lift any (type-valued) binary relation on a type
|B| to a binary relation on function types with co-domain |B|.
%
% \REMARK{Nicola}{As the type of |extify| is now |BinRel B -> BinRel
% (A -> B)|, the name of the function and the name |eqB| in its
% implementation are perhaps not appropriate? |BinRel| also should
% perhaps be called |EndoRel|? Or just |Rel : Type -> Type -> Type| with
% |Rel A B = A -> B -> Type| and then |extify : Rel B B -> Rel (A -> B)
% (A -> B)|? Perhaps we can get rid of |BinRel| altogether (it is not
% used in the rest of the paper) and simply write |extify : {A, B :
% Type} -> (B -> B -> Type) -> ((A -> B) -> (A -> B) -> Type|? I am
% surprised that |extify| can be applied to |(=) : A -> B -> Type|!}
> extify : {A, B : Type} -> (B->B->Type) -> ((A->B)->(A->B)->Type)
> extify {A} relB f g = (a : A) -> relB (f a) (g a)
The |extify| combinator maps equivalence relations to equivalence relations.
%
Using it we can redefine |(<=>) = extify (=)| and we can easily continue to quantify
over more arguments: |(<==>) = extify (<=>)|, etc.
%
In this paper our main focus is equality on functions, and we will explore in some detail the relationship between |f=g| and |f<=>g|.
%
In Martin-Löf's intensional type theory, and thus in Idris,
extensional equality is strictly weaker than intensional equality.
%
More concretely, we can implement
> IEqImplEE : {A, B : Type} -> (f, g : A -> B) -> f = g -> f <=> g
> IEqImplEE f f Refl = \ x => Refl
but not the converse, normally referred to as \emph{function extensionality}:
> EEqImplIE : {A, B : Type} -> (f, g : A -> B) -> f <=> g -> f = g -- not implementable
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 \citep{UniMath}
foundations or |eqfun| in Coq \citep{CoqProofAssistant_8_11}.
In reasoning about generic programs in the style of the Algebra of
Programming \citep{DBLP:books/daglib/0096998,mu2009algebra} and, more
generally, in pen and paper proofs, the principle of function
extensionality is often taken for granted.
\paragraph*{EE preservation.}
Preservation of extensional equality is a property of higher order
functions: we say that, for fixed, non-function types |A|, |B|, |C|
and |D|, a function |h : (A -> B) -> (C -> D)| preserves extensional
equality (in one argument) if |f <=> g| implies |h f <=> h g|.
Higher order functions are a distinguished trait of functional
programming languages \citep{bird2014thinking} and many well known
function combinators can be shown to preserve extensional equality.
%
For example the arrow-function |map| for |Identity|, |List|, |Maybe|
and for many other polymorphic data types preserve extensional
equality.
%
Similarly, if |h| takes two function arguments it preserves
extensional equality (in two arguments) if |f1 <=> g1| and |f2 <=> g2|
implies |h f1 f2 <=> h g1 g2|, etc.
%PJ: See notesTR/NonExamples.lidr for some analysis of this.
%
To illustrate the Idris notation for equational reasoning we show the
lemma |compPresEE| proving that function composition satisfies the
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 =
> ( (g . f) x ) ={ Refl }=
> ( g (f x) ) ={ cong (fExtEq x) }=
> ( g (f' x) ) ={ gExtEq (f' x) }=
> ( g' (f' x) ) ={ Refl }=
> ( (g' . f') x ) QED
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{idrisreference,idristutorial}.
%
The steps with |Refl| are just for human readability, they could be
omitted as far as Idris is concerned.
%
Note that the proof steps are at the level of intensional equality
which all functions preserve as witnessed by |cong|. So one can often
use |cong| in steps where an outer context is unchanged (like |g|
in this example).
%
A special case of a two-argument version of |cong| shows that composition (like all functions) preserves intensional equality:
> compPresIE : {A, B, C : Type} -> {g, g' : B -> C} -> {f, f' : A -> B} ->
> g = g' -> f = f' -> g . f = g' . f'
> compPresIE Refl Refl = Refl
Note that the ``strengths'' of the two equality preservation lemmas
are not comparable: |compPresIE| proves a stronger conclusion, but
from stronger assumptions.
\paragraph*{ADTs and equality preservation.}
Abstract data types are often specified (e.g., via Idris
\emph{interfaces} or Agda \emph{records}) in terms of higher order
functions.
%
Typical examples are, beside the already mentioned |map| for functors,
bind and Kleisli composition (see section \ref{section:example}) for monads.
%
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).
%
This is exemplified in sections \ref{section:functors} and
\ref{section:monads} for 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.
Thus, our work can also be seen as a contribution to the discussion on
verified ADTs initiated by Nicholas Drozd on
\href{https://groups.google.com/forum/#!topic/idris-lang/VZVpi-QUyUc}{idris-lang}.
%
A caveat is perhaps in place: the discussion on ADTs for functors and
monads in sections sections \ref{section:functors} and
\ref{section:monads} is not meant to answer the question of ``what
verified interfaces should look like''. Our aim is to demonstrate that,
like preservation of identity functions or preservation of composition,
preservation of extensional equality is a useful principle
for ADT design.
\paragraph*{What this paper is not about.}
Before turning to a first example, let us spend a few words on what this
paper is \emph{not} about.
%
It is not intended as a contribution to the theoretical study of the
equality type in intensional type theory or the algorithmic content of
the function extensionality principle. %|EEqImplIE|
%% TR: ``The fact ... is by no means new.'' isn't good. I copied ``and
%% the question of ... in this context'' to the next sentence
%%
%The fact that |EEqImplIE| is not provable in Martin-Löf's intensional
%type theory and the question of how to deal with extensional concepts
%in this context are by no means new.
%
The equality type in intensional type theory and the question of how
to deal with extensional concepts in this context has been the subject
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}.
%
Eventually, the study of Martin-Löf's equality type has lead to the
development of Homotopy Type Theory and Voevodsky's Univalent
Foundations program
\citep{DBLP:books/daglib/0067012,DBLP:conf/lics/HofmannS94,hottbook}.
%
Univalence and recent developments in \emph{Cubical Type Theory}
\citep{cohen2016cubical} promise to finally provide developers with a
computational version of function extensionality.
%% Tim/Nuria: new paragraph?
%%\paragraph*{What this paper is about.}
% This paper is a contribution towards \emph{pragmatic} verified generic
% programming. It might become obsolete when fully computational notions
% of function extensionality will become available in mainstream
% programming.
This paper is a contribution towards \emph{pragmatic} verified generic
programming. In this sense it might become obsolete when fully computational notions
of function extensionality will become available in mainstream
programming.
%
However, from a more abstract mathematical perspective, there are good reasons
to not use axioms that are stronger than necessary.
%
For example, there are interesting models of type theory that refute
function extensionality \citep{streicher1993investigations,
vanGlehn_2015, 10.1145/3018610.3018620}, and results that do not
rely on it can be interpreted in these models.
%
The paper has been generated from literate Idris files.
%
These can be type-checked with Idris 1.3.2 and are available at
\url{https://gitlab.pik-potsdam.de/botta/papers}.
%, 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}).
% -*-Latex-*-
%if False
> module Appendix
> import Syntax.PreorderReasoning
> import Data.List
> import About
> import Functors
> import Monads
> import Applications
> %default total
> %auto_implicits off
> %access public export
%endif
\appendix
\label{section:appendix}
% -*-Latex-*-
%if False
> module Applications
> import Syntax.PreorderReasoning
> import Data.Vect
> import About
> import Functors
> import Monads
> %default total
> %auto_implicits off
> %access public export
> %hide Prelude.List.last
> DetSys : Type -> Type
> DetSys X = X -> X
> flowDet : {X : Type} -> DetSys X -> Nat -> DetSys X
> flowDet f Z = id
> flowDet f ( S n) = flowDet f n . f
> lastLemma : {A : Type} -> {n : Nat} ->
> (x : A) -> (xs : Vect (S n) A) -> last (x :: xs) = last xs
> lastLemma x (y :: ys) = Refl
%endif
\section{Applications in dynamical systems and control theory}
\label{section:applications}
In this section we discuss applications of the principle of preservation
of extensional equality to dynamical systems and control theory.
%
We have seen in section \ref{section:example} that time discrete
deterministic dynamical systems on a set |X| are functions of type |X -> X|
< DetSys : Type -> Type
< DetSys X = X -> X
and that generalizing this notion to systems with uncertainties leads to
monadic systems
> MonSys : (Type -> Type) -> Type -> Type
> MonSys M X = X -> M X
where |M| is an \emph{uncertainty} monad: |List|, |Maybe|, |Dist|
\citep{10.1017/S0956796805005721}, |SimpleProb|
\citep{2017_Botta_Jansson_Ionescu}, etc.
%
For monadic systems, one can derive a number of general results.
%
One is that every deterministic system can be embedded in a monadic
systems:
> embed : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => DetSys X -> MonSys M X
> embed f = pure . f
A more interesting result is that the flow of a monadic system is a monoid morphism from |(Nat, (+), 0)| to |(MonSys M X, (>=>),
pure)|.
%
As discussed in section~\ref{section:example}, |flowMonL <=>
flowMonR| and here we write just |flow|.
%if False
> flow : {M : Type -> Type} -> {X : Type} -> Fat.VeriMonadFat M =>
> MonSys M X -> Nat -> MonSys M X
> flow f Z = pure
> flow f ( S n) = f >=> flow f n
%endif
The two parts of the monoid morphism proof are
> flowLemma1 : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> flow f Z <=> pure
>
> flowLemma2 : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => {m, n : Nat} ->
> (f : MonSys M X) -> flow f (m + n) <=> (flow f m >=> flow f n)
Proving |flowLemma1| is immediate (because |flow f Z = pure|):
> flowLemma1 f = reflEE
%
We prove |flowLemma2| by induction on |m| using the properties from
section \ref{section:monads}: |pure| is a left and right identity of
Kleisli composition and Kleisli composition is associative.
%
The base case is straightforward
> flowLemma2 {m = Z} {n} f x =
> ( flow f (Z + n) x ) ={ Refl }=
> ( flow f n x ) ={ sym (pureLeftIdKleisli (flow f n) x) }=
> ( (pure >=> flow f n) x ) ={ Refl }=
> ( (flow f Z >=> flow f n) x ) QED
but the induction step again relies on Kleisli composition preserving extensional equality.
> flowLemma2 f {m = S l} {n} x =
> ( flow f (S l + n) x ) ={ Refl }=
> ( (f >=> flow f (l + n)) x ) ={ kleisliPresEE f f (flow f (l + n)) (flow f l >=> flow f n)
> reflEE (flowLemma2 f) x }=
> ( (f >=> (flow f l >=> flow f n)) x ) ={ sym (kleisliAssoc f (flow f l) (flow f n) x) }=
> ( ((f >=> flow f l) >=> flow f n) x ) ={ Refl }=
> ( (flow f (S l) >=> flow f n) x ) QED
As seen in section \ref{section:monads}, this follows directly from
the monad ADT and from the preservation of extensional equality for
functors.
\paragraph*{A representation theorem.}
%
Another important result for monadic systems is a representation
theorem: any monadic system |f : MonSys M X| can be represented by
a deterministic system on |M X|. With
> repr : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => MonSys M X -> DetSys (M X)
> repr f = id >=> f
% in other symbols: repr f x = x >>= f
%
and for an arbitrary monadic system |f|, |repr f| is equivalent to |f|
in the sense that
% %format (flowDet f n) = f "^{" n "}"
> reprLemma : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> (n : Nat) -> repr (flow f n) <=> flowDet (repr f) n
where |flowDet| is the flow of a deterministic system
< flowDet : {X : Type} -> DetSys X -> Nat -> DetSys X
< flowDet f Z = id
< flowDet f ( S n) = flowDet f n . f
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:
% > reprLemma f Z mx =
% > ( (repr (flow f Z)) mx ) ={ Refl }=
% > ( (id >=> flow f Z) mx ) ={ Refl }=
% > ( (id >=> pure) mx ) ={ Fat.pureRightIdKleisli id mx }=
% > ( id mx ) ={ Refl }=
% > ( 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 }=
> ( (id >=> (f >=> flow f m)) mx ) ={ sym (Fat.kleisliAssoc id f (flow f m) mx) }=
> ( ((id >=> f) >=> flow f m) mx ) ={ kleisliLeapfrog (id >=> f) (flow f m) mx }=
> ( (id >=> flow f m) ((id >=> f) mx) ) ={ Refl }=
> ( repr (flow f m) ((id >=> f) mx) ) ={ reprLemma f m ((id >=> f) mx) }=
> ( flowDet (repr f) m ((id >=> f) mx) ) ={ Refl }=
> ( flowDet (repr f) m (repr f mx) ) ={ Refl }=
> ( flowDet (repr f) (S m) mx ) QED
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.
\paragraph*{Flows and trajectories.}
%
The last application of preservation of extensional
equality in the context of dynamical systems theory is a result about
flows and trajectories.
%
For a monadic system |f|, the trajectories of length |n+1| starting at
state |x : X| are
> trj : {M : Type -> Type} -> {X : Type} -> Fat.VeriMonadFat M =>
> MonSys M X -> (n : Nat) -> X -> M (Vect (S n) X)
> trj f Z x = map (x ::) (pure Nil)
> trj f ( S n) x = map (x ::) ((f >=> trj f n) x)
In words, the trajectory obtained by making zero steps starting at |x|
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|.
%
Finally, we prepend these possible trajectories with the initial state
|x|.
Since |trj f n x| is an |M|-structure of vectors of states, we can
compute the last state of each trajectory.
%
It turns out that this is point-wise equal to |flow f n|:
> flowTrjLemma : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M =>
> (f : MonSys M X) -> (n : Nat) ->
> flow f n <=> map {A = Vect (S n) X} last . trj f n
To prove this result, we first derive the auxiliary lemma
> mapLastLemma : {F : Type -> Type} -> {X : Type} -> {n : Nat} -> VeriFunctor F =>
> (x : X) -> (mvx : F (Vect (S n) X)) ->
> (map last . map (x ::)) mvx = map last mvx
> mapLastLemma {X} {n} x mvx =
> ( map {A = Vect (S (S n)) X} last (map (x ::) mvx) )
> ={ sym (mapPresComp {A = Vect (S n) X} last (x ::) mvx) }=
> ( map (last . (x ::)) mvx )
> ={ mapPresEE (last . (x ::)) last (lastLemma x) mvx }=
> ( map last mvx ) QED
where |lastLemma x : last . (x ::) <=> last|.
In the implementation of |mapLastLemma| we have applied both
preservation of composition and preservation of extensional
equality.
%
With |mapLastLemma| in place, |flowTrjLemma| is readily implemented by
induction on the number of steps
%**PJ: Only added to avoid bad page-break
%\newpage
> flowTrjLemma {X} f Z x =
> ( flow f Z x ) ={ Refl }= (pure x) ={ Refl }=
> ( pure (last (x :: Nil)) ) ={ sym (Fat.pureNatTrans last (x :: Nil)) }=
> ( map last (pure (x :: Nil)) ) ={ cong {f = map last}
> (sym (Fat.pureNatTrans {A = Vect Z X} (x ::) Nil)) }=
> ( map last (map (x ::) (pure Nil)) ) ={ Refl }=
> ( map last (trj f Z x) ) QED
>
> flowTrjLemma f (S m) x =
> ( flow f (S m) x ) ={ Refl }=
> ( (f >=> flow f m) x ) ={ kleisliPresEE f f (flow f m) (map (last {len = m}) . trj f m)
> reflEE (flowTrjLemma f m) x }=
>
> ( (f >=> map (last {len = m}) . trj f m) x ) ={ sym (mapKleisliLemma f (trj f m) last x) }=
> ( map last ((f >=> trj f m) x) ) ={ sym (mapLastLemma x ((f >=> trj f m) x)) }=
> ( map last (map (x ::) ((f >=> trj f m) x)) ) ={ Refl }=
> ( map last (trj f (S m) x) ) QED
Again, preservation of extensional equality proves essential for the induction step.
\paragraph*{Dynamic programming (DP).} The relationship between the
flow and the trajectory of a monadic dynamical system also plays a
crucial role in the \emph{semantic verification} of dynamic