Email Gateway (Aug 22 2022 at 17:07): Email Gateway (Aug 22 2022 at 17:07):From: Tobias Nipkow <nipkow@in.tum.de>
Bounded Natural Functors with Covariance and Contravariance
Andreas Lochbihler and Joshua Schneider
Bounded natural functors (BNFs) provide a modular framework for the construction
of (co)datatypes in higher-order logic. Their functorial operations, the mapper
and relator, are restricted to a subset of the parameters, namely those where
recursion can take place. For certain applications, such as free theorems, data
refinement, quotients, and generalised rewriting, it is desirable that these
operations do not ignore the other parameters. In this article, we formalise the
generalisation BNF_CC that extends the mapper and relator to covariant and
contravariant parameters. We show that
subtypes inherit the BNF_CC structure under conditions that generalise those
for the BNF case, and
BNF_CCs preserve quotients under mild conditions.
These proofs are carried out for abstract BNF_CCs similar to the AFP entry BNF
Operations. In addition, we apply the BNF_CC theory to several concrete functors.
https://www.isa-afp.org/entries/BNF_CC.html
Enjoy!
smime.p7s
Email Gateway (Aug 22 2022 at 17:07):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Tobias Nipkow wrote:
Bounded Natural Functors with Covariance and Contravariance
Andreas Lochbihler and Joshua Schneider
[...]
I'm not sure if I understand this correctly. Could this bring us closer
to obtaining a map function for 'a set, and hence for datatypes
involving sets?
datatype 'a foo = foo "('a × 'a) set"
(* no map_foo is provided since none of the arguments admit recursion *)
(The argument of set is special in that it admits both a contravariant
view (by viewing sets as predicates) and a covariant view with the
f ` X being corresponding map function -- it's the latter that I would
like to have as a map function...)
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 17:07):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Bertram,
You are right. This entry provides exactly the theory for getting such a map function (and
also a relator). For your example, you would precisely get the covariant map (but you
still cannot do (co)datatype recursion through such non-live covariant arguments). You can
also go crazy as in
datatype ('a, 'b) bar = Bar "(('a * 'a) set => 'b) => 'a list"
The construction gives you a map function that is covariant in 'a and contravariant in 'b.
The entry formalises the constructions for an abstract functor and for a few examples.
There's no automation yet, so you have to intelligently copy-n-paste. I have used these
constructions and proofs for quite complicated (co)datatypes. Joshua and I have a paper on
the theory at ITP this year. A preliminary draft is available on my homepage:
http://www.andreas-lochbihler.de/pub/lochbihlerschneider2018.pdf
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC