Change to Steed's model of subtyping #3643

jasoncarr0 · 2020-09-06T01:32:01Z

Most individual commits have a long comment describing what they do.
Notably, had to weaken the type of two map methods as they were incorrect for the implementation that they had (and it should be reasonably obvious I hope).

We will also need to ensure that documentation correctly disambiguates between iso and iso^ when talking about subtyping, as otherwise the error messages may be quite confusing (iso is not a subcap of ref). This is painfully unintuitive with current docs/cap-naming, but that unintuitiveness was exactly what got us into this unsound subtyping mess.

Fixes #1964

Updated subtyping table:

jasoncarr0 · 2020-09-06T01:32:34Z

src/libponyc/type/cap.c

@@ -878,6 +889,53 @@ bool cap_view_lower(token_id left_cap, token_id left_eph,
  return true;
 }

+bool cap_safetomove(token_id into, token_id cap, direction direction)


Rearranged code. No changes here

jasoncarr0 · 2020-09-06T01:33:37Z

src/libponyc/type/cap.c

-bool cap_safetomove(token_id into, token_id cap, direction direction)
+
+
+static ast_t* modified_cap_single(ast_t* type, cap_mutation* mutation)
 {


Related to the above, I believe that the Git diffing algorithm has decided that this was derived from the cap safe_to_move above, so I would recommend not attempting to make sense of the diff and just looking at the raw code

In any case, this is only used right now for the unisolation bit. More code can be made to use this, but that starts bringing up the scope (as there's also bugs caused by the way that some of those are implemented today)

src/libponyc/codegen/gentrace.c

jemc

Looks good other than these small quibbles:

src/libponyc/type/cap.h

src/libponyc/type/cap.c

jasoncarr0 · 2020-10-02T07:20:14Z

Noting that f92d601 may still not be correct with how we use the bounds, since it allows #alias <= #any, but we wouldn't want the meaning implied by the original which was #alias <= ref. Hopefully don't want too much scope creep with.

jasoncarr0 · 2020-10-04T18:41:32Z

Once tests pass, this will be good to go, but we also need to update the tutorial's subtyping section and talk about error messages here. Still looking at package/stdlib updates

packages/builtin/string.pony

packages/collections/persistent/_map_node.pony

jasoncarr0 · 2020-10-23T01:53:00Z

Current question: what's the expected behavior for https://github.com/ponylang/ponyc/pull/3643/files#diff-de4b55849bafa987e2a3f3cd5f61edbced75be7d892d847d7beef4e9f9fcbeb5R460

These were the examples which were in tail position that was not exactly the last expression of a function. Should this sort of case be supported automatically? Perhaps it may be sufficient for now to support the easiest cases explicitly and later a more complete rule.

ponylang-main · 2021-04-20T18:14:09Z

Hi @jasoncarr0,

The changelog - fixed label was added to this pull request; all PRs with a changelog label need to have release notes included as part of the PR. If you haven't added release notes already, please do.

Release notes are added by creating a uniquely named file in the .release-notes directory. We suggest you call the file 3643.md to match the number of this pull request.

The basic format of the release notes (using markdown) should be:

## Title

End user description of changes, why it's important,
problems it solves etc.

If a breaking change, make sure to include 1 or more
examples what code would look like prior to this change
and how to update it to work after this change.

Thanks.

SeanTAllen · 2021-04-20T18:14:28Z

@jemc @jasoncarr0 i put a "fixed" label on this as it fixes a bug, however, maybe "changed" would be better.

SeanTAllen · 2021-04-20T18:14:51Z

I do think some release notes are in order either way.

jasoncarr0 · 2021-04-24T18:51:51Z

src/libponyc/pass/expr.c

@@ -139,6 +139,7 @@ bool is_method_result(typecheck_t* t, ast_t* ast)
    case TK_IF:
    case TK_WHILE:
    case TK_MATCH:
+    case TK_IFDEF:


Are there any other cases known missing from this function?

Referencing treecheckdef.h, here are things I'm not seeing in this function that probably should be here:

TK_FOR - the first two children are part of iterator declaration, and should return false here

TK_WITH - the first child should return false

TK_REPEAT - the second child (the condition) should return false

jasoncarr0 · 2021-05-01T02:00:14Z

Removed the do not merge label since it was originally due to needing the tutorial updates.

ponylang/pony-tutorial#449 should be merged whenever this is released

SeanTAllen · 2021-05-01T02:42:48Z

When this is merged, ponylang/pony-tutorial#449 should be added to the current open release issue as something to be merged after the release.

SeanTAllen · 2021-05-01T16:34:35Z

@jemc @jasoncarr0 are we ready to merge this sucker?

jasoncarr0 · 2021-05-01T17:48:33Z

@SeanTAllen I believe we are

SeanTAllen · 2021-05-01T18:37:13Z

@jasoncarr0 is the initial commit comment good for when this gets squashed? do you want to squash and update the commit comment? otherwise i can squash it only keeping the initial comment.

let me know which you prefer to do.

jasoncarr0 · 2021-05-01T18:46:12Z

Could you clarify which comment you're referring to as the initial comment @SeanTAllen ? I'm guessing I should just squash myself. I would think "Change to Steed's model of subtyping" or "Change to Steed's model of subtyping to fix return subtyping checks" would be sufficient as the commit

SeanTAllen · 2021-05-01T19:02:10Z

I think the commit comment needs a why and what for general guidance. This is a change that touches a lot of places and for future history I think its important to have a commit comment that someone can use to understand it.

For example, linking to where the steed work can be found and other relevant details. Basically "release notes" but pony developer focused rather than pony user.

The original notion of subtyping in Pony combined subtyping and aliasing simultaneously (K1 <= K2 if K1^ could be coerced to K2). This is reasonable for many checks, which used aliasing already, but this wasn't sufficient for some subtyping checks (most notably return subtyping, where we do not alias a priori) and as a result, the subtyping used for return types was unsound, allowing an `iso` expression (Not `iso^`) to be coerced to any cap, such as creating a `val` reference while the `iso` was still around. This change decouples the two, using the subtype ordering for capabillities which was presented in George Steed's Masters thesis: "A Principled Design of Capabilites in Pony" Primarily, this means that most cases where aliasing were required before now check `K1 <= K2^`, whereas before it was often `!K1 <= K2` Importantly, this now means that subtyping can be checked without aliasing by checking that `K1 <= K2`. Some standard library methods had to be given weaker types due to the improper return type checks. It may be possible to re-strengthen these checks with some unsafe code, if it is genuinely sound to do so. In addition, the tail expression code was strengthened to handle some cases which were not handled prior. These likely did not arise due to the incorrect return subtyping checks, but are now necessary to auto-consume.

SeanTAllen · 2021-05-01T21:21:58Z

Looks good @jasoncarr0. Awesome work. Thanks.

jasoncarr0 commented Sep 6, 2020

View reviewed changes

jasoncarr0 changed the title ~~[WIP] Fix unsound subtyping and use Steed-style subtyping~~ [WIP] Fix unsound subtyping Sep 6, 2020

jasoncarr0 marked this pull request as ready for review September 8, 2020 00:28

jasoncarr0 commented Sep 15, 2020

View reviewed changes

src/libponyc/codegen/gentrace.c Outdated Show resolved Hide resolved

jasoncarr0 changed the title ~~[WIP] Fix unsound subtyping~~ [WIP] Change to Steed's model of subtyping Sep 27, 2020

SeanTAllen added the do not merge This PR should not be merged at this time label Sep 29, 2020

jemc approved these changes Sep 29, 2020

View reviewed changes

src/libponyc/type/cap.h Outdated Show resolved Hide resolved

src/libponyc/type/cap.c Outdated Show resolved Hide resolved

jasoncarr0 changed the title ~~[WIP] Change to Steed's model of subtyping~~ Change to Steed's model of subtyping Oct 4, 2020

jasoncarr0 mentioned this pull request Oct 6, 2020

Update for changes to use George Steed's subtyping model ponylang/pony-tutorial#449

Merged

jasoncarr0 requested review from SeanTAllen and jemc October 6, 2020 18:23

jemc reviewed Oct 20, 2020

View reviewed changes

packages/builtin/string.pony Outdated Show resolved Hide resolved

packages/collections/persistent/_map_node.pony Outdated Show resolved Hide resolved

jemc approved these changes Oct 23, 2020

View reviewed changes

Base automatically changed from master to main February 8, 2021 23:02

bb010g mentioned this pull request Feb 28, 2021

RFC 59: Formal Viewpoint Adaptation #2815

Open

SeanTAllen added the changelog - fixed Automatically add "Fixed" CHANGELOG entry on merge label Apr 20, 2021

jasoncarr0 commented Apr 24, 2021

View reviewed changes

jemc approved these changes Apr 27, 2021

View reviewed changes

jasoncarr0 removed the do not merge This PR should not be merged at this time label May 1, 2021

jasoncarr0 force-pushed the fix-unsound-return-subtyping branch from af4a2c8 to ffac258 Compare May 1, 2021 19:46

SeanTAllen merged commit 2b9eb70 into ponylang:main May 1, 2021

github-actions bot pushed a commit that referenced this pull request May 1, 2021

Updates release notes for PR #3643

7575c41

github-actions bot pushed a commit that referenced this pull request May 1, 2021

Update CHANGELOG for PR #3643

151a2f5

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change to Steed's model of subtyping #3643

Change to Steed's model of subtyping #3643

jasoncarr0 commented Sep 6, 2020 •

edited

Loading

jasoncarr0 Sep 6, 2020

jasoncarr0 Sep 6, 2020

jasoncarr0 Sep 6, 2020

jemc left a comment

jasoncarr0 commented Oct 2, 2020

jasoncarr0 commented Oct 4, 2020 •

edited

Loading

jasoncarr0 commented Oct 23, 2020 •

edited

Loading

ponylang-main commented Apr 20, 2021

SeanTAllen commented Apr 20, 2021

SeanTAllen commented Apr 20, 2021

jasoncarr0 Apr 24, 2021

jemc Apr 25, 2021

jasoncarr0 commented May 1, 2021 •

edited

Loading

SeanTAllen commented May 1, 2021

SeanTAllen commented May 1, 2021

jasoncarr0 commented May 1, 2021

SeanTAllen commented May 1, 2021

jasoncarr0 commented May 1, 2021 •

edited

Loading

SeanTAllen commented May 1, 2021

SeanTAllen commented May 1, 2021

Change to Steed's model of subtyping #3643

Change to Steed's model of subtyping #3643

Conversation

jasoncarr0 commented Sep 6, 2020 • edited Loading

jasoncarr0 Sep 6, 2020

Choose a reason for hiding this comment

jasoncarr0 Sep 6, 2020

Choose a reason for hiding this comment

jasoncarr0 Sep 6, 2020

Choose a reason for hiding this comment

jemc left a comment

Choose a reason for hiding this comment

jasoncarr0 commented Oct 2, 2020

jasoncarr0 commented Oct 4, 2020 • edited Loading

jasoncarr0 commented Oct 23, 2020 • edited Loading

ponylang-main commented Apr 20, 2021

SeanTAllen commented Apr 20, 2021

SeanTAllen commented Apr 20, 2021

jasoncarr0 Apr 24, 2021

Choose a reason for hiding this comment

jemc Apr 25, 2021

Choose a reason for hiding this comment

jasoncarr0 commented May 1, 2021 • edited Loading

SeanTAllen commented May 1, 2021

SeanTAllen commented May 1, 2021

jasoncarr0 commented May 1, 2021

SeanTAllen commented May 1, 2021

jasoncarr0 commented May 1, 2021 • edited Loading

SeanTAllen commented May 1, 2021

SeanTAllen commented May 1, 2021

jasoncarr0 commented Sep 6, 2020 •

edited

Loading

jasoncarr0 commented Oct 4, 2020 •

edited

Loading

jasoncarr0 commented Oct 23, 2020 •

edited

Loading

jasoncarr0 commented May 1, 2021 •

edited

Loading

jasoncarr0 commented May 1, 2021 •

edited

Loading