Extend typechecker inversion lemma for type annotation #569
Conversation
john-h-kastner-aws
force-pushed
the
type-annot-inversion
branch
from
555ff0e to
3ae02e1
Compare
Signed-off-by: John Kastner <jkastner@amazon.com>
john-h-kastner-aws
force-pushed
the
type-annot-inversion
branch
from
3ae02e1 to
5e64bec
Compare
| ∃ tx₁ c₁ tx₂ c₂, | ||
| typeOf x₁ c env = Except.ok (tx₁, c₁) ∧ | ||
| typeOf x₂ c env = Except.ok (tx₂, c₂) ∧ | ||
| ∃ ty, tx = .binaryApp op₂ tx₁ tx₂ ty |
There was a problem hiding this comment.
Is it ok to combine the two existential quantifiers? Btw, there's no detailed specification of ty, like other inversion theorems. Is it intended?
There was a problem hiding this comment.
I realized that these inversion theorems essentially say that typedOf produces well-typed expressions and subsequent proofs are "Well typed programs cannot go wrong." I'm not sure if we can complete the TPE soundness proof using this inversion theorem. That being said, we can always expand the theorem later.
There was a problem hiding this comment.
Is it ok to combine the two existential quantifiers?
I don't see why not
Btw, there's no detailed specification of ty
I don't actually care about ty for my proofs, so this is good enough. The inversion lemma for the specific binary operators do specify ty, but I wanted one inversion lemma for all binary operators to make my proofs simpler. We could extend this lemma to specify the types of tx tx\1 and tx\2 in a match on op\2. Then other inversion lemma could be done in terms of this one, but I didn't need to go that far.
I realized that these inversion theorems essentially say that typedOf produces well-typed expressions
Yeah, there's probably some overlap here. I expect that TPE will need something stronger than what I needed for levels, but we'll probably be able to end up with both proof using the same inversion theorems.
Some changes pulled out of #533
if