fn 类型的 ml 函数：'a -> 'b答案

【问题标题】：ml function of type fn : 'a -> 'bfn 类型的 ml 函数：'a -> 'b
【发布时间】：2016-04-27 00:17:05
【问题描述】：

功能：

fn : 'a -> 'b

现在，有没有可以定义并具有这种类型的函数？

【问题讨论】：

你能解释一下你想要做什么吗？
是的，目标是什么。
没有这样的函数实际上返回任何东西。（尝试构造一个我刚刚想到的Heffalump 类型的值。）

标签： functional-programming sml ml parametric-polymorphism

【解决方案1】：

我能想到一个例子：

fun f a = raise Div;

【讨论】：

【解决方案2】：

标准 ML 中的函数签名有两种可能的实现。一个使用异常，另一个使用递归：

val raises : 'a -> 'b =
  fn a => raise Fail "some error";

(* Infinite looping; satisfies the type signature, *)
(* but won't ever produce anything.                *)
val rec loops : 'a -> 'b =
  fn a => loops a;

第一个解决方案可能对定义一个辅助函数很有用，比如bug，它可以节省一些击键：

fun bug msg = raise Fail ("BUG: " ^ msg);

另一种解决方案可能对定义服务器循环或 REPL 有用。

在Basis库中，OS.Process.exit就是这样一个返回未知泛型类型'a的函数：

- OS.Process.exit;
val it = fn : OS.Process.status -> 'a

一个类型为val repl = fn : unit -> 'a的小回声REPL：

fun repl () =
  let
    val line = TextIO.inputLine TextIO.stdIn
  in
    case line of
      NONE        => OS.Process.exit OS.Process.failure
    | SOME ":q\n" => OS.Process.exit OS.Process.success
    | SOME line   => (TextIO.print line ; repl ())
  end

这个question about the type signature of Haskell's forever function 也可能对你有用。

【讨论】：

【解决方案3】：

我能想到几个：

递归的，
```
fun f x = f x
```
任何引发异常的函数，
```
fun f x = raise SomeExn
```
任何相互递归的函数，例如，
```
fun f x = g x
and g x = f x
```
任何使用强制转换的函数（需要特定的编译器支持，以下适用于莫斯科 ML），
```
fun f x = Obj.magic x
```
像这样破坏类型系统可能是作弊，但与所有其他具有这种类型的函数不同，这个函数实际上返回了一些东西。（在最简单的情况下，它是恒等函数。）

如果 Collatz 猜想为假则抛出一个函数，如果为真则无限递归，

fun f x =
    let fun loop (i : IntInf.int) =
            if collatz i
            then loop (i+1)
            else raise Collatz
    in loop 1 end

实际上只是前两者的结合。

任何执行任意 I/O 并无限递归的函数，例如

fun f x = (print "Woohoo!"; f x)

fun repl x =
    let val y = read ()
        val z = eval y
        val _ = print z
    in repl x end

有人可能会争辩说异常和无限递归代表相同的理论值 ⊥（底部）表示“没有结果”，尽管由于您可以捕获异常而不是无限递归函数，您也可能会争辩它们是不同的。

如果您将自己限制为纯函数（例如，没有打印或异常）并且只有标准 ML（而不是特定于编译器的功能），并且您认为相互递归的情况在功能上是等效的，尽管他们不同的递归方案，我们回到fun f x = f x。

fun f x = f x 有类型 'a → 'b 的原因或许很明显：类型推断算法假设输入类型和输出类型都是 'a 和 'b 并继续总结函数的唯一约束：f x 的输入类型必须等于 f x 的输入类型，并且f x 的输出type 必须等于 f x 的输出类型，此时 'a 和 'b 类型还没有被进一步特化。

【讨论】：