[Haskell-cafe] Master's thesis topic sought

[Matus Tejiscak]

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.

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.

Anyway, is there a possibility to restrict Mu to a least-fixed-point
operator?

Matus