[isabelle] fixed-point types?


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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.