Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?

like image 917
Ingun전인건 Avatar asked Jan 28 '20 15:01

Ingun전인건


Video Answer


2 Answers

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.

like image 165
chepner Avatar answered Sep 27 '22 20:09

chepner


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
like image 44
oisdk Avatar answered Sep 27 '22 21:09

oisdk