seq does not preclude parametricity (Re: [Haskell-cafe] IO is not a monad)

Robert Dockins robdockins at fastmail.fm
Wed Jan 24 10:41:09 EST 2007

```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

```