subtyping - 如果 A 是 B 的子类型，那么 (A→B) → A 是否是 (B→B) → A 的子类型？

Question

假设A是B的子类型，(A→B)→A是(B→B)→A的子类型吗？A→(B→A)是B→(B→A)的子类型吗？

标签： subtyping

Answer 1

根据子类型和函数类型，方法如下：

象征意义和假设：

1. A是( )的子类型BA < B
2. X→Y是接收类型实例X并返回类型实例的函数（类型）Y
3. 函数类型S1→S2是iif的子类型，并且T1→T2 T1 < S1 S2 < T2

要(A→B)→A成为(B→B)→A它的子类型，将需要：

1. (B→B)<(A→B)和
2. A < A（真实身份）

为了(B→B) < (A→B)再次应用我们需要的函数子类型：

1. A < B（假设为真）和
2. B < B（缩进为真）

或(A→B)→A的子类型也是如此(B→B)→A(A→B)→A < (B→B)→A

尝试按照类似的分析来回答第二个问题：

是A→(B→A)的亚型B→(B→A)吗？