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

[Robert Dockins]

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