search

Whiley / RFCs

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

Ownership in Whiley #32

Open DavePearce opened 5 years ago

DavePearce commented 5 years ago

Given the recent addition of lifetimes (#642), the next question is: what about ownership?

An interesting approach to ownership is to try and leverage the verification system for this. Here's an example (using template syntax from #540):

template
type unique is (&T r) where |>r<| == 1

Here, we've defined the concept of a unique pointer. The syntax |> r <| returns the number of inbound references to the item referred to by r. Since the constraint ensures that there is only one inbound reference, we know r is a unique reference.

This raises the further question: what else could we do with this syntax?

DavePearce commented 5 years ago

Migrated from https://github.com/Whiley/WhileyCompiler/issues/646