Subtyping in Simply Typed Lambda-Calculus

Using Coq
#1

Hello,

I am trying to solve this exercise
Exercise: 1 star, standard (subtype_instances_tf_2)

from this chapter
https://softwarefoundations.cis.upenn.edu/plf-current/Sub.html

This statemen below. Is it true?

∃S,
       S <: S→S

This is what I think about it:

Going to use 2 rules:
S_Refl and S_Arrow

exists S,
S <: S->S ??? is it true or false, let’s try Exists (S->S)
then

S -> S <: (S -> S) -> (S -> S)
S1 S2 T1 T2 According to S_Arrow we should have 2 statements

Statement 1. (S -> S) <: S
AND
Statement 2. S <: (S -> S)

but it is a contradiction. So answer is False? Is it correct? is it a contradiction?

Thanks,
Nat

#2

This statement seems to be wrong given the subtyping system in the SF chapter. However, in some intersection type systems, this holds for the Top (aka. ω) type.

This is not contradictory. This is called type equivalence or bi-directional subtyping. Example: {name:String, age:Nat} and {age:Nat, name:String}. If A <: B and B <: A, this means that everywhere where A is required we can use B, and vice versa.

#3

Thank you for your answer!

yes, they have Top for this system they define:
this is how they define Top : a type that lies above every other type and is inhabited by all (well-typed) values. Is it the Top you describe?

so it would be :
Top <: Top -> Top
is it true? with their Top?

As for statements I marked as contradictory… they should be true, They both should be true (my AND is extremely confusing, sorry for it). So if they both true, then initial statement is true (one we are trying to solve).

Your example for type equivalence… they call it Record Permutation, and it’s about records, not about arrow type. And we have arrow type here. right? so we should use arrow type rule, right?

so conditions which above the line in arrow type rule, they both should be true. That is why I wrote AND, but they can’t be true for arrow type, right?

so is it correct they we have a contradiction, so initial statement is false?

Thanks,
Nat

#4

1
11920×1080 273 KB

Types they have

#5

No, this does not hold in this system. You could try to formally prove (in Coq) that this doesn’t hold.

Here’s the idea:

  1. Prove that if U <: S -> T, then there exists U1, U2, such that U = U1 -> U2, S <: U1 and U2 <: T.
  2. From this follow: forall S, not S <: S -> S.

The proof script for (1) would begin with:

intros U S T. intros H.
remember (S -> T) as ST. (* This replaces `S->T` with the fresh variable `ST` and introduces an equation `eqnST: ST = S -> T` *)
induction H; inversion H; clear H.
...
#6

Oh, oh you are so right… I see now. They even have this theorem in the chapter below… just the one you suggested. 3 stars… Thank you. Will try to prove it.