[Haskell-cafe] Master's thesis topic sought
wren ng thornton
wren at freegeek.org
Sat Nov 7 15:46:30 EST 2009
Matus Tejiscak wrote:
> On Pi, 2009-11-06 at 17:25 -0500, Brent Yorgey wrote:
>> On Fri, Nov 06, 2009 at 03:29:47PM +0000, Stephen Tetley wrote:
>>> Hello all,
>>> Are any of the of the more exotic recursion schemes definable without
>>> a least-fixed point /Mu/ type?
>> Note that Haskell datatypes have a built-in implicit "mu" (that is,
> I'd say Mu gets you a greatest-fixed point. I don't have a proof, I just
> note that Mu(ΛX. 1 + A x X) contains infinite lists, too.
Mu is the notation for least-fixed, Nu is the notation for
greatest-fixed. In Haskell, the two fixed points coincide due to
laziness and _|_.
> I wonder whether this is a problem; if I want to define an initial
> algebra of a functor, I should take a least fixed point (if I understand
> it correctly) -- but all I have is Mu. Inductively defined functions
> will loop on infinite lists, which are included in the resulting type,
> and -- i imagine -- the type system might prevent such errors, by not
> enabling casting from greatest-Mu(F) to least-Mu(F). But that's probably
> too restrictive to be useful.
If you want the type system to catch infinite looping like this, then
you'll need to switch to a total functional programming language which
distinguishes data and codata (and hence what can be inducted on vs what
needs to be coinducted on).
More information about the Haskell-Cafe