涉及 ATS 中的 andalso 宏的类型检查错误

Question

这里有两段代码我认为是等效的，除了第二段的行数比它应该多：

fun
move_ul
{i:nat}
(
  p: int(i) 
, ms: list0(Int)
): list0(Int) =
if p - 5 >= 0 andalso p % 4 != 0 then
  move_ul(p - 5, cons0(p - 5, ms))
else
  ms



fun
move_ul
{i:nat}
(
  p: int(i) 
, ms: list0(Int)
): list0(Int) =
if p % 4 != 0 then
  if p - 5 >= 0 then
    move_ul(p - 5, cons0(p - 5, ms))
  else
    ms
else
  ms

出于某种原因，第二个在类型检查中幸存下来，第一个没有（未能满足约束）......有人能告诉我为什么吗？

Answer 1

这是由于定义的方式andalso（作为不使用依赖类型的宏）造成的。如果您更改andalso为*（这会重载布尔乘法），则代码的第一个版本应该进行类型检查。

顺便说一下，orelse使用 if 时，类似的情况可以简单地通过替换orelsewith来解决+（这会重载布尔加法）。