Re: in defense of types

[Michael Vanier <address@hidden>]

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)
      0
      (+ 1 (length (cdr lst)))))

You do this:

;; doesn't require recursion:
(define length
   (Y (lambda (len)
         (lambda (lst)
                 (if (null? lst)
                     0
                     (+ 1 (len (cdr lst))))))))

See "The Little Schemer", chapter 9, for more on this topic.
</note for people who've zoned out>

Mike


> From: Jaeyoun Chung <jay@kldp.org>
> Date: Thu, 30 May 2002 13:00:39 +0900
> 
> * Michael Vanier <mvanier@cs.caltech.edu> 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
>   forever!
> 
> 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 '_'
> 
>