2013 | OriginalPaper | Chapter
On Monadic Parametricity of Second-Order Functionals
Authors : Andrej Bauer, Martin Hofmann, Aleksandr Karbyshev
Published in: Foundations of Software Science and Computation Structures
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
How can one rigorously specify that a given ML functional
$f : (\texttt{int} \to \texttt{int}) \to \texttt{int}$
is
pure
, i.e.,
f
produces no computational effects except those produced by evaluation of its functional argument? In this paper, we introduce a semantic notion of
monadic parametricity
for second-order functionals which is a form of purity. We show that every monadically parametric
f
admits a question-answer strategy tree representation. We discuss possible applications of this notion, e.g., to the verification of generic fixpoint algorithms. The results are presented in two settings: a total set-theoretic setting and a partial domain-theoretic one. All proofs are formalized by means of the proof assistant
Coq
.