Jon Fairbairn writes:
On 2005-02-28 at 18:03GMT Ben Rudiak-Gould wrote:
Pedro Vasconcelos wrote:
Jim Apple <japple@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@psualum.com> <http://www.eyrie.org/~zednenem/>