Unexpected/confusing <cloref1> behavior

[Srdjan Mitrovic]

Hi! First time using both google groups and ATS, so forgive me if this is a really dumb question or the wrong spot but this seems like the best place to get in contact with other ATS people :p

I'm working through the intro to programming in ATS book, and in this section it says that you should denote functions which use a value not at the top level nor in the function arguments with <cloref1>.

In the next section on higher order functions, there's a function which is supposed to find the first natural number root of a given polynomial. The example given looks like this:

fun rtfind
  (f: int -> int): int = let
  fun loop (
    f: int -> int, n: int
  ) : int =
    if f(n) = 0 then n else loop (f, n+1)
  // end of [loop]
in
  loop (f, 0)
end // end of [rtfind]

I was a little curious, so I removed `f` from the inner `loop` function and re-compiled, curious to see if I would get an error for having not included <cloref1>

fun rtfind

  (f: int -> int): int = let

  fun loop (

    n: int

  ) :(* <cloref1> *) int =

    if f(n) = 0 then n else loop (n+1)

in

  loop (0)

end

As it is, this works fine, but what I found more surprising was that uncommenting <cloref1> results in this:

am I missing something here? I have atspre_staload.hats included in my file fwiw

[Richard]

Hello Srdjan,

On Saturday, June 1, 2019 at 1:12:35 AM UTC-4, Srdjan Mitrovic wrote:

Hi! First time using both google groups and ATS, so forgive me if this is a really dumb question or the wrong spot but this seems like the best place to get in contact with other ATS people :p

Glad you found the right place and all questions are always welcome!

 

I'm working through the intro to programming in ATS book, and in this section it says that you should denote functions which use a value not at the top level nor in the function arguments with <cloref1>.

Perhaps things have changed a bit since the time the book was written or the example given is potentially misleading. 

I tested the code and looked over the C output and although the function (without closure annotation) still requires enivromental variables from the outside (i.e. n), a closure is not created.

 

In the next section on higher order functions, there's a function which is supposed to find the first natural number root of a given polynomial. The example given looks like this:

fun rtfind
  (f: int -> int): int = let
  fun loop (
    f: int -> int, n: int
  ) : int =
    if f(n) = 0 then n else loop (f, n+1)
  // end of [loop]
in
  loop (f, 0)
end // end of [rtfind]

I was a little curious, so I removed `f` from the inner `loop` function and re-compiled, curious to see if I would get an error for having not included <cloref1>

fun rtfind

  (f: int -> int): int = let

  fun loop (

    n: int

  ) :(* <cloref1> *) int =

    if f(n) = 0 then n else loop (n+1)

in

  loop (0)

end

As it is, this works fine, but what I found more surprising was that uncommenting <cloref1> results in this:

am I missing something here? I have atspre_staload.hats included in my file fwiw

When annotating the function with :<cloref1> means that the function is a closure and so the compiler needs to allocate memory for creating this environment. 

This is why the error (which in this case is a warning from the linker/loader) states that there is an undefined reference to 'atsruntime_malloc_undef'. 

Basically you just need to add a compiler flag (-DATS_MEMALLOC_LIBC)

the full command would be,

patscc -DATS_MEMALLOC_LIBC -o hofs hofs.dats

Hope that helps!

[gmhwxi]

Welcome!

The book was written several years back.

ATS has since evolved a lot. For instance, rtfind could

be implemented as follows in ATS-Temptory:

fn
rtfind
(
f: int -> int
): stream_vt(int) =
(
stream_vt_filter
(sint_streamize_gte(0))
) where
{
  impltmp
  stream_vt_filter$test<int>(n) = (f(n) = 0)
}

Returning a stream of all the roots of a given function 'f' makes

'rtfind' a lot more flexible.

The "classical" ATS code tends to be like code in C or ML. Newer ATS code

emphasizes a lot more on "batch-processing". Please find some explanation

and documentation in the following directory and also some coding examples:

https://github.com/githwxi/ATS-Temptory/tree/master/docgen

On Saturday, June 1, 2019 at 1:12:35 AM UTC-4, Srdjan Mitrovic wrote:

[Srdjan Mitrovic]

A little late on the reply, but thanks for the help guys, really appreciate it!

On Saturday, June 1, 2019 at 5:57:34 PM UTC-4, gmhwxi wrote:

Welcome!

The book was written several years back.

ATS has since evolved a lot. For instance, rtfind could

be implemented as follows in ATS-Temptory:

fn
rtfind
(
f: int -> int
): stream_vt(int) =
(
stream_vt_filter
(sint_streamize_gte(0))
) where
{
  impltmp
  stream_vt_filter$test<int>(n) = (f(n) = 0)
}

Returning a stream of all the roots of a given function 'f' makes

'rtfind' a lot more flexible.

The "classical" ATS code tends to be like code in C or ML. Newer ATS code

emphasizes a lot more on "batch-processing". Please find some explanation

and documentation in the following directory and also some coding examples:

https://github.com/githwxi/ATS-Temptory/tree/master/docgen

That looks quite a bit nicer - will I be able to use this syntax with ATS2 (postiats)? Or do I need to remove that and get temptory instead?

[gmhwxi]

Temptory and ATS-Postiats use the same syntax.

But the library code for Temptory is different from that for the latter.

Installing Temptory is the same as installing ATS-Postiats:

https://sparverius.github.io/tmplats-doc/

Just make sure that TEMPTORY is set (instead of PATSHOME).