How to write for-loops and while-loops in ATS2?

Google Group
1

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()

2

Your syntax may seem intuitive, but its semantics is not so clear.
Also it is quite limited. Say we want to write a loop to process a list:

while (list_isnot_empty(xs)) .<length(xs)>. { … }

Here we use the length of the list as our termination metric.This means that
the function ‘length’ needs to be brought into the domain of constraints,
greatly
complicating constraint-solving. If ‘length’ is added, what about other
functions
like ‘tree_size’. ‘tree_height’, etc.

The constructs for* and while* are taken from Xanadu, a language I designed
and
implemented and played with before ATS. I suggest to stay away from for*
and while*
as type-error message involving these constructs are extremely difficult to
figure out.On Thursday, December 19, 2013 3:11:32 PM UTC-5, Ming Lei wrote:

I’m glad to see this kind of verified for/while loops are already
supported. However, in my opinion the syntax is still not easy enough.

In the examples both the two loops run in the context of their enclosing
functions, and all the variables referenced in the loop bodies have already
been declared above them. Why can’t they inherit the outer environment and
save the seemingly redundant declaration of n and i?

Ideally, the code could be as simple as:

fn fact2_1 {n:nat} (n: int n): int = let

var n: int = n
var res: int = 1
in
while* (n > 0) .. res := res * n; n := n - 1; res

end

fn fact3_1 {n:nat} (n: int n): int = let
var i: int
var res: int = 1
in
for* (i := n; i > 0; i := i - 1) .. res := res * i; res
end

The idea is no need for repetitive declarations for known variables.

On Thursday, December 19, 2013 12:39:02 AM UTC-6, gmhwxi wrote:

That requires more involved syntax:

fun fact2_1
{n:nat} (n: int n): int = let
var n: int = n
var res: int = 1
in
while* {n:nat} .. (n: int n) => (n > 0) (res := res * n; n := n - 1
); res
end

fun fact3_1
{n:nat} (n: int n): int = let
var i: int
var res: int = 1
in
for* {i:nat} .. (i: int i) => (i := n; i > 0; i := i-1) res := res *i
; res
end

On Thursday, December 19, 2013 1:22:53 AM UTC-5, Ming Lei wrote:

Thanks for showing us the example. My guess is that currently we can not
prove the termination of for/while loops, is that correct?

On Thursday, December 19, 2013 12:18:36 AM UTC-6, gmhwxi wrote:

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()

3

I’m glad to see this kind of verified for/while loops are already
supported. However, in my opinion the syntax is still not easy enough.

In the examples both the two loops run in the context of their enclosing
functions, and all the variables referenced in the loop bodies have already
been declared above them. Why can’t they inherit the outer environment and
save the seemingly redundant declaration of n and i?

Ideally, the code could be as simple as:

fn fact2_1 {n:nat} (n: int n): int = let

var n: int = n
var res: int = 1
in
while* (n > 0) .. res := res * n; n := n - 1; res

end

fn fact3_1 {n:nat} (n: int n): int = let
var i: int
var res: int = 1
in
for* (i := n; i > 0; i := i - 1) .. res := res * i; res
end

The idea is no need for repetitive declarations for known variables.On Thursday, December 19, 2013 12:39:02 AM UTC-6, gmhwxi wrote:

That requires more involved syntax:

fun fact2_1
{n:nat} (n: int n): int = let
var n: int = n
var res: int = 1
in
while* {n:nat} .. (n: int n) => (n > 0) (res := res * n; n := n - 1);res
end

fun fact3_1
{n:nat} (n: int n): int = let
var i: int
var res: int = 1
in
for* {i:nat} .. (i: int i) => (i := n; i > 0; i := i-1) res := res *i
; res
end

On Thursday, December 19, 2013 1:22:53 AM UTC-5, Ming Lei wrote:

Thanks for showing us the example. My guess is that currently we can not
prove the termination of for/while loops, is that correct?

On Thursday, December 19, 2013 12:18:36 AM UTC-6, gmhwxi wrote:

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()
4

Here is an example involving a more complex construction of while-loop:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/fibver_loop.datsOn Thursday, December 19, 2013 1:18:36 AM UTC-5, gmhwxi wrote:

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()

5

That requires more involved syntax:

fun fact2_1
{n:nat} (n: int n): int = let
var n: int = n
var res: int = 1
in
while* {n:nat} .. (n: int n) => (n > 0) (res := res * n; n := n - 1);res
end

fun fact3_1
{n:nat} (n: int n): int = let
var i: int
var res: int = 1
in
for* {i:nat} .. (i: int i) => (i := n; i > 0; i := i-1) res := res * i;res
endOn Thursday, December 19, 2013 1:22:53 AM UTC-5, Ming Lei wrote:

Thanks for showing us the example. My guess is that currently we can not
prove the termination of for/while loops, is that correct?

On Thursday, December 19, 2013 12:18:36 AM UTC-6, gmhwxi wrote:

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()
6

Thanks for showing us the example. My guess is that currently we can not
prove the termination of for/while loops, is that correct?On Thursday, December 19, 2013 12:18:36 AM UTC-6, gmhwxi wrote:

Here is some code involving both a for-loop and a while-loop:

//
#include “share/atspre_staload.hats”
//

fun fact (n: int): int =
if n > 0 then n * fact(n-1) else 1

fun fact2
(n: int): int = let
var n: int = n
var res: int = 1
in
while (n > 0) (res := res * n; n := n - 1); res
end

fun fact3
(n: int): int = let
var i: int
var res: int = 1
in
for (i := n; i > 0; i := i-1) res := res * i; res
end

val () = assertloc (fact(10) = fact2(10))
val () = assertloc (fact(10) = fact3(10))

implement main0 () = ()