[Grace-core] Structural Typing vs Specifications

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

	Andrew