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

Sync with unshared/manuscripts/2020.exteqaxiom.

parent a33c0e8f
......@@ -24,7 +24,7 @@ import LexerFriendlyReasoning -- not yet working as intended
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
Agda~\citep{norell2007thesis} and Coq~\citep{CoqProofAssistant} that
implement %some version of
Martin-Löf's intensional type
theory \citep{martinlof1984}. % , nordstrom1990programming
......@@ -161,8 +161,8 @@ 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 \citep{UniMath}
foundations or |eqfun| in Coq \citep{CoqProofAssistant_8_11}.
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
......@@ -179,10 +179,15 @@ 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.
%
%For example the arrow-function |map| for |Identity|, |List|, |Maybe|
%and for many other polymorphic data types preserve extensional
%equality.
% Tim: is this the place to hint to Coq and Agda standard libs?
In particular, the arrow-function |map| for |Identity|, |List|, |Maybe|
and for many other polymorphic data types preserves extensional
equality. The standard libraries of Agda and Coq provide several
instances\footnote{e.g. Agda for |Maybe|: \url{https://agda.github.io/agda-stdlib/Data.Maybe.Properties.html}}
\footnote{e.g. Coq for |List|: \url{https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html}}.
Similarly, if |h| takes two function arguments it preserves
extensional equality (in two arguments) if |f1 <=> g1| and |f2 <=> g2|
......@@ -205,7 +210,7 @@ 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{idrisreference,idristutorial}.
\citep{idrisdocs}.
%
The steps with |Refl| are just for human readability, they could be
omitted as far as Idris is concerned.
......@@ -302,17 +307,16 @@ computational version of function extensionality.
% 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.
programming. From this perspective, it might become obsolete when fully
computational notions of function extensionality will become available
in mainstream programming.
%
From a more mathematical perspective, there are good reasons not to rely
on axioms that are stronger than necessary: there are interesting models
of type theory that refute function extensionality
\citep{streicher1993investigations, vanGlehn_2015,
10.1145/3018610.3018620}, and our results can be interpreted in these
models.
%
The paper has been generated from literate Idris files.
......
% -*-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}
......@@ -50,12 +50,12 @@ monadic systems
where |M| is an \emph{uncertainty} monad: |List|, |Maybe|, |Dist|
\citep{10.1017/S0956796805005721}, |SimpleProb|
\citep{2017_Botta_Jansson_Ionescu}, etc.
\citep{ionescu2009, 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:
system:
> embed : {X : Type} -> {M : Type -> Type} -> Fat.VeriMonadFat M => DetSys X -> MonSys M X
......
......@@ -12,9 +12,9 @@
\label{section:conclusions}
In dependently typed programming in the context of Martin-Löf type
theories \citep{nordstrom1990programming}, the problem of how to specify
abstract data types for verified generic programming is still not well
understood.
theories \citep{nordstrom1990programming, martinlof1984}, the problem of
how to specify abstract data types for verified generic programming is
still not well understood.
%
In this work, we have shown that requiring functors to preserve
extensional equality of arrows yields abstract data types that are
......
......@@ -42,10 +42,10 @@ In dynamical systems theory \citep{Kuznetsov:1998:EAB:289919,
thomas2012catastrophe}, a prominent notion is that of the flow (or
iteration) of a system.
%
A \emph{deterministic} dynamical system on a set |X| is an endofunction on |X|.
The set |X| is often called the \emph{state space} of the system.
%
After explaining this simpler, deterministic, case we will get to a more general, monadic, case.
We start by discussing deterministic systems and then generalize to the
monadic case. A \emph{deterministic} dynamical system on a set |X| is an
endofunction on |X|. The set |X| is often called the \emph{state space}
of the system.
Given a deterministic system |f : X -> X|, its $n$-th iterate or flow,
is typically denoted by |pow f n : X -> X| and is defined by induction
......@@ -147,26 +147,20 @@ fuzzy systems?
Can we extend our results to the general case of \emph{monadic}
dynamical systems?
%
Monadic dynamical systems \citep{ionescu2009, 2017_Botta_Jansson_Ionescu}
Monadic dynamical systems \citep{ionescu2009}
on a set |X| are functions of type |X -> M X| where |M| is a monad.
%
When |M| is equal to 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.
%%Tim, Nuria: perhaps avoid "equal" altogether?
%%When |M| is the identity monad, one recovers the
%%deterministic case.
%%%
%%When |M| is |List| one has non-deterministic systems. Taking for |M|
%%a finite probability monad (e.g. |Dist|
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}) captures the notion of stochastic
%%\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.
%
Other monads encode other notions of uncertainty, see
\citep{ionescu2009,giry1981}.
......@@ -187,8 +181,8 @@ with |pure| and function composition with Kleisli composition (|>=>|):
> flowMonR f Z = pure
> flowMonR f ( S n) = f >=> flowMonR f n
Notice, however, that now the implementation of |flowMonL| and
|flowMonR| depends on |(>=>)|, which is a monad-specific operation.
Notice, however, that now the implementations of |flowMonL| and
|flowMonR| depend on |(>=>)|, which is a monad-specific operation.
%
This means that, in proving properties of the flow of monadic systems,
we can no longer rely on a specific \emph{definition} of |(>=>)|: we
......
......@@ -57,8 +57,9 @@ When considering ADT specifications of functor (and of natural
transformation, monad, etc.) in dependently typed languages, one has to
distinguish between two related but different situations.
One in which the specification is part of an attempt at formalizing
category theory. In this situation, one has to expect the notion of
One in which the specification is put forward in the context of
formalizations of category theory, see for example \citep{UniMath,
CoqProofAssistant}. In this situation, one has to expect the notion of
category to be in place and that of functor to be predicated on that of
its source and target categories. A functor ADT in this situation is an
answer to the question ``What shall the notion of functor look like in
......@@ -152,7 +153,7 @@ generality (supporting a larger class of functors) by parameterising
over the equalities used, but this leads to quite a bit of book-keeping
(basically a setoid-based framework).
%
We instead stop at this point and hope to show that it is a pragmatic
We instead stop at this point and show that it is a pragmatic
compromise between generality and convenient usage.
\paragraph*{Equality preservation examples.}
......@@ -171,11 +172,11 @@ proof looks as follows:
% {-" below=\the\belowdisplayskip"-}
> mapListPresEE : {A, B : Type} -> (f, g : A -> B) -> f <=> g -> mapList f <=> mapList g
> mapListPresEE f g fExtg [] = Refl
> mapListPresEE f g fExtg (a :: as) =
> 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)} (fExtg a) }=
> ( g a :: mapList f as ) ={ cong (mapListPresEE f g fExtg as) }=
> ( 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
......@@ -259,7 +260,7 @@ If we try to implement preservation of extensional equality we end up with
> mapReaderPresEE : {A, B : Type} -> (f, g : A -> B) ->
> f <=> g -> mapReader f <=> mapReader g
> mapReaderPresEE f g fExtEqg r =
> mapReaderPresEE f g fEEg r =
> ( mapReader f r) ={ Refl }=
> ( f . r ) ={ whatnow1 r }= -- here we need |f = g| to proceed
> ( g . r ) ={ Refl }=
......@@ -267,7 +268,8 @@ If we try to implement preservation of extensional equality we end up with
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 \citep{idrisguides}. Among others, we can ask about the
this step, see ``Elaborator Reflection -- Holes'' in \citep{idrisdocs}.
Among others, we can ask about the
type of |whatnow1r|. Perhaps not surprisingly, this turns out to be |f
. r = g . r|.
......@@ -290,7 +292,7 @@ extify (<=>)| it is easy to show
> mapReaderPresEE2 : {E, A, B : Type} -> (f, g : A -> B) ->
> f <=> g -> mapReader f <==> mapReader g
> mapReaderPresEE2 f g fExtEqg r x = fExtEqg (r x)
> mapReaderPresEE2 f g fEEg r x = fEEg (r x)
Thus, |Reader E| is an example of a functor which does not preserve,
but rather \emph{transforms} the notion of equality.
......@@ -332,4 +334,4 @@ the monad ADT design.
%% We are interested in ADTs that support well verified generic programming
%% and we discuss the advantages and the disadvantages of different
%% approaches from an DSL perspective. As in section \ref{section:example},
%% we discuss appplications in dynamical systems and control theory.
%% we discuss applications in dynamical systems and control theory.
......@@ -16,7 +16,6 @@ main.tex: main.lhs \
Applications.lidr \
RelatedWork.lidr \
Conclusions.lidr \
Appendix.lidr \
references.bib
${LHS2TEX} --poly main.lhs > main.almost_tex
./spacefix.bash main.almost_tex > main.tex
......
......@@ -32,10 +32,9 @@ We discuss the role of extensional equality preservation for deriving
monad laws and for verifying the equivalence between the different ADT
formulations.
%
Note that there are many possible versions of the axioms and we do not
claim to have found the ``optimal'' axioms for Monad specifically, but
we want to explain the trade-offs between different kinds of
formulations.
There are many possible way of formulating Monad axioms. Here, we do not
argue for or against a specific formulation but rather discuss the most
popular ones and their trade-offs.
\subsection{The traditional view}\label{sec:MonadTradView}
......@@ -157,7 +156,7 @@ The same approach can be followed for implementing bind, another monad
combinator similar to Kleisli composition:
> (>>=) : {A, B : Type} -> {M : Type -> Type} -> ThinVeriMonad M => M A -> (A -> M B) -> M B
> ma >>= f = join (map f ma)
> ma >>= f = join (map f ma)
Starting from a \emph{thin} monad ADT as in the example above and
adding monadic operators that fulfil a specification
......@@ -544,11 +543,9 @@ The lifting operation is required to satisfy W1--W3 for any objects
\paragraph*{From tradition to Wadler and back.}
%
We here briefly explain how the two monad definitions can be seen as
views on the same mathematical concept.
%
We do this because we would like the corresponding ADT formulations to
also preserve this relationship.
The two monad definitions can be seen as views on the same mathematical
concept and we would like the corresponding ADT formulations to preserve
this relationship.
It turns out that, if (|M|, |etaN|, |muN|) fulfil the properties T1--T5
of the traditional view, then the object part of |M|, |etaN|, and the
......
......@@ -115,7 +115,6 @@ generic programming.
%include Applications.lidr
%include RelatedWork.lidr
%include Conclusions.lidr
%%include Appendix.lidr
\section*{Acknowledgments}
%**PJ[after review]: The authors thank the JFP editors and reviewers, whose comments have
......
......@@ -22,6 +22,15 @@
year = 2020
}
@misc{idrisdocs,
author = {{The Idris Community}},
title = {{D}ocumentation for the {I}dris {L}anguage},
howpublished = {\url{http://docs.idris-lang.org/en/latest/}},
url = {http://docs.idris-lang.org/en/latest/},
year = 2020
}
@book{idrisbook,
author = {Edwin Brady},
publisher = {Manning Publications Co.},
......@@ -41,7 +50,7 @@
author = {Nicola Botta},
howpublished = {\url{https://gitlab.pik-potsdam.de/botta/IdrisLibs}},
title = {{I}dris{L}ibs},
year = {2016--2020}
year = {2016-2021}
}
@inproceedings{ionescujansson:LIPIcs:2013:3899,
......@@ -269,7 +278,7 @@
(DSLsofMath)},
url =
{https://www.chalmers.se/en/projects/Pages/Domain-Specific-Languages-of-Mathematics-QDSLsofMathQ.aspx},
year = {2014-2020}
year = {2014-2021}
}
@book{Kuznetsov:1998:EAB:289919,
......@@ -473,17 +482,15 @@
year = 1981
}
@misc{CoqProofAssistant_8_11,
doi = {10.5281/ZENODO.1003420},
url = {https://zenodo.org/record/1003420},
author = "{The Coq Dev.\ Team}",
LONGauthor = "{The Coq Development Team}",
keywords = {proof assistant, mathematical software, formal
proofs},
language = {en},
title = {The Coq Proof Assistant, version 8.11.0},
publisher = {Zenodo},
year = 2020
@misc{CoqProofAssistant,
author = {{The Coq Development Team}},
title = {The Coq Proof Assistant (Version 8.13.0)},
month = jan,
year = 2021,
publisher = {Zenodo},
version = {8.13},
doi = {10.5281/zenodo.4501022},
howpublished = {\url{https://doi.org/10.5281/zenodo.4501022}}
}
@book{nordstrom1990programming,
......@@ -497,9 +504,9 @@
@misc{brede2020,
author = {Brede, Nuria and Botta, Nicola},
title = {Semantic verification of dynamic programming},
howpublished = {In submission to J. Funct. Program.},
year = 2020
title = {On the correctness of monadic backward induction},
howpublished = {Submitted to J. Funct. Program., \url{https://arxiv.org/abs/2008.02143}},
year = 2021
}
@article{gnesi1981dynamic,
......@@ -840,22 +847,48 @@ isbn="978-3-540-71067-7"
@misc{CoRN_library,
author = {Spitters, Bas and Semeria, Vincent (Maintainers)},
howpublished = {\url{https://github.com/coq-community/corn}},
title = {Coq Repository at Nijmegen},
year = {2000-2020}
title = {Coq Repository at Nijmegen (Version 1.2.0)},
year = {2017}
}
@InProceedings{10.1007/978-3-540-27818-4_7,
author="Cruz-Filipe, Lu{\'i}s
and Geuvers, Herman
and Wiedijk, Freek",
editor="Asperti, Andrea
and Bancerek, Grzegorz
and Trybulec, Andrzej",
title="C-CoRN, the Constructive Coq Repository at Nijmegen",
booktitle="Mathematical Knowledge Management",
year="2004",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="88--103",
isbn="978-3-540-27818-4"
}
@misc{CoLoR_library,
author = {Frederic Blanqui and others},
howpublished = {\url{https://github.com/fblanqui/color}},
title = {CoLoR: a Coq Library on Rewriting and termination},
year = {2005-2020}
title = {CoLoR: a Coq Library on Rewriting and termination (Version 1.8.0)},
year = {2020}
}
@article{blanqui_koprowski_2011,
title={CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates}, volume={21},
DOI={10.1017/S0960129511000120},
number={4},
journal={Mathematical Structures in Computer Science},
publisher={Cambridge University Press},
author={Blanqui, Fred{\'e}d{\'e}ric and Koprowski, Adam},
year={2011},
pages={827--859}}
@misc{arend_prover,
author = {{JetBrains Research}},
howpublished = {\url{https://arend-lang.github.io/}},
title = {Arend Theorem Prover},
year = {2020}
title = {Arend Theorem Prover (Version 1.6.0)},
year = {2021}
}
@Misc{UniMath,
......@@ -865,8 +898,7 @@ isbn="978-3-540-71067-7"
univalent mathematics},
url = {https://github.com/UniMath/UniMath},
howpublished = {Available at
\url{https://github.com/UniMath/UniMath}},
year = 2017
\url{https://github.com/UniMath/UniMath}}
}
@book{pierce_basic_1991,
......@@ -884,16 +916,16 @@ isbn="978-3-540-71067-7"
@Misc{carette_agda,
author = {Jacques Carette and Jason Z. S. Hu},
title = {A new Categories library for {Agda}},
title = {A new Categories library for {Agda} (Version 0.1.5)},
howpublished = {\url{https://github.com/agda/agda-categories}},
year = 2020
year = 2021
}
@Misc{wiegley_coq,
author = {Wiegley, John},
title = {Category Theory in {Coq}},
howpublished = {\url{https://github.com/jwiegley/category-theory}},
year = 2017
year = {2014\mbox{--}2018}
}
@Misc{megasz_coq,
......@@ -1065,7 +1097,7 @@ isbn="978-3-540-71067-7"
title={Formalizing of Category Theory in Agda},
author={Jason Z. S. Hu and Jacques Carette},
year={2021},
howpublished={\url{https://arxiv.org/abs/2005.07059v2}},
howpublished={\url{https://arxiv.org/abs/2005.07059}},
eprint={2005.07059},
archivePrefix={arXiv},
primaryClass={cs.LO}
......@@ -1169,4 +1201,4 @@ series = {CPP 2017}
{https://dblp.org/rec/journals/corr/abs-1202-2919.bib},
bibsource = {dblp computer science bibliography,
https://dblp.org}
}
\ No newline at end of file
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment