涉及 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，类似的情况可以简单地通过将 orelse 替换为 + 来解决（这会重载布尔加法）。

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

Typechecking error involving the andalso macro in ATS

ats