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

*To*: Michael Vanier <address@hidden>*Subject*: Re: in defense of types*From*: Jaeyoun Chung <address@hidden>*Date*: Thu, 30 May 2002 13:00:39 +0900*Cc*: address@hidden, address@hidden*In-reply-to*: <200205292327.g4TNRaL11580@orchestra.cs.caltech.edu> (MichaelVanier's message of "Wed, 29 May 2002 16:27:36 -0700")*References*: <20020529172958.1945.qmail@mail.archub.org><200205292327.g4TNRaL11580@orchestra.cs.caltech.edu>*Reply-to*: address@hidden*Sender*: address@hidden*User-agent*: Gnus/5.090007 (Oort Gnus v0.07) Emacs/21.3.50(i386-msvc-nt5.0.2195)

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

**Follow-Ups**:**Re: in defense of types***From:*Michael Vanier <mvanier@cs.caltech.edu>

**References**:**Re: in defense of types***From:*Paul Graham <pg@archub.org>

**Re: in defense of types***From:*Michael Vanier <mvanier@cs.caltech.edu>

- Prev by Date:
**RE: Macros and little languages** - Next by Date:
**RE: Macros and little languages** - Previous by thread:
**Re: in defense of types** - Next by thread:
**Re: in defense of types** - Index(es):