[Grace-core] Structural Typing vs Specifications

[Erik Ernst]

Den 14/10/2011 kl. 09.25 skrev James Noble:

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


Just an additional comment:  I don't even think nominal typing is sufficient.  Witness, e.g., the fact that Scala prevents "inheriting from a virtual" (using an abstract type member as a superclass) exactly because this would enable (in Java-like syntax) the following kind of unsound overriding:

  class A {}

  class B extends A { Cowboy x = foo(); Cowboy foo(){..} }

  class B_as_A = (class A) class B;  // some language mechanism that allows us to denote the class B with A as the statically known type

  class C extends B_as_A { String foo(){..}}

Unless we take care, x will be initialized with a String in a 'new C()', because the most specific foo method in that object returns a String.  Neither the declaration in B nor the one in C is type incorrect as seen locally.

I consider this to be a type-level example of the same thing as the contract/specification level issue that James describes.  But contracts may be more interesting because they are relevant for correctness of code that is not subject to compile time type analysis, and in that case it is very easy to denote a class (like B) without knowing its full specification (like B_as_A).

The trick I'm using in gbeta to define this problem out of the way is to use static name binding to attributes (declarations/slots) whose values are dynamically bound, and then the two 'foo' methods would simply be unrelated and allowed to coexist peacefully.  ;-)

  best regards,

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