Whiley / WhileyCompiler

The Whiley Compiler (WyC)
http://whiley.org
Apache License 2.0
219 stars 36 forks source link

Removing Tuples Types? #537

Closed DavePearce closed 8 years ago

DavePearce commented 9 years ago

An interesting question is whether or not we can actually remove tuple types altogether. My reasoning for this is:

  1. Tuple types are an additional point of complexity. In particular, there is currently confusion over the parameters/return to a function and whether or not they should be a tuple. This has been largely a disaster in WyCS and I don't want to repeat that.
  2. Tuple types are not used that much. In general, tuple types are mostly used for multiple returns. Therefore, we can support multiple return values explicitly along with destructuring syntax whilst still getting rid of tuples.
  3. Tuples are useful, but records provide a good alternative. Although one of my big gripes with Java was the lack of support for tuples, part of the reason for this is that there is no lightweight alternative. In Whiley, record types are a light weight alternative which provide very little additional overhead compared with tuples. Hence, in the few cases we really want tuples, we can just use records instead.

To support this, I think it would be quite useful to examine the use of tuple types in my benchmarks and test cases.

DavePearce commented 9 years ago

From 0XX benchmark series, have the following observations:

  1. 006_queens uses a tuple (int,int)[].
  2. 009_lz77, 011_codejam, 012_cyclic use multiple return values.

In 006_queens the tuple is use to represent a position on the board:

type Pos is (int,int)

Realistically, this would be better anyway:

type Pos is {int x, int y}
DavePearce commented 9 years ago

One of the big challenges here, however, is: what type to give functions which return multiple values?

A few points on this:

  1. Could retain tuple type specifically for this purpose. In this case, there would be no source-level syntax for the tuple type. However, this would then need to be at the WyIL level as well?
  2. Could have specific syntax for multi-assignment function/method invocations. Then we would update the invoke bytecode to support multiple assignment as well.
DavePearce commented 8 years ago

Right, I'm closing this now as it's essentially now resolved. The remaining issues are split out separately into #566 (fields in invariants), #565 (multiple returns), #339 (flow typing field accesses), #552 (which should be reopened)