-
Notifications
You must be signed in to change notification settings - Fork 81
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
Preliminary fix for recursive records with polymorphic contracts #1194
Changes from all commits
45ba45c
6930051
c0318de
4effc72
6b1450f
e692ffb
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -37,7 +37,13 @@ | |
# blaming polymorphic contracts. | ||
%seal% sealing_key (%chng_pol% label) value, | ||
|
||
"$forall" = fun sealing_key polarity contract label value => | ||
"$forall" = | ||
let flip = match { | ||
`Positive => `Negative, | ||
`Negative => `Positive, | ||
} in | ||
fun sealing_key polarity contract label value => | ||
let polarity = if %dualize% label then flip polarity else polarity in | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. So you flip the polarity if the label is dualized, although the polarity was already flipped as well in the code generating the recursive environment. This means the polarity is back to the original one? Is there any difference between a normal label and a dualized one, then? I might be a bit lost. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ah, if I understand correctly, you flip two different polarities when dualizing: the current polarity of the label (makes sense, as the whole contract moves to the codomain), and the one corresponding to what was the polarity of the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. When There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. But you already flip the label polarity when dualizing, right? There is a call to Additionally, here, the dualization seems to also targets type variables that are already introduced in There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Let's walk through an example, say
The contract
So Now, when the resulting contracts are applied, another layer of polarity tracking is initiated in the label. Let's imagine we're applying the contract
When building the recursive environment in a record, when thinking of a recursive field as a function
where There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, I think I get it when the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In some sense, it feels like it treats There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The corresponding
Evaluation will then proceed and In a sense, setting the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ooooh, it's the It's a really non trivial magic trick we're pulling here, we'll have to document it very clearly and in details, if we want this to be remotely understandable 6 months from now. The examples you posted here are valuable and should be stored somewhere, before we put the note in good shape. |
||
contract (%insert_type_variable% sealing_key polarity label) value, | ||
|
||
"$enums" = fun case label value => | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I fear this will disappear just as we do the fusion of the contract and the dual contract. But it's not too important, we can get rid of it then.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it really should disappear then. I tried for a while to make do with just the data in
type_environment
, but I think I really need a global flag to compute the dual contracts dynamically.