我能想到的最简单的方法是稍微重新格式化您的代码,基本上将每个子表达式放在自己的行上。子级以增加的缩进表示。
让我们举个例子:
fun ff f x y = if (f x y) then (f 3 y) else (f x "zero")
首先,我们需要做一些脱糖工作。以上等价于:
val ff =
fn f =>
fn x =>
fn y =>
if (f x y) then (f 3 y) else (f x "zero")
现在,让我们将每个子表达式放在自己的行中(括号在这个特定示例中是多余的;没有它们一切正常):
val ff =
fn f =>
fn x =>
fn y =>
if
f
x
y
then
f
3
y
else
f
x
"zero"
最后,让我们为每个子表达式附加一个类型,但是让我们为我们还不知道的类型使用类型变量。请注意,我们对相同的事件使用相同的类型变量。例如,x 在任何地方都有 t3 类型。
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | t1 -> t2
fn x => | t3 -> t4
fn y => | t5 -> t6
if | t7 (* the type of the whole `if` expression *)
f | t1
x | t3
y | t5
then | t8 (* the type of the whole `then` part *)
f | t1
3 | int
y | t5
else | t9 (* the type of the whole `else` part *)
f | t1
x | t3
"zero" | string
然后,您可以通过注意某些类型变量是等效的或它们在某些上下文中使用来做一些进一步的简化。比如从这三个调用f:
我们可以得出x 必须是int 类型并且y 必须是string 类型。所以,让我们将x 的类型,即t3,替换为int,将y 的类型,即t5,替换为string。我们在任何地方都这样做:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | t1 -> t2
fn x => | int -> t4
fn y => | string -> t6
if | t7
f | t1
x | int
y | string
then | t8
f | t1
3 | int
y | string
else | t9
f | t1
x | int
"zero" | string
此外,f 被用作每次都被传递 int 的函数。结果也用作函数,并被传递给string。这意味着t1,它是分配给f 的类型变量,必须是int -> string -> r0 类型,对于一些我们还不知道的r0。让我们将所有出现的t1 替换为int -> string -> r0。
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> r0) -> t2
fn x => | int -> t4
fn y => | string -> t6
if | t7
f | int -> string -> r0
x | int
y | string
then | t8
f | int -> string -> r0
3 | int
y | string
else | t9
f | int -> string -> r0
x | int
"zero" | string
但请注意,r0 必须被视为bool,因为f x y 的结果用于if 表达式的条件部分,所以让我们将r0 替换为bool。 :
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> t2
fn x => | int -> t4
fn y => | string -> t6
if | t7
f | int -> string -> bool
x | int
y | string
then | t8
f | int -> string -> bool
3 | int
y | string
else | t9
f | int -> string -> bool
x | int
"zero" | string
接下来,整个if表达式的类型必须与then部分的类型相同,它必须与else部分的类型相同。所以t7、t8 和t9 必须都相同。让我们使用t7,我们看到t8 和t9。
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> t2
fn x => | int -> t4
fn y => | string -> t6
if | t7
f | int -> string -> bool
x | int
y | string
then | t7
f | int -> string -> bool
3 | int
y | string
else | t7
f | int -> string -> bool
x | int
"zero" | string
接下来,t7 必须是 bool 类型,因为 f 3 y 和 f x "zero" 的类型都是 bool:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> t2
fn x => | int -> t4
fn y => | string -> t6
if | bool
f | int -> string -> bool
x | int
y | string
then | bool
f | int -> string -> bool
3 | int
y | string
else | bool
f | int -> string -> bool
x | int
"zero" | string
接下来,t6 也必须是 bool,因为我们返回的是 if 表达式的结果:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> t2
fn x => | int -> t4
fn y => | string -> bool
if | bool
f | int -> string -> bool
x | int
y | string
then | bool
f | int -> string -> bool
3 | int
y | string
else | bool
f | int -> string -> bool
x | int
"zero" | string
接下来,t4 必须是 string -> bool 类型,因为这就是它的主体类型:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> t2
fn x => | int -> string -> bool
fn y => | string -> bool
if | bool
f | int -> string -> bool
x | int
y | string
then | bool
f | int -> string -> bool
3 | int
y | string
else | bool
f | int -> string -> bool
x | int
"zero" | string
t2 是什么?必须是body的类型,即int -> string -> bool:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | t0
fn f => | (int -> string -> bool) -> int -> string -> bool
fn x => | int -> string -> bool
fn y => | string -> bool
if | bool
f | int -> string -> bool
x | int
y | string
then | bool
f | int -> string -> bool
3 | int
y | string
else | bool
f | int -> string -> bool
x | int
"zero" | string
最后,ff 的类型t0 必须与分配给ff 的值的类型相同。所以:
Subexpression | Type
---------------------- | ------------------------------------------
val ff = | (int -> string -> bool) -> int -> string -> bool
fn f => | (int -> string -> bool) -> int -> string -> bool
fn x => | int -> string -> bool
fn y => | string -> bool
if | bool
f | int -> string -> bool
x | int
y | string
then | bool
f | int -> string -> bool
3 | int
y | string
else | bool
f | int -> string -> bool
x | int
"zero" | string
这就是你的最终结果。