Correction on our FoSSaCS 2001 paper
(1 February 2001, by Masahito Hasegawa)
In Section 7 (Conclusion and Further Work),
the dinaturality for the call-by-value fixpoint operator
is wrongly stated:
We do need these eta-expansions for the precise correspondence
with the dinaturality on the corresponding iterator.
We apologize for this sloppiness (we noticed this shortly after
submitting the final camera-ready...).
In fact, one can show that the first equation is operationally wrong,
by writing down simple ML programs F, G which invalidate it,
fun F (f:int->int) = (print "Hello"; fn x:int => x);
fun G (f:int->int) = (print "Bye"; fn x:int => x);
(* F, G : (int -> int) -> int -> int *)
Obviously, fix (G o F) 1 and G (fix (F o G)) 1 behave differently.
On the other hand, the second (corrected) equation is valid as the
eta-expansions prevent undesirable side-effects.
Similar seemingly-correct equations like fix F = fix (F o F)
are also invalidated by this example.
In the extended version (to appear in Higher-Order Symbolic Computation),
this mistake has been corrected.
Back to Hassei's
Research Page / Home Page