[Grace-core] Structural Typing vs Specifications

[Kim Bruce]

I agree with Andrew, though I have additional reasons.  I agree that it is a non-problem in practice.  I've never seen anyone confusing a cowboy drawing a gun and an artist drawing a picture in a program.

My second reason is that to actually enforce the conformance of pre- and post-conditions is undecidable and would require a theorem-prover to come close to being useful.  While I like Eiffel's requirements to "or" preconditions on to those of the superclasses methods and the "and" postconditions, this is not likely to be of any use with structural types.

Kim



On Oct 14, 2011, at 9:45 AM, Andrew P. Black wrote:

> 
> On 14 Oct 2011, at 1:25, James Noble wrote:
> 
>> Hi all
>> 
>> an interesting point from a series of emails with Erik - who points out that:
>> 
>>> Any two methods named foo with type (int,int)->int are the same method, period.  This means that there is no way to ensure that the actual method implementation which is running when you call 'foo' is in any way related to the one you have been looking at in order to see its specification (pre/post-cond, comment, or whatever it has as its specification).
>> 
>> 
>> The problem is - say we want to put pre/post conditions on some type ---
>> 
>> type Cowboy = {
>> draw()   
>>     require {gun.holstered}
>>     ensure {gun.aimed}      
>> }
>> 
>> the type system will of course allow a Polygon
>> 
>> type Polygon = { draw () }  // draw on screen
>> 
>> Polygon is nothing to do with Cowboy but Grace would allow either to be assigned to the other. 
>> 
>> Nominal typing - or some form of branding - then seems essential for these kind of pre/post conditions to make sense.
> 
> 
> I don't see that.  What seems essential is that gun.holstered and gun.aimed (presumably self.gun.holstered and self.gun.aimed) are defined and are boolean-valued.   If that's not the case, then the assertion system can emit and error.  
> 
> The problem of "accidental conformance" is a non-problem in practice.
> 
> 	Andrew
> 
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core