function effects tags information

[okeuday]

Please provide a function effects tags section in the ATS book when you have a chance. Their usage doesn't seem to have much clarity in general (i.e., not a problem specific to ATS) and it would help to avoid misusing them. Providing the information in the book would also help to make function types clearer when a 0 or 1 is used.

I obtained my information from https://bluishcoder.co.nz/2010/06/13/functions-in-ats.html which was helpful but it seems like !ref needs to be slightly more inclusive to cover reads of global memory that may change during runtime. I made my own cheat-sheet for a core subset of the syntax:

function effect tags:
!ntm - possibly non-terminating (divergent)
!exn - may raise an exception (partial functions)
!ref - write to memory not owned (no proof) or
       read from global memory that may change state during runtime
       (includes file descriptors, not reentrant)
!wrt - write (includes alloc/free) to memory owned (reentrant)
fun0 - mathematical purity (no side-effects) during runtime
fun1 - may have all possible side-effects (default)

operational purity (Haskell's purity) is similar to <!ntm,!exn>
(catching exceptions breaks referential transparency and
 most Haskell source code uses throwIO for raising exceptions,
 so <!ntm> should be closer in practice)

However, I may be wrong in some way.

It also seems to be important to clarify that mathematical purity is only during a single execution and not across all executions on all platforms (so things like handling filenames can have mathematical purity when executed on both Windows and UNIX despite the "/" and "\" difference).

[githwxi]

Unfortunately, this has to wait. I have to be focusing on implementing ATS3 now as I am already falling far behind at this point.

What you wrote about effect tracking in ATS2 is accurate. There is no longer support for tracking effects in ATS3. It could be added in an extension, though.

[okeuday]

@githwxi Ok, no problem. I am disappointed that effect tracking wouldn't be part of the core of ATS3 but I understand it creates extra work. I am hoping effects may remain in the prelude ATS source code (and other ATS source code) so that it can impact the usage of the specific functions, even if it requires an extension to process them.

[okeuday]

@githwxi I wanted to describe an idea which seems beneficial to me, at least for ATS2. If there was a way in ATS2 to say "this function is completely verified" that should be helpful to show how trustworthy the function is.

So, for example, the ifac2 function example in the "Introduction to Programming in ATS" book is considered verified. If a function effects tag value could mark a function to say "this function is completely verified in ATS and all functions it calls are completely verified in ATS", that should help a developer have more trust in that function providing correct outputs for all inputs. An error could occur if the function effects tag value for a verified function was invalid based on function calls within the function (e.g., due to source code changes).

My understanding of a function being verified in ATS is that it is not necessarily a function being completely correct because there isn't an exhaustive equivalence check between the proof and the program, based on the description in the book for "Programming with Theorem-Proving". Is that correct?

[githwxi]

I actually did experiment with this idea many years ago. It prompted me to investigate the possibility of building some kind of trusted code base for functions written in ATS. It is great idea! But I really don't feel that I have energy for this at the moment. Hopefully, we can revisit this.

My understanding of a function being verified in ATS is that it is not necessarily a function being completely correct because there isn't an exhaustive equivalence check between the proof and the program, based on the description in the book for "Programming with Theorem-Proving". Is that correct?

That is correct. It all depends on what types are specified in the program.