Blog post on DOT #397
Merged
Blog post on DOT #397
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| inconsistencies, at least not by a local analysis that does not need | ||
| to look at the whole program. What's worse, once you have an | ||
| inconsistent set of definitions you can use these definitions to | ||
| "prove" their own consistency - much like an mathematical theory that |
| trait Sub2 extends Base { type A = Int } | ||
|
|
||
| Now, if you combine `Sub1` and `Sub2` in one class, you get a conflict, since the type `A` is supposed to be equal to both `String` and `Int`. If you do | ||
| not detect the conflict and assume the equalities at face value you |
There was a problem hiding this comment.
"Now, if you combine Sub1 and Sub2 in one class" is a crucial step and I guess readers will want to know more precisely what you mean here, e.g. some Scala code like trait Bad extends Sub1 with Sub2.
|
You might consider putting the "Why is This Important?" section first, not last, if you want that section to be widely read. In the current order, a lot of general/casual readers will bail during the calculus section. |
| ## Difficulties | ||
|
|
||
| Formulating the precise soundness theorem and proving it was unexpectedly hard, | ||
| because it uncovered a problem complex that had not been |
There was a problem hiding this comment.
"a problem complex" ? Do you mean "a complex problem" ?
|
@SethTisue It's a concern but it would be difficult to change the flow now. Let's leave it as it is. |
|
I believe it's ready to merge now, unless there are further change requests. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Comments solicited, but not merge yet.