Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: Undefined evaluation order
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John R Harrison <johnh@i...>
Subject: Re: Undefined evaluation order

In the old ML compiler used in Cambridge LCF and HOL88 (which I guess was
a kind of ur-CAML), the order of evaluation was genuinely changeable, e.g:

   #let f x y = (x,y);;
   f = - : (* -> ** -> (* # **))

   #f (print_int 1;100) (print_int 2;200);;
   21(100, 200) : (int # int)

   #(I f) (print_int 1;100) (print_int 2;200);;
   12(100, 200) : (int # int)

We just ended up saying in HOL's DESCRIPTION manual:

   "Due to optimizations in the ML compiler, the order of evaluation
    may vary."

Gerard Huet might have been responsible for the optimizations that led to
this behaviour, so perhaps he knows more...

Cheers,

John.