From e68b56e938f134865c837b5c090eb316867451fa Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Mon, 10 Feb 2020 15:47:15 -0800 Subject: [PATCH] Add a note about the type of mfix --- src/Control/Monad/Fix.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Control/Monad/Fix.v b/src/Control/Monad/Fix.v index 59f9c93..893ebc9 100644 --- a/src/Control/Monad/Fix.v +++ b/src/Control/Monad/Fix.v @@ -10,7 +10,14 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. (****************************************************************************** - * The State Monad + * The MonadFix class + * + * Note that the type of `mfix` here is quite different from Haskell's + * @(T -> m U) -> m U@, and this is due to the call-by-value nature of Coq. + * For more information on this encoding and what it means, see the article + * "Axioms for Recursion in Call-by-Val": + * + * http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.2580&rep=rep1&type=pdf *) Class MonadFix (m : Type -> Type) : Type := {