[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: in defense of types
Michael Vanier <email@example.com> writes:
> > let z f = (fun x -> f (fun z -> x x z)) (fun x -> f (fun z -> x x z));;
> > is not typable. since two 'x' in 'x x z' cannot have the same type.
> > The key point is distinguish the type of these instances of 'x'.
> > # type 'a t = I of ('a t -> 'a);;
> > type 'a t = I of ('a t -> 'a)
> > # let z f = (function I x -> f (fun z -> x (I x) z))
> > (I (function I x -> f (fun z -> x (I x) z)));;
> > val z : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
> > voila! you can type it. Now, let's try simple example.
> This is a brilliant and non-obvious demonstration; thanks a lot! You saved
> me hours of scratching my head ;-)
> BTW I'm not sure what you mean when you say that Y is not usable in eager
> languages. You can define Y in scheme, which is eager. Do you mean in
> eager statically-typed languages?
I don't understand either. And isn't this much simpler and working:
let rec y f e = f (y f) e
let ffact f n = if n = 1 then 1 else n * f (n - 1)
y ffact 5