search

Whiley / RFCs

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

RFC/subtyping #51

Closed DavePearce closed 5 years ago

DavePearce commented 5 years ago

See: https://github.com/DavePearce/RFCs/blob/rfc/subtyping/text/0000-subtyping.md

DavePearce commented 5 years ago

So, having almost completed a reference implementation, at least one significant issue has arisen. The following no longer type checks:

nat i = 0
i = i + 1

This is actually quite a big deal as we can no longer do much with constrained primitive types. We can of course implement the above as:

nat i = 0
i = (nat) i + 1

This forces the verification check at the point of the cast which is, in some sense, what we want. However, it is pretty ugly as well sadly.

DavePearce commented 5 years ago

In fact, quite a few situations arise with integer constants. For example, even this doesn't currently compile:

nat i = 0

That's because the type of 0 is, of course, int. This can actually be resolved using forward type inference. However, the FlowTypeChecker currently does not actually implement this. Another common example is the following:

   if x == 0:

Again, this comes back saying we have incomparable operands. Potentially, this can be resolved by adjusting the requirements for equality. Specifically, to just employ the underlying type for determining whether an equality is permitted or not.