Re: in defense of types

[Jaeyoun Chung <address@hidden>]

* 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 '_'