-
Notifications
You must be signed in to change notification settings - Fork 371
Subtyping reconstruction #410
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
base: master
Are you sure you want to change the base?
Conversation
Hi Roman, glad to see that Kotlin is moving in this direction! I was pointed to your proposal by a student and was curious whether you were aware of our recent paper on the topic: A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning. While our paper was focused on the soundness of subtyping reconstruction rather than on the algorithm, you might find it interesting because it basically shows how we ended up thinking about the feature in the context of Scala 3, while implementing it. The paper also mentions Kotlin and elucidates important differences between Kotlin and Scala 3 with respect to subtyping reconstruction. This is also the paper where we came up with the term "Subtyping Reconstruction", which you seem to have adopted! So I was a bit surprised not to find it in your references section. |
Hi Lionel (@LPTK), Thank you for your comment. We are indeed aware of that work and have drawn significant inspiration from it. You'll find it referenced as “Description of the Scala 3 implementation (Section 6.2)” in the second position of our references list. We chose to emphasize the algorithm section, as we believe it may be interesting to more readers. Please note that we did not format it extensively, as it is not typical for KEEP documents to have references list and since it isn’t indexed elsewhere. However, if you’d prefer a specific format, we’re happy to adjust it. Also, if you have any concerns about the soundness of our approach, we’d be glad to hear your thoughts! |
Thanks for your quick response, Roman!
Oh, I had not realized that link (which I had not clicked) was pointing to our paper, my bad! I had assumed it pointed to some internal discussions of the Dotty/Scala 3 compiler project.
Not at all; I just wanted to check you were aware of the paper 😉
For this I'll need to take some time to sit down and look into the details for a while, which won't happen in the near future unfortunately (too many deadlines these days). But it would help if you could come up with a formalization or paper draft at some point. |
@@ -0,0 +1,1254 @@ | |||
# Subtyping reconstruction | |||
|
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.
UQA5NWl5eH6KvxwnMBCj7vDbb-Xebok-pWGfFuHhq1zMxmv5
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.
Only comment here about the text itself. The discussion about the feature is in #409.