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.
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
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
