[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: in defense of types
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?
<note for people who've zoned out>
The Y combinator is a way of creating recursive functions in a language
which doesn't necessarily support them directly. So instead of defining a
function to find the length of a list as:
;; requires recursion:
(define (length lst)
(if (null? lst)
(+ 1 (length (cdr lst)))))
You do this:
;; doesn't require recursion:
(Y (lambda (len)
(if (null? lst)
(+ 1 (len (cdr lst))))))))
See "The Little Schemer", chapter 9, for more on this topic.
</note for people who've zoned out>
> From: Jaeyoun Chung <firstname.lastname@example.org>
> Date: Thu, 30 May 2002 13:00:39 +0900
> * Michael Vanier <email@example.com> at 2002-05-29 16:27-0700
> | There is a cost in flexibility (I don't think you can write the Y
> | combinator in ocaml, for instance ;-)), but it's much less than most
> | people assume.
> Actually, yes! You can make Z (equiv with Y with one step eta
> conversion)combinator typeable in ML family language. Note that Y is not
> usable in eage language in which the fixpoint function will simply loop
> 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.
> # let f = fun f -> fun n -> if n = 1 then 1 else n * (f (n - 1));;
> val f : (int -> int) -> int -> int = <fun>
> # z f ;;
> - : int -> int = <fun>
> as we expected. and
> # z f 5;;
> - : int = 120
> The true value of static typing of ML style type system is that it makes
> sure the invariant at compile time based on the rigid theory. You
> can encode the invariants of your program into to type.
> jay@_kldp_._org_ sans '_'