[POPLmark] Experience report with Twelf

[Stephanie Weirich]

Dan Licata wrote:

>>A side note: I don't think that this is exactly the law of the
>>excluded middle. I think it says something like "at least one of the
>>'subtyping' and 'notsubtyping' judgments are derivable." 
>>    
>>
>
>The law of the excluded middle is usually phrased as (A or not(A)),
>which corresponds in this instance to the phrase in quotes above.
>
>  
>
<rest snipped>

 I think we dis agree on what the definition of not-subtype should be, 
and that makes all of the difference.
You propose the following definition:

> not-subtyping-contra : not-subtyping A B
>		       <- (subtyping A B -> false).

where I define non-subtyping without relation to the subtyping 
judgement. (Technically, a judgments that
holds when two types aren't subtypes of one another.)   That's why  the 
subtyping-exclusive lemma

>>subtyping-exclusive: subtyping A B -> not-subtyping A B -> false ->  
>>type.
>>    
>>
is necessary to make it clear that both of these judgments can't hold.  
(It is true by definition for your version.).

However, I prefer my definition of not-subtyping because with your 
definition, the excluded middle lemma
is not provable in Twelf---there is no LF canonical form of type 
(subtyping A B -> false). Even though I
originally wanted to assert the decidablity of subtyping, since 
subtyping *is* in fact decidable, it makes sense for me to
assert it in a way that could eventually be proven in Twelf.

>>
>>lookupClass_strengthen :
>>   ({x:exp} lookupClass CT C (class C D FS (MT x)))
>>     -> lookupClass CT C (class C D FS (MT unit)) -> type.
>>
>>However, I think this is a case where strengthening is unavoidable.
>>The type exp is subordinate to the type methodTable, but since the
>>methodTable MT comes from the classTable CT (which does not depend on
>>x) in this case, it can't depend on x.
>>    
>>
>
>This could be a property of the system you're formalizing, not just
>the LF encoding.  That is, on paper, how do you *know* that the class
>you get back doesn't mention some variable in the context?  Sometimes
>I've glossed over things like this on paper only to have Twelf point
>them out to me.
>  
>
This issue didn't come up in either the Coq version of the proof (that I 
did) or the Isabelle/HOL version
(that two grad students here at Penn did).

--Stephanie