在 SML 中派生表达式类型

Question

我对 sml 有点陌生，我正在尝试了解如何派生表达式类型。
我读了Deriving type expression in ML，并试图按照他所做的来推导出我的表达方式，但我无法理解其中的一段。

我试图得出的表达式是：

fn x => fn y => fn z => z(z(y x))

我正在做的事情如下：

fn x : T1 => fn y : T2 => fn z : T3 => z(z(y x)) : T4

此时应该是

T2 = T1 -> T5                       //y x
T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T7                       //z(z(y x))

这是我认为我做错的地方。

还应该有一个像

这样的约束

T7 = T4 or T6 = T4.    

我不确定也不清楚这一点。

提前感谢您的帮助。

Answer 1

您已经将T4 分配给z(z(y x))，所以我们可以在最后一个等式中使用它。

T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T4                       //z(z(y x))

由于T5 -> T6 = T6 -> T4，因此T5 = T6和T6 = T4。