ats - 涉及 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至 * (重载 bool 乘法)，您的代码的第一个版本应该进行类型检查。

顺便说一句，如果orelse使用，类似的情况可以简单的通过替换orelse来解决与 + (它重载了 bool 加法)。