[PRL] Benjamin Pierce: Types Considered Harmful

[John Clements]

On May 30, 2008, at 8:32 AM, Felix S Klock II wrote:

>
> On May 30, 2008, at 10:15 AM, Dave Herman wrote:
>
>> Where's the beef?
>
>
> and on the subject of flesh:
>
> Can someone with more knowledge of contracts than myself please flesh
> out the last two bullets of slide 57 (page 29).  Please include (as
> ketchup) which meaning of the word "reasonable" Pierce is likely to be
> using here.
>
> (Better still, just point me at the appropriate reference.  I'll
> accept a chapter number in Robby Finder's thesis, or someone else's
> thesis, if that is where the information can be found, but I won't
> give credit for anything more coarse than that.)
>
> ((I'll admit I only spent a minute or three puzzling in my head before
> giving up on trying to interpret how both mappings are reasonable.  So
> maybe its obvious, but I would still appreciate an assist.))

I think I can do a bad enough job of explaining this that Robby or  
Matthias will jump in and correct me. Here goes.

Pierce's contracts differ from Findler's (old thesis work) in several  
ways.  Firstly, the contracts contain a pair of types, rather than a  
single type.  On the other hand, they contain a single blame label  
rather than two labels.

At the core of the difference, in my understanding, is what it means  
to use the trivially satisfied contract (let me call it "any".  In the  
"latent" world, attaching the "any" contract to an expression doesn't  
change the meaning of the program; you've added a runtime check that's  
guaranteed to succeed.  In the "manifest" world, though, this "any"  
contract will result in an expression with a type about which nothing  
is known, and therefore to which no operations can be applied (at  
least, in a language with parametricity).

I believe I can express this more succinctly in this way:

scheme's any: "we agreed on a totally nonrestrictive contract, so I  
can do anything I want with this value. "
ML's any: "I don't know anything about this value, so I can't do  
anything at all with it."

...

You'll notice that I carefully avoided picking which of these is  
contravariant and which is covariant; slide 58 makes more sense to me  
than slide 57. I believe that using Pierce's terminology, the latent  
system would be described as covariant. OTOH, I'm not convinced that  
this should actually be described as covariance.

John
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2484 bytes
Desc: not available
Url : https://lists.ccs.neu.edu/pipermail/prl/attachments/20080530/b9dde674/attachment-0001.bin