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

[Lennart Augustsson]

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