# Subtyping in Simply Typed Lambda-Calculus

**URL:** <https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014>\
**Category:** Using Rocq\
**Created:** [August 12, 2020, 10:40am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014 "2020-08-12T10:40:14Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [August 12, 2020, 10:40am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/1 "2020-08-12T10:40:14Z")

</div>

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](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

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [August 12, 2020, 12:01pm UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/2 "2020-08-12T12:01:01Z")

</div>

> [@Natasha](#):
>
> This statemen below. Is it true?
> 
> ```auto
> ∃S,
> S <: S→S 
> 
> ```

This statement seems to be wrong given the subtyping system in the SF chapter. However, in some [intersection type systems](https://en.wikipedia.org/wiki/Intersection_type_system#Intersection_type_subtyping), this holds for the `Top` (aka. `ω`) type.

> [@Natasha](#):
>
> Statement 1. (S → S) \<: S  
> AND  
> Statement 2. S \<: (S → S)
> 
> but it is a contradiction.

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.

---

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [August 13, 2020, 9:26am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/3 "2020-08-13T09:26:20Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [August 13, 2020, 9:27am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/4 "2020-08-13T09:27:15Z")

</div>

![1](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/ba68bde901263ecd18b3c4fd7dcce7e44c4f24b8.png)

Types they have

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [August 13, 2020, 11:40am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/5 "2020-08-13T11:40:46Z")

</div>

> [@Natasha](#):
>
> so it would be :  
> Top \<: Top → Top  
> is it true? with their Top?

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:

```auto
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.
...
```

---

<div class="post-metadata">

**Author:** ![Natasha](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/natasha/32/213_2.png) [@Natasha](https://discourse.rocq-prover.org/u/Natasha)\
**Post date:** [August 14, 2020, 5:35am UTC](https://discourse.rocq-prover.org/t/subtyping-in-simply-typed-lambda-calculus/1014/6 "2020-08-14T05:35:18Z")

</div>

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.