Tag checks

[panagosg7]

Safe downcasts based on arbitrary tag checks.

https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/pos/misc/animals.ts https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/neg/misc/animals.ts

[ranjitjhala]

Btw, thinking about this a bit more, I think its better NOT to use the invariant mechanism, but instead, for now, to use the type alias mechanism. So you'd write something like:

predicate Inst X Key Val Type = keyVal(X, Key) = Val => instanceOf (X, Type)

use it to define:

predicate InstHorse  V = Inst V "kind" "horse" Horse
predicate InstSnake  V = Inst V "kind" "snake" Snake
predicate InstTiger   V = Inst V "kind" "tiger" Tiger
...

and use the above to write an alias:

type AnimalK = {v:Animal | InstHorse /\ InstSnake /\ InstTiger /\ ... }

Now, the crucial part is to just use AnimalK instead of Animal in all the ref-type specifications...

In short, once you add the:

1. keyVal measure -- that generalizes the hasKey predicate,
2. instanceOfmeasure -- that is used to check a downcast,

I think we should be able to support this idiom...

[panagosg7]

Sure, then I suppose we'd have to tweak the getProp operation here: https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/pos/misc/animals.ts#L14

To be something like this:

getProp :: 
  /\ forall A . (this: { [Immutable]f: A }) => { v: A | keyVal(this, "f") = v }
  /\ forall A . (this: { f: A }) => A

Where f in the first case is a "final" field.

[ranjitjhala]

Yes, nice!

On Oct 8, 2014, at 2:29 PM, Panagiotis Vekris notifications@github.com wrote:

Sure, then I suppose we'd have to tweak the getProp operation here: https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/pos/misc/animals.ts#L14

To be something like this:

getProp :: /\ forall A . (this: { [Immutable]f: A }) => { v: A | keyVal(this, "f") = v } /\ forall A . (this: { f: A }) => A Where f in the first case is a "final" field.

— Reply to this email directly or view it on GitHub.

[panagosg7]

This is almost done.

The changes I made revealed an issue that has to do with unification/subtyping with unions.

In particular, in:

number + tUndef `unify` tUndef + T0

It's hard for unification to figure out that T0 needs to be unified with number instead of number + tUndef. For such cases (perhaps for tNull) we could instead introduce a new type container that rids us of this disambiguation:

OrUndef t r, OrNull t r, ...

These containers cannot be parts of unions, but can enclose unions. Also:

OrUndef s `unify` OrUndef t = s `unfiy` t
TV `unfiy` OrUndef t = [TV := OrUndef t]
s `unify` OrUndef t = s `unify` t
-- etc.
t <: OrUndef t  -- because OrUndef t === t + tUndef

I think this will allow for a more straightforward encoding of optional object fields, which are a pretty common idiom.

[panagosg7]

Addressed by #58