[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: in defense of types

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

```