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.

Sign up for GitHub

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

Jump to bottom

Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax... #19

Open
wants to merge 2 commits into
base: 1ml-prime
Choose a base branch
from
Open

Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax... #19

wants to merge 2 commits into from

Conversation

polytypic
Copy link
Member

@polytypic polytypic commented Feb 18, 2020 •
edited
Loading

Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax for type refinement.

The new

T_abs & T_sub

mechanism is similar to the old

T_abs with (Path = T_sub)

mechanism and also to the include mechanism

{...T_abs; ...T_sub}

The main difference is that, instead of using a path to target a specific substructure or requiring that no declarations overlap, an intersection, T_int, of the nested declarations of T_abs and T_sub, is computed.

Then it is checked whether T_abs :> T_int and if so a substitution, 𝛿, is obtained. Finally the nested declarations of 𝛿(T_abs) and T_sub are merged.

Also, in T1 & T2 both T1 and T2 are elaborated in the same environment whereas in {...T1; ...T2} the environment for T2 includes declarations from T1 and in T1 with (P = T2) the path P is specific to T1.

When defined, T1 & T2 is always a subtype of both T1 and T2

T1 & T2  :>  T1
T1 & T2  :>  T2

@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch 5 times, most recently from 4a4c30a to 229896c Compare February 19, 2020 18:24
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch 3 times, most recently from aff9b3e to 7845dd3 Compare February 22, 2020 13:29
@polytypic polytypic force-pushed the 1ml-prime branch 4 times, most recently from 1d77593 to b248d00 Compare February 22, 2020 18:46
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 7845dd3 to 604881f Compare February 22, 2020 18:48
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 604881f to 5fc4f42 Compare February 22, 2020 18:57
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 5fc4f42 to ea353d3 Compare February 23, 2020 10:47
@polytypic polytypic force-pushed the 1ml-prime branch 2 times, most recently from 6167f5b to 88b09cf Compare February 28, 2020 06:01
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from ea353d3 to 2268faa Compare February 28, 2020 06:45
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch 2 times, most recently from e909120 to afd4d23 Compare February 29, 2020 08:49
@polytypic polytypic force-pushed the 1ml-prime branch 6 times, most recently from 0fb0880 to 5c75b59 Compare March 1, 2020 13:20
@polytypic polytypic force-pushed the 1ml-prime branch 2 times, most recently from 0b0a19e to 486657d Compare July 4, 2020 09:18
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 21012f8 to 2dc5974 Compare July 4, 2020 09:39
@polytypic polytypic force-pushed the 1ml-prime branch 3 times, most recently from dcc40ea to 7825b41 Compare July 4, 2020 10:40
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 2dc5974 to 6ffef69 Compare July 4, 2020 10:45
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch 3 times, most recently from df4bb4c to 8597788 Compare July 12, 2020 08:54
@polytypic polytypic force-pushed the 1ml-prime branch 3 times, most recently from ec6e7c7 to 8c8671b Compare July 21, 2020 14:10
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 8597788 to a94dd33 Compare July 21, 2020 14:42
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from a94dd33 to 2a76357 Compare July 21, 2020 15:52
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch 2 times, most recently from dac23e1 to ac35709 Compare July 28, 2020 14:19
@polytypic polytypic force-pushed the 1ml-prime branch 2 times, most recently from 59f2865 to 00bc488 Compare August 3, 2020 02:21
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from ac35709 to 59631d1 Compare August 3, 2020 03:53
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 59631d1 to ad5f067 Compare August 10, 2020 06:46
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from ad5f067 to 1c2a1b9 Compare August 24, 2020 03:55
@polytypic
Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax...
d0e549b 
...for type refinement.

The new

    T_abs & T_sub

mechanism is similar to the old

    T_abs with (Path = T_sub)

mechanism and also to the include mechanism

    {...T_abs; ...T_sub}

The main difference is that, instead of using a path to target a specific
substructure or requiring that no declarations overlap, an intersection,
`T_int`, of the nested declarations of `T_abs` and `T_sub`, is computed.

Then it is checked whether `T_abs :> T_int` and if so a substitution, `𝛿`, is
obtained.  Finally the nested declarations of `𝛿(T_abs)` and `T_sub` are merged.

Also, in `T1 & T2` both `T1` and `T2` are elaborated in the same environment
whereas in `{...T1; ...T2}` the environment for `T2` includes declarations from
`T1` and in `T1 with (P = T2)` the path `P` is specific to `T1`.

When defined, `T1 & T2` is always a subtype of both `T1` and `T2`

    T1 & T2  :>  T1
    T1 & T2  :>  T2
@polytypic
Separate matching from subtyping like in F-ing modules to allow RDS
0778534
@polytypic polytypic force-pushed the intersection-sub-to-replace-with branch from 1c2a1b9 to 0778534 Compare August 24, 2020 05:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
1 participant
@polytypic