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