CODEWITHSUNDEEP
ats
Daren McCulley
Daren McCulley

Reputation: 73

Typechecking error involving the andalso macro in ATS

Here are two pieces of code I think are equivalent aside from the second one having more lines then it should:

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

For some reason the second one survives type checking and the first does not (failure to satisfy constraints)... can someone tell me why?

Upvotes: 6

Views: 92

Answers (1)

Hongwei Xi
Hongwei Xi

Reputation: 935

This is due to the way andalso is defined (as a macro that does not use dependent types). If you change andalso to * (which overloads the boolean multiplication), the first version of your code should typecheck.

By the way, if orelse is used, a similar situation can simply be resolved by replacing orelse with + (which overloads the boolean addition).

Upvotes: 3

Related Questions