Jon Fairbairn writes: > On 2005-02-28 at 18:03GMT Ben Rudiak-Gould wrote: > > Pedro Vasconcelos wrote: > > >Jim Apple <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell