[Grace-core] Structural Typing vs Specifications

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

James