State type annotation

Google Group
1

Sometimes, one needs to add a state type annotation
to an if-then-else expression in ATS. Here is a simple example:

//
fun
foo{i:nat}
(x: int(i), y: int(i+1)): void = ()
//
(* ****** ****** *)

implement
main0 () = () where
{
//
var x: int
var y: int
//
val i = (1: intGte(0))
//
val () = (
//
if: [i:nat]
(
x: int(i), y: int(i+1)
) => (i >= 1)
then (x := i; y := x+1)
else (x := 10; y := 11)
//
) : void // end of [val]
//
val () = foo(x, y)
//
val () = println! ("x = ", x, "and y = ", y)
//
} (* end of [main0] *)

Without the annotation, foo(x, y) cannot pass typechecking in ATS.

You can also use state type annotation with case-expressions as well.

Here are some examples:


2

I forgot that the new trend should be using glot.io :slight_smile:

https://glot.io/snippets/eex5kpwvqdOn Saturday, May 21, 2016 at 8:46:53 AM UTC-4, gmhwxi wrote:

Sometimes, one needs to add a state type annotation
to an if-then-else expression in ATS. Here is a simple example:

//
fun
foo{i:nat}
(x: int(i), y: int(i+1)): void = ()
//
(* ****** ****** *)

implement
main0 () = () where
{
//
var x: int
var y: int
//
val i = (1: intGte(0))
//
val () = (
//
if: [i:nat]
(
x: int(i), y: int(i+1)
) => (i >= 1)
then (x := i; y := x+1)
else (x := 10; y := 11)
//
) : void // end of [val]
//
val () = foo(x, y)
//
val () = println! ("x = ", x, "and y = ", y)
//
} (* end of [main0] *)

Without the annotation, foo(x, y) cannot pass typechecking in ATS.

You can also use state type annotation with case-expressions as well.

Here are some examples:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/ifhead.dats

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/casehead.dats