Whiley / RFCs

Request for Comment (RFC) proposals for substantial changes to the Whiley language.
3 stars 2 forks source link

Syntax for Object Invocation #67

Open DavePearce opened 4 years ago

DavePearce commented 4 years ago

(see also #41)

Here's a simple example of the proposed syntax:

type Channel<T> is {
  method read(this) -> T
  method write(this, T),
  ...
}

Here, this is an existential type which refers to the actual type of the object in question. For example, we might define a BufferChannel<T> like this:

type BufferChannel<T> is { T[] data, int rp, int wp, ... }
where rp <= wp && wp <= |data|

method read<T>(BufferChannel<T> self) -> (BufferChannel<T> 'self, T item):
   ...

method create<T>(int size) -> Channel<T>:
   return {
     data: [0; size],
     rp: 0,
     wp: 0,
     read: &read(BufferChannel<T>),
     write: &write(BufferChannel<T>,byte)
   }

In order to use a channel, we introduce the object invocation syntax e!m(e,..e). For example, the following illustrates:

Channel<int> c = create(10)
c!write(1)
int i = c!read()

Here, c!write(1) is syntactic sugar for c.write(c,1). A key challenge is how to handle the returned state.