【发布时间】：2021-07-12 17:43:07
【问题描述】：
我需要找到一个带有以下签名的函数：
'a -> 'b -> ('a * 'b -> 'b) -> 'b
所以我试着这样做：
fun f a b g = g(a,b)
得到了结果：
val f = fn : 'a -> 'b -> ('a * 'b -> 'c) -> 'c
如何根据需要将此c 设置为b？
非常感谢。
【问题讨论】：
【发布时间】：2021-07-12 17:43:07
【问题描述】：
你可以写一个显式的类型注解，例如：
fun f a b (g : _ * 'b -> 'b) = g(a,b)
(* val f = fn : 'a -> 'b -> ('a * 'b -> 'b) -> 'b *)
推断的类型'a -> 'b -> ('a * 'b -> 'c) -> 'c 比你强加的类型'a -> 'b -> ('a * 'b -> 'b) -> 'b 更一般。
关于函数的类型注释，另见this question。
【讨论】：
问题是g(a,b) 不限制结果类型。
您可以访问的'b 类型的唯一值是第二个参数，因此您需要在某个地方返回它，或者使用它来以某种方式限制结果。
一个非常简单的解决方案是添加一个条件，
- fun f a b g = if false then b else g(a,b);
val f = fn : 'a -> 'b -> ('a * 'b -> 'b) -> 'b
附录，几周后，我突然想起了一个更优雅的解决方案，没有丑陋的条件。
由于g 的结果应该与它的第二个参数具有相同的类型，因此您可以为其提供自己的结果。
这将强制 b 和 g(a,b) 具有相同的类型：
- fun f a b g = g(a, g(a,b));
val f = fn : 'a -> 'b -> ('a * 'b -> 'b) -> 'b
【讨论】：
-
如果你在语言中只有隐式类型的表达式，推理是正确的，这是学习静态类型推理的有趣练习。但是该语言确实支持类型注释，因此在实践中您不会引入这样无用的运行时代码。
-
@Maëlan 是的，因为这不是练习，而是理解类型推断的练习，添加显式类型注释是作弊。
-
啊，问题里没写，现在你说，也许是？