Whiley / WhileyCompiler

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

Rethinking Runtime Type Test Operator ? #850

Closed DavePearce closed 5 years ago

DavePearce commented 6 years ago

Currently, the following program fails to compile:

type in_rec is {(int|null) f}
type ib_rec is {(int|bool) f}
type rec is in_rec | ib_rec

function write(rec x, int n) -> (rec r):
    //
    if x is in_rec:
        x.f = n
    else:
        x.f = n
    //
    return x

The reason for this is that, in the false branch, the type for x is {bool f}.

QUESTION: is that what we want?

DavePearce commented 6 years ago

IDEA: perhaps clarify the type test operator as a true selector? That is, given a union type, the purpose of the test is to select at most one term (and possibly only a partial one at that). This would allow the above to compile (which is perhaps more intuitive), and cause the following to fail:

type in_rec is {(int|null) f}
type ib_rec is {(int|bool) f}
type rec is in_rec | ib_rec

function write(rec x, int n) -> (rec r):
    //
    if x is {int f}:
        x.f = n
    else:
        x.f = n
    //
    return x

The reason for this is that it would be ambiguous as to whether in_rec or ib_rec was being selected.

DavePearce commented 6 years ago

Need an RFC. Things to think about:

DavePearce commented 5 years ago

Migrated to https://github.com/Whiley/RFCs/issues/36