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

Lennart Augustsson lennart at augustsson.net
Wed Jan 24 19:49:11 EST 2007

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

```