SML 语法：`val rec` 和 `fun` 相互比较

Question

有哪些已知的事情是可能的，而不是另一个？有哪些已知的习语可以解决两者中任何一个的限制？

我所知道的

在 another question 中，Andreas Rossberg 指出了适用于 SML 中 val rec 的限制：它必须采用 fn-match 的形式，即使其他表达式也有意义。

fun 语法没有这样的限制，但不能用于引入简单的绑定（我的意思是，只是一个带有可选类型注释的名称，仅此而已），因为它需要公开参数.

在一个我忘记的旧问题中，有离散的 cmets 支持或 fun 超过 val/val rec。

我个人更多地使用val/val rec，因为它暴露了自递归和非自递归绑定之间的区别（虽然暴露为自递归的可能实际上不是，但另一种方式总是成立，暴露为非自递归的东西永远不会自递归），还因为它使用与匿名 lambda 表达式相同的语法（更一致）。

（所有相关的）问题

这些是我所知道的。还有其他人吗？我对任何解决方法的习语知之甚少。有吗？

在我看来，两者的限制都只是句法上的，没有真正的语义或健全性背景。是否确实如此，或者这些限制是否存在语义和合理性背景？

一个样例（可以跳过）

如果不是滥用，我将在 sn-p 下面发布，这是上面链接的问题中发布的一个变体。这个 sn-p 暴露了一个我对两者都有问题的案例（我对这两个都不满意）。 cmets 告诉我这两个问题在哪里以及为什么它对我来说是个问题。此示例无法真正简化，因为问题是语法问题，因此真正的用例很重要。

(* ======================================================================== *)

(* A process chain. *)

datatype 'a process = Chain of ('a -> 'a process)

(* ------------------------------------------------------------------------ *)

(* An example controlling iterator using a process chain. it ends up to be
 * a kind of co‑iteration (if that's not misusing the word). *)

val rec iter =
   fn process: int -> int process =>
   fn first: int =>
   fn last: int =>
      let
         val rec step =
            fn (i, Chain process) =>
               if i < first then ()
               else if i = last then (process i; ())
               else if i > last then ()
               else
                  let val Chain process = process i
                  in step (i + 1, Chain process)
                  end
      in step (first, Chain process)
      end

(* ------------------------------------------------------------------------ *)

(* A tiny test use case. *)

val rec process: int -> int process =
   fn a: int =>
     (print (Int.toString a);
      Chain (fn a => (print "-";
      Chain (fn a => (print (Int.toString a);
      Chain (fn a => (print "|";
      Chain process)))))))

(* Note the above is recursive: fn x => (a x; Chain (fn x => …)). We can't
 * easily extract seperated `fn`, which would be nice to help composition.
 * This is solved in the next section. *)

val () = iter process 0 20
val () = print "\n"

(* ======================================================================== *)

(* This section attempts to set‑up functions and operators to help write
 * `process` in more pleasant way or with a more pleasant look (helps
 * readability).
 *)

(* ------------------------------------------------------------------------ *)

(* Make nested functions, parameters, with an helper function. *)

val chain: ('a -> unit) -> ('a -> 'a process) -> ('a -> 'a process) =
   fn e =>
   fn p =>
   fn a => (e a; Chain p)

(* Now that we can extract the nested functions, we can rewrite: *)

val rec process: int -> int process =
   fn a =>
      let
         val e1 = fn a => print (Int.toString a)
         val e2 = fn a => print "-"
         val e3 = fn a => print (Int.toString a)
         val e4 = fn a => print "|"
      in
         (chain e1 (chain e2 (chain e3 (chain e4 process)))) a
      end

(* Using this:
 *     val e1 = fn a => print (Int.toString a)
 *     val e2 = fn a => print "-"
 *     …
 *
 * Due to an SML syntactical restriction, we can't write this:
 *     val rec process = chain e1 (chain e2 ( … process))
 *
 * This requires to add a parameter on both side, but this, is OK:
 *     fun process a = (chain e1 (chain e2 ( … process))) a
 *)

val e1 = fn a => print (Int.toString a)
val e2 = fn a => print "-"
val e3 = fn a => print (Int.toString a)
val e4 = fn a => print "|"

(* An unfortunate consequence of the need to use `fun`: the parameter added
 * for `fun`, syntactically appears at the end of the expression, while it
 * will be the parameter passed to `e1`. This syntactical distance acts
 * against readability.
 *)

fun process a = (chain e1 (chain e2 (chain e3 (chain e4 process)))) a

(* Or else, this, not better, with a useless `fn` wrapper: *)

val rec process = fn a =>
   (chain e1 (chain e2 (chain e3 (chain e4 process)))) a

(* A purely syntactical function, to move the last argument to the front. *)

val start: 'a -> ('a -> 'b) -> 'b = fn a => fn f => f a

(* Now that we can write `start a f` instead of `f a`, we can write: *)

fun process a = start a (chain e1 (chain e2 (chain e3 (chain e4 process))))

infixr 0 THEN
val op THEN = fn (e, p) => (chain e p)

fun process a = start a (e1 THEN e2 THEN e3 THEN e4 THEN process)

(* This is already more pleasant (while still not perfect). Let's test it: *)

val () = iter process 0 20
val () = print "\n"

Answer 1

val rec 形式计算最小的固定点。在一般情况下，这样的固定点并不总是定义明确或唯一的（至少在严格的语言中不是）。特别是，如果右侧包含需要非平凡计算的表达式，并且这些计算已经依赖于所定义的内容，那么递归绑定的含义应该是什么？

不存在有用的答案，因此 SML（与许多其他语言一样）将递归限制为（句法）函数。这样，它就可以用 Y 等著名的不动点算子进行清晰的语义解释，并且可以给出足够简单的求值规则。

当然，fun 也是如此。更具体地说，

fun f x y = e

仅仅被定义为

的语法糖

val rec f = fn x => fn y => e

因此fun 必须至少有一个参数才能满足val rec 的语法要求。

Answer 2

我将尝试开始回答我自己的问题。

对于由于句法限制而强制使用包装器 fn 的情况（可能是考虑使用 sML 寻址的问题？），我可以找到，不是真正的解决方法，而是一个有助于让这些案例不那么嘈杂。

我重用了示例中的start 函数（参见问题），并将其重命名为n_equiv，原因在评论中给出。这只需要一些事先的措辞来解释 η 等价是什么，并说明证明这个函数的定义和使用合理的句法限制（无论如何这总是有利于学习材料，我打算发布法语论坛上的一些 SML 示例）。

(* A purely syntactical function, to try to make forced use of `fn` wrappers
 * a bit more acceptable. The function is named `n_equiv`, which refers to
 * the η-equivalence axiom. It explicitly tells the construction has no
 * effect. The function syntactically swap the function expression and its
 * argument, so that both occurrences of the arguments appears close
 * to each other in text, which helps avoid disturbance. 
 *)

val n_equiv: 'a -> ('a -> 'b) -> 'b = fn a => fn f => f a

问题示例中的用例，现在看起来像这样：

fun process a = n_equiv a (chain e1 (chain e2 (chain e3 (chain e4 process))))
…
fun process a = n_equiv a (e1 THEN e2 THEN e3 THEN e4 THEN process)

这已经更好了，因为现在清楚地告知周围的构造是中性的。

要回答问题的另一部分，这种情况至少用fun 比用val rec 更容易处理，就像val rec 一样，不能应用n_equiv 自记录习语。这是支持fun 而不是val rec … = fn … 的一点

更新 #1

提到fun 与val 的比较冗长的页面：TipsForWritingConciseSML (mlton.org)。请参阅页面中间的“从句功能定义”。对于非自递归函数，val … fn 比 fun 更简洁，自递归函数可能会有所不同。