0
$\begingroup$

In Higher-order bounded quantification ($F^ω_{<:}$), introduced in Ch31 in Types and Programming Langauges by Pierce, its subtyping and equivalence rules are:

enter image description here

  1. Does subtyping relation only exist between two type expressions in the same kind? Can two type expressions in different kinds have subtyping relation?

  2. In rule (S-TRANS), why is Γ |- U :: K needed?

  3. In rule (S-EQ), why are Γ |- S :: K and Γ |- T :: K needed? Are they not implied by S ≡ T?

  4. Does the equivalence relation exist only between two type expressions in the same kind? Can two types in different type expressions have the equivalence relation?

Thanks.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.