[Haskell] Type of y f = f . f

[David Menendez]

Jon Fairbairn writes:

> 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.

There are type systems which can type this, but they have their own
quirks. For example, System E [1] would give us:

    y :: (a -> b & b -> c) -> a -> c

where "a & b" is the intersection of types "a" and "b". The advantage of
System E over, say, System F, is that type inferencing is decidable. The
downside is that the inferred types can be pretty long.

[1] <http://www.macs.hw.ac.uk/~sebc/>
-- 
David Menendez <zednenem at psualum.com> <http://www.eyrie.org/~zednenem/>