Email Gateway (Aug 19 2022 at 15:44): Email Gateway (Aug 19 2022 at 15:44):From: Eddy Westbrook <westbrook@kestrel.edu>
Hi,
I was wondering if there is any way to directly construct a fixed-point type in Isabelle, without (at least, without directly) using datatypes. That is, I have a type constructor F x, and I would like to construct a fixed-point type tau = F tau. Any ideas on how to go about this? Of course, this should only be possible if F is a functor, since otherwise it doesn’t have a fixed-point.
In more detail, I am trying to axiomatize the resumption monad transformer, as follows. I start by declaring the underlying monad type, as follows:
typedecl ‘a Monad
By positing the monad laws as axioms, I am assured that Monad is a functor. Then I would like to define the resumption transformer like this:
datatype 'a ResumpT
= Done 'a
| Pause "('a ResumpT) Monad"
Of course, this is not a valid datatype, because Isabelle does not know that Monad is positive. I was thinking, however, that I could turn ResumpT into a type-level function, as follows:
datatype (‘a, ’t) ResumpT
= Done 'a
| Pause “’t Monad"
Then, if I could build a fixed-point type over the ’t type argument, I would by able to define ResumpT, at least indirectly.
Any help on this front would be appreciated.
Thanks,
-Eddy
Email Gateway (Aug 19 2022 at 15:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eddy,
Of course you can construct your fixpoint type manually, but this will be a lot of work.
Or, you just continue to axiomatize the structure of the resumption monad transformer,
too, but axioms are better avoided.
The new datatype package might, however, offer a solution, because it supports fixpoint
types for natural functors that are bounded. Boundedness means that the cardinality of
the elements of the type is bounded by some cardinal that does not depend on the type
variable over which the fixpoint is built. To that end, you have to register your monad
type as a BNF.
In Isabelle2013-2, you have to import the BNF package via "~~/src/HOL/BNF/BNF", in the
coming Isabelle2014 release, the datatype_new command will already be part of Main. The
tutorial on datatypes tells you what is needed and provides further references.
By the way, I would also suggest to think about taking the greatest fixpoint (codatatype)
rather than the least (datatype) for ResumpT. Then you can also reason about possibly
infinite computations.
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:44):From: Eddy Westbrook <westbrook@kestrel.edu>
Andreas,
The new datatype package sounds pretty cool, if it can do all the things that you say here. I will definitely try it out… as soon as we upgrade our tool to work with the latest Isabelle. But now, we will have an excuse. :)
Thanks so much for getting back to me, and for the helpful pointers!
-Eddy
Last updated: Nov 21 2024 at 12:39 UTC