[Haskell] Type of y f = f . f
David Menendez
zednenem at psualum.com
Mon Feb 28 19:30:06 EST 2005
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/>
More information about the Haskell
mailing list