How the type `Fix` and function `fix` are same in Haskell?
Asked Answered
R

2

5

I'm trying to convince myself that type Fix and function fix are the same thing.
But I can't find the correlation between their definitions

-- definition of fix 
fix :: (p -> p) -> p
fix f = let {x = f x} in x -- or fix f = f (fix f)
-- definition of Fix
newtype Fix f = Fix { unFix :: f (Fix f) }

How does the constructor Fix fit into the form of (x -> x) -> x?

Royer answered 28/1, 2020 at 15:50 Comment(0)
I
9

Look at the kind of the type constructor Fix:

> :k Fix
Fix :: (* -> *) -> *

The type constructor Fix is what's analogous to the function fix.

The data constructor is something else. Following the explanation found in Understanding F-Algebras, Fix is an evaluator: it evaluates a term of type f (Fix f) to produce a value of type Fix f. This evaluation is lossless; you can recover the original value from the result using unFix.

Increscent answered 28/1, 2020 at 15:55 Comment(1)
I'm hoping the last paragraph is both sensible and correct.Increscent
A
6

Let's take the naive implementation of fix:

fix f = f (fix f)

For a function f, this creates something like the following:

f (f (f (f (f (f (f ...

The Fix newtype does the same, but for types. So if we take the type Maybe, we would want to create:

Maybe (Maybe (Maybe (Maybe (Maybe (Maybe ...

How would we create a function which constructs that type? We can first try with a type synonym:

--   fix f = f (fix f)
type Fix f = f (Fix f)

You should be able to see that this is the same as the naive implementation of fix above with some minor changes. But it's not legal Haskell!

This is for a number of reasons: mainly, Haskell doesn't allow infinite types like the Maybe example above, and Haskell's type system is strict, in contrast to the lazy evaluation required in fix. That's why we need a newtype. New type definitions (introduced with newtype or data) allow recursion, so we take our type synonym and change it into a newtype.

type    Fix f =                f (Fix f)
newtype Fix f =                f (Fix f)   -- change to newtype
newtype Fix f = Fix           (f (Fix f))  -- need to have a constructor
newtype Fix f = Fix { unFix :: f (Fix f) } -- And name the field, also
Armallas answered 28/1, 2020 at 16:26 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.