[Haskell-cafe] Fixed point newtype confusion
wren ng thornton
wren at freegeek.org
Thu May 10 00:26:33 CEST 2012
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
More information about the Haskell-Cafe
mailing list