On Jan 24, 2007, at 8:27 AM, Lennart Augustsson wrote:
Well, I think fix destroys parametricity too, and it would be better
to get rid of fix. But I'm not proposing to do that for Haskell,
because I don't have a viable proposal to do so. (But I think the
proposal would be along the same lines as the seq one; provide fix
in a type class so we can keep tabs on it.)
BTW, fix can be defined in the pure lambda calculus, just not in
simply
typed pure lambda calculus (when not qualified by "typed" the term
"lambda calculus" usually refers to the untyped version).
I think its important to point out here that fix _can_ be defined in
sufficiently rich typed lambda-calculi. You just need unrestricted
recursive types (iso-recursive is sufficient). Since Haskell has
those, you can't get rid of fix using typeclasses. You would also
need something like the strict positivity restriction, which is a
pretty heavyweight restriction.
<code>
newtype Mu a = Roll { unroll :: Mu a -> a }
omega :: a
omega = (\x -> (unroll x) x) (Roll (\x -> (unroll x) x))
fix :: (a -> a) -> a
fix f = (\x -> f . (unroll x) x) (Roll (\x -> f . (unroll x) x)) omega
ones :: [Int]
ones = fix (1:)
fibs :: [Int]
fibs = fix (\f a b -> a : f b (a+b)) 0 1
main = print $ take 20 fibs
</code>
FYI, don't try to run this in GHC, because it gives the simplifier fits.
[snip]
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
