[racket-dev] promise vs polym contracts

On Jul 7, 2012, at 10:27 AM, Sam Tobin-Hochstadt wrote:

> Right, that's what I thought.  This is only different in that:
> 
>    (define v (delay (+ 1 2)))
>    (sum v) ; => v
> 
> Which means clients of `sum` now have to handle either Integers or
> Promises.  Is that intentional?


Yes. 

;; --- 

Overall I feel like Bob Harper when he called me to say that 
he had figured out ML got it all wrong with let after he had
read and understood the draft of Andrew's value restriction 
paper I had mailed him. Here is how he put it -- Omega has 
the wrong type on the right side of the let, you just don't 
notice. 

The real idea, which he developed a year later or so, was to 
map ML to a language with Lambda and then you see that let 
should be translated like this 

 [[ let x = e in e' ]] . = let x = Lambda it. [[e]]. in [[e']].

where it is the inferred possibly forall-quantified type. Now
you see that old ML shifted the semantics for Omega (and ref
and callcc etc) w/o knowing it. In the purely functional case --
which everyone uses for papers and stuff -- you don't notice
the "shift" from bottom to functional bottom or (which is what
I conjectured) there are errors in old proofs. 

-- Matthias, CPS 






> 
> On Sat, Jul 7, 2012 at 10:23 AM, Matthias Felleisen
> <matthias at ccs.neu.edu> wrote:
>> 
>> I may have made a mistake under time pressure:
>> 
>> [else (+ (force (sum (car x))) (force (sum (cdr x))))]
>> 
>> 
>> 
>> 
>> 
>> On Jul 7, 2012, at 10:19 AM, Sam Tobin-Hochstadt wrote:
>> 
>>> On Sat, Jul 7, 2012 at 10:14 AM, Matthias Felleisen
>>> <matthias at ccs.neu.edu> wrote:
>>> 
>>>> p.s. Sam's version forces too early because strict functions should
>>>> force not variable lookups. This is a common misconception among programmers.
>>>> I suspect it goes back to Abelson and Sussman getting it wrong (see what
>>>> happens if you don't understand the foundations).
>>> 
>>> I still don't think my version forces too early -- your alternative
>>> contains no calls to `force` at all.  Are you suggesting that I should
>>> `force` around the recursive calls to `sum`?  In that case, clients
>>> are exposed to promises, and the result type is (U Integer (Promise
>>> Integer)).  I can't tell from your description if you think that's an
>>> acceptable result.
>>> --
>>> sam th
>>> samth at ccs.neu.edu
>> 
> 
> 
> 
> -- 
> sam th
> samth at ccs.neu.edu