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

*To*: address@hidden*Subject*: Re: in defense of types*From*: Michael Vanier <address@hidden>*Date*: Wed, 29 May 2002 22:55:05 -0700*Cc*: address@hidden, address@hidden*In-reply-to*: <6616qo7s.fsf@kldp.org> (message from Jaeyoun Chung on Thu, 30May 2002 13:00:39 +0900)*References*: <20020529172958.1945.qmail@mail.archub.org><200205292327.g4TNRaL11580@orchestra.cs.caltech.edu> <6616qo7s.fsf@kldp.org>*Sender*: 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 '_' > >

**Follow-Ups**:**Re: in defense of types***From:*Lauri Alanko <la@iki.fi>

**Re: in defense of types***From:*Pixel <pixel@mandrakesoft.com>

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

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

**Re: in defense of types***From:*Jaeyoun Chung <jay@kldp.org>

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