search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
377 stars 81 forks source link

Unrestricted Recursion (tmFix) in TemplateMonad #377

Open fakusb opened 4 years ago

fakusb commented 4 years ago

Have there been thought on integrating an monadic operation to the TemplateMonad to allow unguarded recursion?

I have seen a few monadic programs defined in the monad requiring fuel to allow non-structural recursion. It seems to me that it should be possible to have a fixpoint operator tmFix : forall X, (X -> X) -> X -> TM X that removes the need for fuel. Or is there a theoretical/practical argument against having this?

gmalecha commented 4 years ago

This was also suggested in https://github.com/MetaCoq/metacoq/pull/133

gmalecha commented 4 years ago

An alternative is to make the definition coinductive, which would also work and might make it possible to prove termination after the fact using existing Coq mechanisms.

mattam82 commented 4 years ago

We could add this, but one can already rely on unchecked fixpoints in Coq, no?

JasonGross commented 1 year ago

Implemented for the non-extractable monad in #790.