Commit 11a4dd0c authored by Nicola Botta's avatar Nicola Botta
Browse files

Final.

parent c06d4c30
......@@ -257,7 +257,7 @@ 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
monads in 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,
......@@ -295,7 +295,7 @@ 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
\citep{cohenetal18:cubical} promise to finally provide developers with a
computational version of function extensionality.
......@@ -315,7 +315,7 @@ 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,
\citep{streicher1993investigations, vonGlehn_2015,
10.1145/3018610.3018620}, and our results can be interpreted in these
models.
%
......
......@@ -201,6 +201,9 @@ Kleisli composition to fulfil the specification
%
\vspace*{-2ex}
\begin{center}
%%***TODO replace with pdf include
%% See https://tex.stackexchange.com/questions/452/how-can-i-create-a-pdf-document-exactly-as-big-as-my-tikz-picture/514
\beginpgfgraphicnamed{ExtEqPres-f1}
\begin{tikzcd}[column sep=large]
|M C|
& |M (M C)| \arrow[l, "|join|"]
......@@ -209,6 +212,7 @@ Kleisli composition to fulfil the specification
\mathbin{> \!\! = \!\! >}
g"]
\end{tikzcd}
\endpgfgraphicnamed
\end{center}
> kleisliSpec : {A, B, C : Type} -> {M : Type -> Type} -> Monad M =>
......
......@@ -50,17 +50,21 @@ two \emph{natural transformations}
such that, for any object |A| of $\mathcal{C}$, the following diagrams commute:
\begin{minipage}{0.4\textwidth}
\beginpgfgraphicnamed{ExtEqPres-f2}
\begin{tikzcd}[row sep=large, column sep=large]
|M A| \arrow[r, "|eta (M A)|"] \arrow[dr, "|id_MA|"'] & |M (M A)| \arrow[d, "|mu A|"] & |M A| \arrow[l, "|M (eta A)|"'] \arrow[dl, "|id_MA|"] \\
& |M A| &
\end{tikzcd}
\endpgfgraphicnamed
\end{minipage}
\hfill
\begin{minipage}{0.4\textwidth}
\beginpgfgraphicnamed{ExtEqPres-f3}
\begin{tikzcd}[row sep=large, column sep=large]
|M (M (M A))| \arrow[r, "|M (mu A)|"] \arrow[d, "|mu (M A)|"'] & |M (M A)| \arrow[d, "|mu A|"] \\
|M (M A)| \arrow[r, "|mu A|"'] & |M A|
\end{tikzcd}
\endpgfgraphicnamed
\end{minipage}
\noindent
......@@ -79,17 +83,21 @@ diagrams commute for any arrow |f : A -> B| in $\mathcal{C}$:
%\end{minipage}
\hfill
\begin{minipage}{0.3\textwidth}
\beginpgfgraphicnamed{ExtEqPres-f4}
\begin{tikzcd}[row sep=large, column sep=large]
|A| \arrow[r, "|f|"] \arrow[d, "|eta A|"'] & |B| \arrow[d, "|eta B|"] \\
|M A| \arrow[r, "|M f|"'] & |M B|
\end{tikzcd}
\endpgfgraphicnamed
\end{minipage}
\hfill
\begin{minipage}{0.4\textwidth}
\beginpgfgraphicnamed{ExtEqPres-f5}
\begin{tikzcd}[row sep=large, column sep=large]
|M (M A)| \arrow[r, "|M (M f)|"] \arrow[d, "|mu A|"'] & |M (M B)| \arrow[d, "|mu B|"] \\
|M A| \arrow[r, "|M f|"'] & |M B|
\end{tikzcd}
\endpgfgraphicnamed
\end{minipage}
\noindent
......
......@@ -64,12 +64,12 @@ and in Agda has to be disabled using a special flag.
%
%
Finally, in \emph{Cubical Type Theory} \citep{cohen2016cubical}
Finally, in \emph{Cubical Type Theory} \citep{cohenetal18:cubical}
function extensionality is provable because of the presence of the
\emph{interval primitive} and thus has computational content.
%
Cubical type theory has recently been implemented as a special version
of Agda \citep{10.1145/3341691}.
of Agda \citep{cubicalagda2}.
%
Another (similar) version of homotopy type theory is implemented in
the theorem prover Arend \citep{arend_prover}.
......@@ -82,7 +82,7 @@ On the topic of interfaces (type classes) and their laws there is
related work in specifying \citep{janssonjeuring-dataconv}, rewriting
\citep{peytonjones2001playing}, testing
\citep{jeuringHaskell12ClassLaws} and proving
\citep{DBLP:journals/corr/abs-1808-05789} type class laws in Haskell.
\citep{arvidssonetal19:typeclasslaws} type class laws in Haskell.
%
The equality challenges here are often related to the semantics of
non-termination as described in the Fast and Loose Reasoning paper
......
% -*-Latex-*-
\RequirePackage{amsmath}
\documentclass{jfp}
%\documentclass{jfphack}
\usepackage{tikz-cd}
%% begin for submission
\pgfrealjobname{main}
%% end for submission
\usepackage{quoting}
\usepackage{bigfoot} % To handle url with special characters in footnotes!
\usepackage{hyperref}
......
......@@ -50,7 +50,7 @@
author = {Nicola Botta},
howpublished = {\url{https://gitlab.pik-potsdam.de/botta/IdrisLibs}},
title = {{I}dris{L}ibs},
year = {2016-2021}
year = {2016--2021}
}
@inproceedings{ionescujansson:LIPIcs:2013:3899,
......@@ -68,7 +68,7 @@
longbooktitle ={18th International Workshop on Types for Proofs and
Programs (TYPES 2011)},
pages = {41--54},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
title = {Testing versus proving in climate impact research},
......@@ -153,8 +153,7 @@
booktitle = {The Stanford Encyclopedia of Philosophy},
edition = {Winter 2016},
editor = {Edward N. Zalta},
howpublished =
{\url{https://plato.stanford.edu/archives/win2016/entries/decision-causal/}},
howpublished = {\url{https://plato.stanford.edu/archives/win2016/entries/decision-causal/}},
publisher = {Metaphysics Research Lab, Stanford University},
title = {Causal Decision Theory},
year = 2016
......@@ -167,7 +166,7 @@
biburl = {https://dblp.org/rec/bib/conf/lics/Moggi89},
booktitle = {Proceedings of the Fourth Annual Symposium on Logic
in Computer Science {(LICS} '89), Pacific Grove,
California, USA, June 5-8, 1989},
California, USA, June 5--8, 1989},
crossref = {DBLP:conf/lics/1989},
doi = {10.1109/LICS.1989.39155},
pages = {14--23},
......@@ -201,7 +200,7 @@
booktitle = {Proceedings of the fourth international conference
on Functional programming languages and computer
architecture, {FPCA} 1989, London, UK, September
11-13, 1989},
11--13, 1989},
crossref = {DBLP:conf/fpca/1989},
doi = {10.1145/99370.99404},
pages = {347--359},
......@@ -235,8 +234,8 @@
biburl = {https://dblp.org/rec/bib/books/daglib/0096998},
isbn = {978-0-13-507245-5},
publisher = {Prentice Hall},
series = {Prentice Hall International series in computer
science},
series = {Prentice Hall International Series in Computer
Science},
timestamp = {Thu, 03 Feb 2011 12:08:27 +0100},
title = {Algebra of programming},
year = {1997}
......@@ -276,17 +275,17 @@
author = {Patrik Jansson and Cezar Ionescu},
title = {Domain Specific Languages of Mathematics
(DSLsofMath)},
url =
{https://www.chalmers.se/en/projects/Pages/Domain-Specific-Languages-of-Mathematics-QDSLsofMathQ.aspx},
year = {2014-2021}
url = {https://www.chalmers.se/en/projects/Pages/Domain-Specific-Languages-of-Mathematics-QDSLsofMathQ.aspx},
year = {2014--2021}
}
@book{Kuznetsov:1998:EAB:289919,
address = {Berlin, Heidelberg},
address = {Berlin},
author = {Yuri A. Kuznetsov},
isbn = {0-387-98382-1},
publisher = {Springer-Verlag},
title = {Elements of Applied Bifurcation Theory (2nd Ed.)},
publisher = {Springer},
title = {Elements of Applied Bifurcation Theory},
edition = {2.},
year = 1998
}
......@@ -297,8 +296,8 @@
biburl = {https://dblp.org/rec/bib/books/daglib/0067018},
isbn = {978-0-13-726233-5},
publisher = {Prentice Hall},
series = {Prentice Hall International Series in computer
science},
series = {Prentice Hall International Series in Computer
Science},
timestamp = {Thu, 22 Feb 2018 18:20:56 +0100},
title = {Programming from specifications},
year = 1990
......@@ -344,7 +343,7 @@
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
title = {Proceedings of the Fourth Annual Symposium on Logic
in Computer Science {(LICS} '89), Pacific Grove,
California, USA, June 5-8, 1989},
California, USA, June 5--8, 1989},
url =
{https://ieeexplore.ieee.org/xpl/conhome/249/proceeding},
year = 1989
......@@ -362,7 +361,7 @@
title = {Proceedings of the fourth international conference
on Functional programming languages and computer
architecture, {FPCA} 1989, London, UK, September
11-13, 1989},
11--13, 1989},
url = {https://doi.org/10.1145/99370},
year = 1989
}
......@@ -421,15 +420,14 @@
year = 2006,
issue_date = {January 2006},
publisher = {Cambridge University Press},
address = {USA},
volume = 16,
number = 1,
issn = {0956-7968},
url = {https://doi.org/10.1017/S0956796805005721},
doi = {10.1017/S0956796805005721},
journal = {J. Funct. Program.},
journal = {Journal of Functional Programming},
month = jan,
pages = {2134},
pages = {21--34},
numpages = 14
}
......@@ -445,7 +443,7 @@
author = {Avery, Tom},
year = 2016,
month = {Mar},
pages = {12291251}
pages = {1229--1251}
}
@phdthesis{norell2007thesis,
......@@ -454,19 +452,18 @@
school = {Chalmers University of Technology},
title = {Towards a practical programming language based on
dependent type theory},
url =
{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
volume = 32,
doi = {10.1.1.436.7331},
year = 2007
}
@book{martinlof1984,
AUTHOR = {Martin-L{\"o}f, Per and Sambin, Giovanni},
TITLE = {Intuitionistic type theory},
VOLUME = {9},
PUBLISHER = {Bibliopolis Naples},
YEAR = 1984
author = {Martin-L{\"o}f, Per and Sambin, Giovanni},
title = {Intuitionistic type theory},
volume = {9},
publisher = {Bibliopolis Naples},
year = 1984
}
@Incollection{giry1981,
......@@ -497,15 +494,16 @@
title = {Programming in {M}artin-{L}{\"o}f’s type theory},
author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith,
Jan M},
series = {International Series of Monographs on Computer Science},
volume = 200,
year = 1990,
publisher = {Oxford University Press Oxford}
publisher = {Oxford University Press}
}
@misc{brede2020,
author = {Brede, Nuria and Botta, Nicola},
title = {On the correctness of monadic backward induction},
howpublished = {Submitted to J. Funct. Program., \url{https://arxiv.org/abs/2008.02143}},
howpublished = {Submitted to Journal of Functional Programming, \url{https://arxiv.org/abs/2008.02143}},
year = 2021
}
......@@ -514,18 +512,21 @@
approach},
author = {Gnesi, Stefania and Montanari, Ugo and Martelli,
Alberto},
journal = {Journal of the {ACM} ({JACM})},
journal = {Journal of the {ACM}},
volume = 28,
number = 4,
pages = {737--751},
year = 1981,
publisher = {ACM New York, NY, USA}
publisher = {ACM}
}
@inproceedings{de_moor1995,
author = {De Moor, Oege},
title = {A generic program for sequential decision processes},
booktitle = {{PLILPS} '95 Proceedings of the 7th International
booktitle = {{PLILPS} '95
Symposium on Programming Languages: Implementations,
Logics and Programs},
longbooktitle = {{PLILPS} '95 Proceedings of the 7th International
Symposium on Programming Languages: Implementations,
Logics and Programs},
pages = {1--23},
......@@ -545,7 +546,7 @@
@article{sozeau2010new,
title = {A new look at generalized rewriting in type theory},
author = {Sozeau, Matthieu},
journal = {Journal of formalized reasoning},
journal = {Journal of Formalized Reasoning},
volume = 2,
number = 1,
pages = {41--62},
......@@ -553,19 +554,21 @@
}
@book{hofmann1995extensional,
@phdthesis{hofmann1995extensional,
title = {Extensional concepts in intensional type theory},
school = {University of Edinburgh},
author = {Hofmann, Martin},
year = 1995,
publisher = {University of Edinburgh. College of Science and
Engineering.},
URL =
"https://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/"
URL = {https://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/}
}
@book{hofmann2012extensional,
title = {Extensional constructs in intensional type theory},
doi = {10.1007/978-1-4471-0963-1},
author = {Hofmann, Martin},
series= {Distinguished Dissertations},
year = 2012,
publisher = {Springer Science \& Business Media}
}
......@@ -586,12 +589,13 @@
@inproceedings{wadler1992essence,
title = {The essence of functional programming},
author = {Wadler, Philip},
booktitle = {Proceedings of the 19th {ACM} {SIGPLAN}-{SIGACT} symposium on Principles of programming languages},
booktitle = {{ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
longbooktitle = {Proceedings of the 19th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
pages = {1--14},
year = {1992}
}
@article{streicher2003category,
@article{streicher2003category_old,
title = {Category {T}heory and {C}ategorical {L}ogic},
author = {Streicher, Thomas},
journal = {Lecture {N}otes, {T}echnische {U}niversit{\"a}t {D}armstadt,
......@@ -599,10 +603,18 @@
year = {2003}
}
@article{dawson2007compound,
@misc{streicher2003category,
title = {Category {T}heory and {C}ategorical {L}ogic},
author = {Streicher, Thomas},
howpublished = {Lecture {N}otes, {T}echnische {U}niversit{\"a}t {D}armstadt,
\url{https://www2.mathematik.tu-darmstadt.de/~streicher/CTCL.pdf}},
year = {2003}
}
@misc{dawson2007compound,
title = {Compound monads and the {K}leisli category},
author = {Dawson, Jeremy E},
journal = {unpublished note, http://users. cecs. anu. edu. au/jeremy/pubs/cmkc/cmkc. pdf},
howpublished = {unpublished note, http://users. cecs. anu. edu. au/jeremy/pubs/cmkc/cmkc. pdf},
year = 2007
}
......@@ -626,28 +638,29 @@
lccn = 83020031,
url = {https://books.google.de/books?id=kQT8CAAAQBAJ},
year = 2012,
publisher = {Springer Berlin Heidelberg}
publisher = {Springer}
}
@Book{hottbook,
author = {The {Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013}
author = {{The Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013
}
@book{DBLP:books/daglib/0067012,
author = {Thomas Streicher},
title = {Semantics of type theory - correctness, completeness and independence
results},
series = {Progress in theoretical computer science},
publisher = {Birkh{\"{a}}user},
year = {1991},
isbn = {978-0-8176-3594-7},
timestamp = {Wed, 17 Jul 2019 17:20:52 +0200},
biburl = {https://dblp.org/rec/books/daglib/0067012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
author = {Thomas Streicher},
title = {Semantics of type theory - correctness, completeness and independence
results},
series = {Progress in Theoretical Computer Science},
publisher = {Birkh{\"{a}}user},
year = {1991},
isbn = {978-0-8176-3594-7},
timestamp = {Wed, 17 Jul 2019 17:20:52 +0200},
biburl = {https://dblp.org/rec/books/daglib/0067012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{10.5555/788021.788977,
author = {Altenkirch, Thorsten},
......@@ -679,24 +692,22 @@
month = {Sep}
}
@article{KINOSHITA2014145,
title = "Category theoretic structure of setoids",
journal = "Theoretical Computer Science",
title = {Category theoretic structure of setoids},
journal = {Theoretical Computer Science},
volume = 546,
pages = "145 - 163",
pages = {145--163},
year = 2014,
note = "Models of Interaction: Essays in Honour of Glynn
Winskel",
issn = "0304-3975",
doi = "https://doi.org/10.1016/j.tcs.2014.03.006",
url =
"http://www.sciencedirect.com/science/article/pii/S0304397514001819",
author = "Yoshiki Kinoshita and John Power",
keywords = "Setoid, Proof assistant, Proof irrelevance,
note = {Models of Interaction: Essays in Honour of Glynn
Winskel},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2014.03.006},
url = {http://www.sciencedirect.com/science/article/pii/S0304397514001819},
author = {Yoshiki Kinoshita and John Power},
keywords = {Setoid, Proof assistant, Proof irrelevance,
Cartesian closed category, Coproduct, -category,
-inserter, -category, -coinserter",
abstract = "A setoid is a set together with a constructive
-inserter, -category, -coinserter},
abstract = {A setoid is a set together with a constructive
representation of an equivalence relation on
it. Here, we give category theoretic support to the
notion. We first define a category Setoid and prove
......@@ -711,98 +722,95 @@
a relaxed form of coequalisers. In doing all this,
we carefully compare our category theoretic
constructs with Agda code for type-theoretic
constructs on setoids."
constructs on setoids.}
}
@inproceedings{DBLP:conf/lics/HofmannS94,
author = {Martin Hofmann and
Thomas Streicher},
title = {The Groupoid Model Refutes Uniqueness of Identity Proofs},
booktitle = {Proceedings of the Ninth Annual Symposium on Logic in Computer Science
{(LICS} '94), Paris, France, July 4-7, 1994},
pages = {208--212},
year = {1994},
url = {https://doi.org/10.1109/LICS.1994.316071},
doi = {10.1109/LICS.1994.316071},
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
biburl = {https://dblp.org/rec/conf/lics/HofmannS94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
author = {Martin Hofmann and Thomas Streicher},
title = {The Groupoid Model Refutes Uniqueness of Identity Proofs},
booktitle = {Proc. Symposium on Logic in Computer Science {(LICS} '94)},
longbooktitle = {Proceedings of the Ninth Annual Symposium on Logic in Computer Science
{(LICS} '94), Paris, France, July 4--7, 1994},
pages = {208--212},
year = {1994},
url = {https://doi.org/10.1109/LICS.1994.316071},
doi = {10.1109/LICS.1994.316071},
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
biburl = {https://dblp.org/rec/conf/lics/HofmannS94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/AbelCDTW20,
author = {Andreas Abel and
Jesper Cockx and
Dominique Devriese and
Amin Timany and
Philip Wadler},
title = {Leibniz equality is isomorphic to Martin-L{\"{o}}f identity,
parametrically},
journal = {J. Funct. Program.},
volume = {30},
pages = {e17},
year = {2020},
url = {https://doi.org/10.1017/S0956796820000155},
doi = {10.1017/S0956796820000155},
timestamp = {Mon, 29 Jun 2020 18:01:27 +0200},
biburl = {https://dblp.org/rec/journals/jfp/AbelCDTW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
author = {Andreas Abel and Jesper Cockx and
Dominique Devriese and Amin Timany and
Philip Wadler},
title = {Leibniz equality is isomorphic to Martin-L{\"{o}}f identity,
parametrically},
journal = {Journal of Functional Programming},
shortjournal = {J. Funct. Program.},
volume = {30},
pages = {e17},
year = {2020},
url = {https://doi.org/10.1017/S0956796820000155},
doi = {10.1017/S0956796820000155},
timestamp = {Mon, 29 Jun 2020 18:01:27 +0200},
biburl = {https://dblp.org/rec/journals/jfp/AbelCDTW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{Bishop1967-BISFOC-3,
title = {Foundations of Constructive Analysis},
author = {Errett Bishop},
publisher = {Mcgraw-Hill},
year = {1967}
title = {Foundations of Constructive Analysis},
author = {Errett Bishop},
publisher = {McGraw-Hill},
year = {1967}
}
@article{spitters_vanderweegen_2011,
title={Type classes for mathematics in type theory},
author={Spitters, Bas and van der Weegen, Eelis},
volume={21},
DOI={10.1017/S0960129511000119},
number={4},
journal={Mathematical Structures in Computer Science},
publisher={Cambridge University Press},
year={2011},
pages={795–825}}
@misc{selsam2020tabled,
title={Tabled Typeclass Resolution},
author={Daniel Selsam and Sebastian Ullrich and Leonardo de Moura},
year={2020},
eprint={2001.04301},
archivePrefix={arXiv},
primaryClass={cs.PL}
}
@article{Krebbers_2013,
title={Type classes for efficient exact real arithmetic in Coq},
volume={9},
ISSN={1860-5974},
url={http://dx.doi.org/10.2168/LMCS-9(1:1)2013},
DOI={10.2168/lmcs-9(1:1)2013},
number={1},
journal={Logical Methods in Computer Science},
publisher={Logical Methods in Computer Science e.V.},
author={Krebbers, Robbert and Spitters, Bas},
editor={Escardó, MartínEditor},
year={2013},
month={Feb}