[PRL] Benjamin Pierce: Types Considered Harmful

[Robby Findler]

My FLOPS paper with Matthias Blume may help clarify this a little.

Robby

On Fri, May 30, 2008 at 5:00 PM, John Clements
<clements at brinckerhoff.org> wrote:
>
> 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