[Haskell] Type of y f = f . f
Jon Fairbairn
Jon.Fairbairn at cl.cam.ac.uk
Mon Feb 28 17:57:33 EST 2005
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.
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
More information about the Haskell
mailing list