<div class="gmail_quote">2009/3/19 Jens Blanck <span dir="ltr">&lt;<a href="mailto:jens.blanck@gmail.com">jens.blanck@gmail.com</a>&gt;</span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi,<br><br>I found myself writing the following<br><br>leastFixedPoint :: (Eq a) =&gt; (a -&gt; a) -&gt; a -&gt; a<br>leastFixedPoint f x = fst . head . dropWhile (uncurry (/=)) $ zip l (tail l)<br>    where l = iterate f x<br>

<br>and was a bit surprised that I couldn&#39;t get any matches on hoogle for the type above. The closest one is fix :: (a -&gt; a) -&gt; a but that sort of assumes that we&#39;re starting the fixed point search from the bottom element (undefined).<br>

<br>Anyway, is there a nicer way of doing the above?</blockquote><div><br></div><div>Well, it&#39;s probably not what you&#39;re looking for, but to remain true to the domain-theoretical roots of &quot;fix&quot;, the &quot;least fixed point above&quot; can be implemented as:</div>
<div><br></div><div>fixAbove f x = fix f `lub` x</div><div><br></div><div>Where lub is from the &quot;lub&quot; package on Hackage.  This function has the proof obligation that there is in fact any least fixed point above x (otherwise results are non-deterministic).</div>
<div><br></div><div>It still needs to be proven that fixAbove always returns a fixed point (given the precondition).  I can kinda see how it would, but I can&#39;t be sure that it does.</div><div><br></div><div>Luke</div>
</div>