Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More clarifications and tweaks #91

Merged
merged 5 commits into from
Jun 5, 2020
Merged

More clarifications and tweaks #91

merged 5 commits into from
Jun 5, 2020

Conversation

rossberg
Copy link
Member

Following implementation feedback from @lukewagner, @jakobkummerow, and @tebbi, includes the following changes:

  • RTT types include a natural number tracking their inheritance depth, in order to actually enable efficient casts.
  • Disallow struct/array.new to take a super-RTT, in order to allow direct representation of RTTs as map/shape objects without hidden dynamic allocation. We could still provide partial type hiding via another RTT allocation instruction, but that can be deferred.
  • Fully type-annotate RTT-related instructions for now.
  • Renamed constype to heaptype, as in funcref repo.

More to come...

@rossberg
Copy link
Member Author

@jakobkummerow, PTAL. For some reason, GH doesn't allow me to add you as a reviewer.

@binji
Copy link
Member

binji commented May 28, 2020

@jakobkummerow, PTAL. For some reason, GH doesn't allow me to add you as a reviewer.

I've added him as a contributor, you should be able add him after he accepts the invitation.

* `i31` is a new constructed type
- `constype ::= ... | 31`
* `i31` is a new heap type
- `heaptype ::= ... | 31`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i31?

@taralx
Copy link

taralx commented May 30, 2020

The array.new* instructions still accept a super-RTT, is that intentional?

@binji binji requested a review from jakobkummerow June 1, 2020 16:05
@rossberg
Copy link
Member Author

rossberg commented Jun 2, 2020

Thanks @taralx, both fixed.

* `rtt.canon <constype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt t)]`
* `rtt.canon <heaptype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt 0 t)]`
- multiple invocations of this instruction yield the same observable RTTs
- this is a *constant instruction*
- equivalent to `(rtt.sub t (rtt.canon any))`, except when `t` itself is `any`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the type of (rtt.canon any)? Does n go negative, or is the typing of rtt.sub different for any?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, good catch! Wrt handling any this was off by one. Fixed rule and description to something more sensible.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line is also missing the <n> update to rtt.sub. Also, rtt.sub n t1 t2 wants t1 to be the supertype. So I think it should be (rtt.sub 1 (rtt.canon any) t).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes, fixed (it's (rtt.sub 1 any t (rtt.canon any))).

Copy link
Contributor

@jakobkummerow jakobkummerow left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me.

* `rtt.canon <constype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt t)]`
* `rtt.canon <heaptype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt 0 t)]`
- multiple invocations of this instruction yield the same observable RTTs
- this is a *constant instruction*
- equivalent to `(rtt.sub t (rtt.canon any))`, except when `t` itself is `any`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line is also missing the <n> update to rtt.sub. Also, rtt.sub n t1 t2 wants t1 to be the supertype. So I think it should be (rtt.sub 1 (rtt.canon any) t).

@@ -186,34 +203,32 @@ Perhaps add the following short-hands:
* `struct.new <typeidx>` allocates a structure of type `$t` and initialises its fields with given values
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Didn't we talk about dropping the rtt-less variants of struct.new? Am I misremembering, or have you changed your mind, or is that postponed until after further/wider discussion?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

- iff `$t = struct (mut t)*`
- and `(type $t) <: t'`
- and `(type $t) == t'`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused by the (type $t) part. Isn't $t a type? What does (type ...) do? Also, I assume == is equivalent to = in the line above? I would have expected to see just $t = t' here, at which point we might as well drop t' and use $t directly instead: (rtt n $t)

If I get to make further wishes: I find the t* part confusing too, because that's not a repeated sequence of a single t type. Maybe at least add an explanation "t* means a sequence of stack values whose types match the struct definition of $t"? Or rephrase the formal definition as something like:

struct.new_with_rtt $t : [(rtt n $t) x y z...] -> [(ref $t)] iff $t = (struct (mut x) (mut y) (mut z)...)

(which would have the additional benefit that it makes more obvious that the value for the last field is the topmost stack value -- which is arguably intuitive but doesn't hurt to spell out explicitly).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused by the (type $t) part. Isn't $t a type?

It's a "type use" referring to $t, see the new definition of heap types. The extra keyword avoids ambiguity in some syntactic contexts and is more consistent with other syntax. Note that (ref $t) is defined as a shorthand for (ref (type $t)).

FWIW, I just removed the type annotation on the instruction, because with type equivalence it can be derived from the operand type.

If I get to make further wishes: I find the t* part confusing too, because that's not a repeated sequence of a single t type.

It's a sequence of possibly different value types. It's a notational convention that is used heavily in the spec, explained here.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just removed the type annotation on the instruction, because with type equivalence it can be derived from the operand type.

I generally agree with removing the redundancy; but I think the current specification [(rtt n t) t'*] isn't implementable: we can't find the rtt on the value stack if we don't know how many t' there are, which in turn we can only determine from the rtt. I can see several solutions:
(1) go back to having a type immediate
(2) add an arity immediate (equalling n, indicating the number of t' stack values)
(3) swap the order of the stack arguments to [t'* (rtt n t)]

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes, good catch, that's ambiguous. I reinstated the type immediate. I figure that if we want to remove it, we should do so consistently along with the other instructions anyway.

```
(type $A (struct))
(type $B (struct (field i32)))
(type $C (struct (field i32 i64)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd suggest to abbreviate a little less: (struct (field i32) (field i64))

- multiple invocations of this instruction with the same operand yield the same observable RTTs
- this is a *constant instruction*

TODO: Add the ability to generate new (non-canonical) RTT values to implement casting in nominal type hierarchies.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you just want to go ahead and add rtt.fresh which is the same as rtt.sub except for the line "multiple invocations ..."?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not yet, it may be unnecessary in the presence of nominal types.

Copy link
Member Author

@rossberg rossberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the close look!

@@ -186,34 +203,32 @@ Perhaps add the following short-hands:
* `struct.new <typeidx>` allocates a structure of type `$t` and initialises its fields with given values
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

- iff `$t = struct (mut t)*`
- and `(type $t) <: t'`
- and `(type $t) == t'`
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm confused by the (type $t) part. Isn't $t a type?

It's a "type use" referring to $t, see the new definition of heap types. The extra keyword avoids ambiguity in some syntactic contexts and is more consistent with other syntax. Note that (ref $t) is defined as a shorthand for (ref (type $t)).

FWIW, I just removed the type annotation on the instruction, because with type equivalence it can be derived from the operand type.

If I get to make further wishes: I find the t* part confusing too, because that's not a repeated sequence of a single t type.

It's a sequence of possibly different value types. It's a notational convention that is used heavily in the spec, explained here.

* `rtt.canon <constype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt t)]`
* `rtt.canon <heaptype>` returns the RTT of the specified type
- `rtt.canon t : [] -> [(rtt 0 t)]`
- multiple invocations of this instruction yield the same observable RTTs
- this is a *constant instruction*
- equivalent to `(rtt.sub t (rtt.canon any))`, except when `t` itself is `any`
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes, fixed (it's (rtt.sub 1 any t (rtt.canon any))).

- multiple invocations of this instruction with the same operand yield the same observable RTTs
- this is a *constant instruction*

TODO: Add the ability to generate new (non-canonical) RTT values to implement casting in nominal type hierarchies.
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not yet, it may be unnecessary in the presence of nominal types.

@rossberg rossberg merged commit 20a80e3 into master Jun 5, 2020
@rossberg rossberg deleted the clarif branch June 5, 2020 12:22
rossberg pushed a commit that referenced this pull request Feb 24, 2021
rossberg added a commit that referenced this pull request Mar 22, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants