[Haskell-cafe] Fixed point newtype confusion

[wren ng thornton]

On 5/8/12 8:24 PM, Sebastien Zany wrote:
> Hmm, I don't understand how that would work.

Using one of the fundep versions:

     class (Functor f) => Fixpoint f x | ... where
         fix :: f x -> x
         unfix :: x -> f x

We'd define instances like the following:

     data List a = Nil | Cons a (List a)

     data PreList a b = PNil | PCons a b
         deriving Functor

     instance Fixpoint (PreList a) (List a) where
         -- fix :: PreList a (List a) -> List a
         fix PNil         = Nil
         fix (PCons x xs) = Cons x xs

         -- unfix :: List a -> PreList a (List a)
         unfix Nil         = PNil
         unfix (Cons x xs) = PCons x xs

Or we could do:

     newtype Fix f = Fix { unFix :: f (Fix f) }

     instance Fixpoint (PreList a) (Fix (PreList a)) where
         -- fix :: PreList a (Fix (PreList a)) -> Fix (PreList a)
         fix = Fix

         -- unfix :: Fix (PreList a) -> PreList a (Fix (PreList a))
         unfix = unFix


> I wish I could define something like this:
>
> class (Functor f) =>  Fixpoint f x | x ->  f where
>      fix :: x ->  Fix f
>
> instance (Functor f) =>  Fixpoint f (forall a. f a) where
>      fix = id
>
> instance (Functor f, Fixpoint f x) =>  Fixpoint f (f x) where
>      fix = Fix . fmap fix
>
> but instances with polymorphic types aren't allowed. (Why is that?)


Well, one problem is that (forall a. f a) is not a fixed-point of f. 
That is, f (forall a. f a) is not isomorphic to (forall a. f a)


Another problem is that (forall a. f a) isn't exactly of kind *. It sort 
of is, but since it's quantifying over * you get into (im)predicativity 
issues. For example, do we allow the following type?

     Maybe (forall a. f a)

Depending on what language extensions you have on and which version of 
GHC you're using, the answer could be yes or it could be no. There isn't 
a "right answer" per se, it just depends on what you want the semantics 
of the type system to be and what other features you want to have.


Another problem is, I don't think that means what you think it means. 
Supposing we were to allow it, the expanded type of the first instance 
of fix would be:

     fix :: (forall a. f a) -> Fix f

Which is isomorphic to

     fix :: exists a. f a -> Fix f

Which means that supposing we have some (f A) where A is some unknown 
but defined type, then we can turn it into Fix f. The only way that 
could be possible is if we throw away all the As that occur in the (f 
A). But that's not what you mean, nor what you want.



> Alternatively if I could write a function that could turn
>
> e :: forall a. F (F (F ... (F a) ... ))
>
> into
>
> specialize e :: F (F (F ... (F X) ... ))
>
> that would work too, but I don't see how that's possible.

Yeah, that'd be nice. In System F, or in Haskell Core, the "forall a. b" 
is treated like a special version of the function arrow. So we have a 
big lambda for type abstraction (written "/\" below), and we have type 
application (written in Core with "@"). Thus we know that e is eta 
equivalent to:

     (/\a. e @a) :: forall a. F (F (F ... (F a) ... ))

This is just like saying that given any function f :: A -> B, it is eta 
equivalent to (\(x::A). f x) :: A -> B.

So if we wanted a version of e monomorphized on a = X, then we'd just say:

     e @X :: forall a. F (F (F ... (F X) ... ))

There are tricks for gaining access to the type abstraction and type 
application of Core, but they're all fairly fragile as I recall.

-- 
Live well,
~wren