涉及ATS中的andalso宏的Typechecking错误

2019年7月20日 147次阅读

这里有两段代码,我认为是相同的,除了第二段有更多的行,然后它应该：

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

由于某种原因,第二个存在类型检查,第一个没有(不满足约束)…有人可以告诉我为什么？

最佳答案 这是由于方式和定义(作为不使用依赖类型的宏).如果你改变andalso到*(它会重载布尔乘法),你的代码的第一个版本应该是typecheck.

顺便说一句,如果使用orelse,可以通过替换orelse(使布尔加法重载)来简单地解决类似的情况.

点赞