[Haskell] Re: Type of y f = f . f

[Jon Fairbairn]

On 2005-02-28 at 23:10EST Jim Apple wrote:
> Jon Fairbairn wrote:
> > If you allow quantification over higher
> > kinds, you can do something like this:
> > 
> >    d f = f . f
> > 
> >    d:: ∀a::*, b::*→*.(b a → a) → b (b a)→ a
> > 
> 
> What's the problem with
> 
> d :: (forall c . b c -> c) -> b (b a) -> a
> d f = f . f
> 
> to which ghci gives the type
> 
> d :: forall a b. (forall c. b c -> c) -> b (b a) -> a

It's too restrictive: it requires that the argument to d be
polymorphic, so if f:: [Int]->[Int], d f won't typecheck. It
also requires that the type of f have an application on the
lhs, so f :: Int->Int won't allow d f to typecheck either.

In the imaginary typesystem I was thinking of above, we
could instantiate b with (λx.x). As others have pointed out,
there are other typesystems that allow different types that
also work.

Incidentally, I think Ponder would have assigned types to
the examples, just not very useful ones; d head would have
come out as (μt.[t])->(μt.[t]) (assuming anything came out
at all).

-- 
Jón Fairbairn                              Jon.Fairbairn at cl.cam.ac.uk