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