feedback
Okay, I spent an hour or so going back over the paper, trying to put special focus on the new additions on Recursive Subtype Constraint Entailment.
I was pretty happy with most of what I read (or maybe I'm just desparate to declare this thing finished), but I found myself going back over section 10.1 several times because I was confused by two things that looked like distinct conflicting "definitions" for the subtyping relation, <:
At one point, there is a line "The subtyping relation on T_Sigma is defined as follows. t <: t' iff ..."
and later there is the paragraph on Nonstructural subtyping which fixes Sigma = { \times, \to, \top, \bot } with latice ordering \bot <: \sigma, \sigma <: \top for all \sigma in \Sigma.
Did you mean to use the same "<:" in both places? Or are the second set of "<:"'s really analogous to the <:_B base type relation (or perhaps I should be calling it <:_\Sigma here)? I was confused by that, but ended up deciding that you must have not intended for the two notations to collide.
There are other changes to suggest, but they are merely suggestions or minor details, so I'll either make them directly myself or add "margin notes" for them.
I was pretty happy with most of what I read (or maybe I'm just desparate to declare this thing finished), but I found myself going back over section 10.1 several times because I was confused by two things that looked like distinct conflicting "definitions" for the subtyping relation, <:
At one point, there is a line "The subtyping relation on T_Sigma is defined as follows. t <: t' iff ..."
and later there is the paragraph on Nonstructural subtyping which fixes Sigma = { \times, \to, \top, \bot } with latice ordering \bot <: \sigma, \sigma <: \top for all \sigma in \Sigma.
Did you mean to use the same "<:" in both places? Or are the second set of "<:"'s really analogous to the <:_B base type relation (or perhaps I should be calling it <:_\Sigma here)? I was confused by that, but ended up deciding that you must have not intended for the two notations to collide.
There are other changes to suggest, but they are merely suggestions or minor details, so I'll either make them directly myself or add "margin notes" for them.
posted by pnkfelix at 12:26 PM
2 Comments:
p.s. phone contact is going to be a bad idea for the next few hours, one because my phone is nearly dead, and two because I'm planning to go to the library to do some background checks on some of these intersection type // strong normalization papers.
I'm planning on adding something to the beginning of the paper that at least DEFINES strong normalization (note that the paper never defines beta reduction, let alone strong normalization; this was a virtue at first, since you didn't *have* to talk about those concepts to make arguments about the decidability/complexity of type inference, but a couple of sections now talk about subject reduction/expansion and strong normalization, so that's not so good.)
Ah, yes, the second "<:" definition you refer to is defining "<:_Sigma", which is included in "<:_T_Sigma" as had been defined above. I will make that more explicit.
I haven't seen any changes in subversion yet, check in what you've got and I'll start responding and cleaning up.
Post a Comment
<< Home