The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Jean-Francois Monin wrote:
> You may have a look in the contribs from Lannion about exceptions,
> and my related paper in SCP.
>
> In summary, it is a kind of CPS translation where the result and its
> type need to be local (rather than global as usual). In particular,
> for ensuring modularity: a function raising an exception has a meaning
> indepandantly from its context. When a recursive call is embedded
> inside a "try with" construct, impredicativity comes naturally into
> play.
>
> The contrib uses impredicative Set.
>
> [...]
>
> On Sat, Aug 27, 2011 at 08:20:38AM -0400, Adam Chlipala wrote:
>    
> > Even without such an axiom, it already has a richer notion than in
> > [Set], because [Prop] allows impredicativity, but my suspicion is
> > that few proofs make deep use of impredicativity.  (Does anyone have
> > a non-contrived counterexample to that suspicion?)

I don't doubt that impredicativity can be useful for modeling 
impredicative polymorphism in programming languages, which I'm guessing 
is a reasonable explanation of what happens in your development.  My 
original curiosity was about impredicativity in [Prop], not [Set], though.