[Haskell] Type of y f = f . f

[Jon Fairbairn]

On 2005-02-28 at 18:03GMT Ben Rudiak-Gould wrote:
> Pedro Vasconcelos wrote:
>  >Jim Apple <japple at freeshell.org> wrote:
>  >>Is there a type we can give to
>  >>
>  >>y f = f . f
>  >>
>  >>y id
>  >>y head
>  >>y fst
>  >>
>  >>are all typeable?
>  >
>  >Using ghci:
>  >
>  >Prelude> let y f = f.f
>  >Prelude> :t y
>  >y :: forall c. (c -> c) -> c -> c
>  >
>  >So it admits principal type (a->a) -> a->a. From this you can see that
>  >(y head) and (y fst) cannot be typed, whereas (y id) can.
> 
> I think the OP's point is that all three of his examples make sense, and 
> the resulting functions would have Haskell types, yet there doesn't seem 
> to be a Haskell type which permits all three uses of y.

The problem is that the type system needs to be checkable,
so has to throw some information away.

if y f = f . f, the easiest way of losing information is to
require that the output type of f be the same as the
input. It certainly needs to be a type acceptable as input
to f.

if you put 

th f = f . f . f

the examples still make sense, but should the type of th be
different from the type of y?

> but I can't find a type which permits more than one.

Not in Haskell.  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

Now we can type
   d id 

   id :: ∀t . t → t
   so id :: ∀t . (λt.t) t → t
    ie b is (λt.t)
   so d id :: (λt.t)((λt.t) t) → t
    :: ∀t . t → t

and
   d head
    head:: ∀t.[t]→t
    so b is []
    so d head :: ∀t . [[t]] → t

and
   fst :: ∀x,y.(x,y)→x
   so b is λx.(x,y)
   d fst :: ∀t,y . (λx.(x,y))((λx.(x,y)) t) → t
	 :: ∀t,y . (λx.(x,y))(t,y) → t
	 :: ∀t,y . ((t,y),y) → t
	       (oops, only one y)

but you would be expecting a bit much of a compiler to infer
any of this.

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