Limiting the value recursion is not enough, of course. You'd have to limit the type recursion as well. -- Lennart On Jan 24, 2007, at 10:41 , Robert Dockins wrote:
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