[Grace-core] Structural Typing vs Specifications

[Erik Ernst]

Den 14/10/2011 kl. 17.45 skrev Andrew P. Black:

> 
> 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.

Hello Andrew,

it may be rare, but if you ask Smalltalkers then they definitely consider 'doesNotUnderstand:' to be rare, too (unless it's being used for some fancy purpose). Still, many people prefer to pay for having static types because they want to increase the confidence that we can have in the absence of that particular type of problem.  Also, larger systems (millions of lines of code) probably correlate with more name clashes and a smaller likelihood that the programmer spots the problem immediately.  Using composition of mixins/traits extensively would probably also create more name clashes (compared to traditional single inheritance), and creating the compositions based on objects rather than classes (presumably with a subsumption step somewhere, such that we only know an upper bound of the classes of those objects) would again add to the opportunities for messing up conceptually distinct features with the same name.  The worst cases would be the ones where two methods are very similar semantically, but are based on different contracts (pre/post cond.), because that would be hard to look up if there is no well-defined place to see what the contract is.

Maybe one take on this could be to enable every feature (method, in particular) to declare that it is associated with a given "meaning", which could just be an opaque token to distinguish it from other "meanings", or it could be a full-fledged contract, or many other things.  It would be very heavy to actually have such an annotation on each method, but a set of implemented interfaces along with some disambiguation might be useful (so this is the Set.add implementation, and here's the Bag.add implementation), in order to avoid long annotations on every single declaration.  In this case two methods 'int foo(int)' with "meaning" A and B, respectively, would never override each other if A!=B (they would then co-exist as distinct methods), and whoever wishes to read and check the implementation of one of those methods would know exactly where to look for the specification.  A compiler could then give a warning as soon as a given class implements two interfaces with clashing names, and the user could then eliminate the warning by adding an annotation to each method about which interface it is (conceptually and technically) associated with.

For code that doesn't carry the burden of all those interfaces the name clashes could happen, and conceptually different methods could accidentally be identified as "the same method" and categorized as an overriding and an overridden method, but this is just an extra potential error at runtime just like 'doesNotUnderstand:', and programmers must find a balance that fits the purpose.

Back to square one:  Those interfaces would be extremely nominal if it's supposed to do any good.  ;-)

  best regards,

-- 
Erik Ernst - eernst at cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark