Read IO and Write IO

[gmhwxi]

Because tracking effects is no longer planned in ATS3, we need to

think about how to handle effects incurred by calling external functions.

We can introduce an abstrace linear VIEW IO:

absview IO

Say a function foo needs to do IO. Then it has to have a proof of the view IO:

fun foo(!IO | ...): ...

This is just a monadic style of handing effects in Haskell.

IO is so-called because there is I and O in IO. So we may also introduce

absview I and O

and proof functions

prfun IO_split : IO -> (I, O)

prfun IO_unsplit: (I, O) -> IO

If a function only does I but no O, then it only needs a proof of the I view:

fun foo2 (!I | ...): ...

Again, this is just a note put here as a reminder.

[Richard]

Wow. So simple yet powerfully insightful.

[Julian Fondren]

On Thursday, August 8, 2019 at 8:24:02 AM UTC-5, gmhwxi wrote:

Because tracking effects is no longer planned in ATS3, we need to

think about how to handle effects incurred by calling external functions.

We can introduce an abstrace linear VIEW IO:

absview IO

Say a function foo needs to do IO. Then it has to have a proof of the view IO:

fun foo(!IO | ...): ...

This is just a monadic style of handing effects in Haskell.

This seems very similar to how Mercury handles I/O: the program entry point gets (and requires back) a unique value representing the state of the world, and Mercury's uniqueness system requires that this be value be singly-threaded throughout the program, allowing the 'optimization' of in-place modifications to the universe, i.e., side-effects.

So you have

1. a type 'io.state'

2. the main entry point and all I/O functions supplying and requiring a value of this type, with 'destructive input' and 'unique output' parameters to enforce its uniqueness

3. something in the implementation that prevents all this value-passing from causing any work at runtime

This system is very easy to work with. Going with an absview instead of a (Mercury-like) viewtype makes it more obvious that nothing happens at runtime.

OTOH, I thought ATS3 was supposed to be easier than ATS2? :-) Is it so much easier in other respects that making it pure is fine?

IO is so-called because there is I and O in IO. So we may also introduce

absview I and O

and proof functions

prfun IO_split : IO -> (I, O)

prfun IO_unsplit: (I, O) -> IO

If a function only does I but no O, then it only needs a proof of the I view:

fun foo2 (!I | ...): ...

Again, this is just a note put here as a reminder.

Even though the term is I/O, I don't think it's a useful distinction to separate I from O. The most basic interaction is prompted input, which requires the prompt. Graphically, in order to receive a click to a button, you have to show the dialog window with the button. And, the prompt absolutely must happen before the input: even if you separate I and O, they can't be separately ordered so that some runs of the program would show the prompt after asking for the input. Operations like 'make directory' and 'delete a file' need to be treated like I/O but don't much make sense as either I or O, and even if you suggest that they're O, the program can gain information from the result of these operations.

[Julian Fondren]

On Thursday, August 8, 2019 at 5:27:34 PM UTC-5, Julian Fondren wrote:

Even though the term is I/O, I don't think it's a useful distinction to separate I from O.

I see that this came up in the other thread, where you were more interested in the types making sense with concurrency.

Mercury hand-waves this with:

    % spawn(Closure, IO0, IO) is true iff `IO0' denotes a list of I/O
    % transactions that is an interleaving of those performed by `Closure'
    % and those contained in `IO' - the list of transactions performed by
    % the continuation of spawn/3.
    %
:- pred spawn(pred(io, io), io, io).
:- mode spawn(pred(di, uo) is cc_multi, di, uo) is cc_multi.

Where 'cc_multi' stands for 'committed choice multideterminism'. There's a whole universe of possible outcomes, and, er, *something* will happen, and the program will stick with that outcome.

[Hongwei Xi]

>>Even though the term is I/O, I don't think it's a useful distinction to separate I from O

I was thinking of using 'I' to handle read-only memory access.

If a function only needs to read from a shared array, then only a proof of the view 'I' is needed.

For instance, performing binary search on an array is such a case.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/d5118001-9937-4dba-9cae-8a644017b8e7%40googlegroups.com.

[Hongwei Xi]

>>OTOH, I thought ATS3 was supposed to be easier than ATS2? :-) Is it so much easier in other respects that making it pure is fine?

"non-pure" style is still supported:

fun print(i: int): void =

{

  val IO = IO_acquire()

  val ( ) = print_pure(IO, i)

  val ( ) = IO_release(IO)

}

On Thu, Aug 8, 2019 at 6:27 PM Julian Fondren <julian....@gmail.com> wrote:

--

[Kiwamu Okabe]

Dear Hongwei,

On Thu, Aug 8, 2019 at 10:24 PM gmhwxi <gmh...@gmail.com> wrote:
> We can introduce an abstrace linear VIEW IO:

I have a just question.
"Why do we separate the IO functions from the pure function?"

Unfortunately, I have not felt that such separation is useful...

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

Sometimes, a programmer may want to track IO effects.

If you don't want to track IO effects, then you don't really

feel the difference.

On Friday, August 9, 2019 at 2:25:25 AM UTC-4, Kiwamu Okabe wrote:

Dear Hongwei,

[M88]

This seems very versatile and flexible.

I like the idea of I/O tracking being opt-in and very specific.  I often find that only one type of effect is of interest, and tracking the rest can get in the way. 

I recently used a similar technique to track drawing to the screen (using an absview, "DRAWING").  This helped annotate function signatures, as well as provide meaningful restrictions for effects.

I do wonder how this change might affect proofs. If it's no longer possible to mark a function as "pure", can any function be used in a proof-function so long as it typechecks?

[Kiwamu Okabe]

Dear all,

On Fri, Aug 9, 2019 at 8:53 PM gmhwxi <gmh...@gmail.com> wrote:
> If you don't want to track IO effects, then you don't really
> feel the difference.

Umm... There will be an option to write ATS3 code without any IO effects.

Example:
If I create my own prelude library without IO effect,
I can write my code without any IO?

[Hongwei Xi]

>>I can write my code without any IO?

Yes, you should be able to program in the same way as you do now.

--Hongwei

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DJnwDYDzC4%3Dj--dcYqLh4AJYr2pqdtmBA2AioDqngH%3Dg%40mail.gmail.com.

[Kiwamu Okabe]

On Sat, Aug 10, 2019 at 10:17 AM Hongwei Xi <gmh...@gmail.com> wrote:
> Yes, you should be able to program in the same way as you do now.

Thanks. It's good news to port my idiomaticca project to ATS3.

[Hongwei Xi]

>>I do wonder how this change might affect proofs. If it's no longer possible to mark a function as "pure", can any function be used in a proof-function so long as it typechecks?

Good point!

There will still be "pure" functions;

such functions can be used in proof construction.

Given that the word "pure" is already taken, maybe we

could call them "proof-like" functions.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/58633b60-e4fe-466e-8f84-329bc6499f30%40googlegroups.com.

[Brandon Barker]

I like this. Also, this later discussion reminds me of ZIO in Scala.
The trouble only really starts when you import the non-pure code and
want to use it from pure code. In that case, you can either go with
the default assumption it has all effects ("regular IO"), or annotate
it as having specific effects, if you really know what is going on. So
practically speaking, not much trouble, though it does leave room for
erroneous modeling of effects.

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrC5K7Zcya6tw-RV8DMFGjH0oaQW7PiSJrkE0QQfS5foA%40mail.gmail.com.



--
Brandon Barker
brandon...@gmail.com

[Hongwei Xi]

>>So practically speaking, not much trouble, though it does leave room for
>>erroneous modeling of effects.

Well, this is really unavoidable.

If you think about it, there is a even bigger issue. Say you call function 'foo'

in your code. How do you even know that 'foo' should be called in the first place?

Usually, it is all based on your understanding of 'foo'? How do you even know that

your understanding of 'foo' is correct? I think I should stop here :)

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRr5PN7ye6u1FgfWGKRfynmEhQq3hn3_TY2h%2BLb%2BffXjgA%40mail.gmail.com.

[Brandon Barker]

Good point! 

Delayed reply, though the updated status on ATS3 lead me to revisit this discussion.

Is there a current (or planned update) on how pure function tracking can be achieved? 

Best,

[gmhwxi]

At this point, I would say that effect tracking is to be supported

by an external tool. Here is the basic design that has gradually formed

in my mind:

Say that you want to know whether a specific kind of effect (e.g, sending

email, drawing, locking/unlocking) is to be generated at run-time. You can

supply a file in which you list the names of the functions that can potentially

generate such effects; the tool takes the information given in the file to generate

a report. Of course, there are a lot of details and varieties :)

[Dambaev Alexander]

Maintaining some external file seems to me as something, which is easy to ignore or easy to forget about and without some scatch of of example of usage, I can't see how it will be helpful at all.

For example:

```

fn foo(): void = println!("hello")

implement main0() = foo()

```

and the external file contains:

```

console: println

```

Do you mean, that such external tool should require foo and main0 to be listed in such file?

In this case, it will still be absent in types so it will be hard to answer a questions like: "what effects contains foo?" or main0 as well.

In contrast, by using proof arguments you will actually see, that in order to use foo you need to pass IO:

so it is clearer to understand, but more verbose as well, as main0 will be probably a source of all kind of effects, like:

```

extern prfn use_console( !IO): Console

fn

  foo

  ( console: !Console

  |

  ): void = println!( console, "hello")

implement main0(io | ) = {

  prval console = use_console( io)

  val () = foo( console | )

}

```

another interesting approach will be to wrap the exceptions (ie, the goal is to see in types which exceptions are possible to be thrown from function), so $raise should have type like:

```

extern fn

  $raise

  {a:type}{b:type| // is there an exception sort?

  ( !Throws(a)

  | a

  ): b

```

then `try` should require `!IO` and bring `Throws(a)` for all branches in `with`, like:

```

fn

   foo

  ( Throws( DivisionByZero)

  , Throws(FileNotFound)

  | a: int

  , b :int

  ): int = a / b

implement main0() =

try

  ( try foo() with // I am not sure if foo() will be able to use Throws(..) implicitely

  | ~DivisionByZero() => ... // this brings Throws(DivisionByZero) into the scope and only within this block of try ... with

  ) with

  | ~FileNotFound() => ... // this brings Throws(FileNotFound) into the scope

```

but of course, this looks like Haskell's typeclasses from https://www.well-typed.com/blog/2015/07/checked-exceptions/

[gmhwxi]

Thanks for the message!

What I said is not in conflict with what you described in the message.

An external tool for tracking effects can be quite useful in large scale programming.

Deciding what effects should be tracked is often open-ended; what is decided today

may not be what is wanted tomorrow.

The type-based approach you described becomes quite burdensome once higher-order

functions are present. A big difficulty in effect-tracking lies precisely in handling higher-order

functions.

[Dambaev Alexander]

You may be right. Can you provide some scatch of your view just to check it out? :)

вт, 24 нояб. 2020 г. в 06:24, gmhwxi <gmh...@gmail.com>:

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/e90611de-5efc-46e2-8d45-61db522c73f1n%40googlegroups.com.

[Brandon Barker]

Would it still be better to include the effects in the source file, and then pass to the compiler (or 3rd party tool) which effects are to be tracked, and possibly how they are tracked?

Advantages of this approach to me seem that:

 - Easily viewable from the source (as was already mentioned)

 - If an effect isn't being used, though it is listed in the source, the effect checker could emit a warning or error (configurable).

 - Encourages use of effects: I worry that without effect tracking, we gain less confidence in the rest of the ATS3 ecosystem. This is similar to the state of play with Mypy and Python's gradual typing (and I'll note that there, types are annotated in the code as one would expect), except we're only talking about effect types and not types in general: most python libraries don't use typings, so even if you are vigilant in your own code, it is much harder to sometimes understand what effects are happening in libraries. Of course, ultimately much of what we do is built on FFIs of some sort, and a certain degree of trust has to be exercised at that level, but I feel like without some degree of standardization with regard to a basic set of effects, and encouraging their use, it could result in them not being very useful due to fractured use within the ATS3 ecosystem.

[Hongwei Xi]

>>Would it still be better to include the effects in the source file,

If we look at a bigger picture, it may not even be practical to require that this kind of information be stored

in the source. Today it is effect-tracking, and tomorrow it will surely be something else. And there is only so

much that you can put in the source file without causing conflicts.

--
You received this message because you are subscribed to a topic in the Google Groups "ats-lang-users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ats-lang-users/HtsSq9thpk8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/af4c0df6-de79-4319-a716-d17a5a98625fn%40googlegroups.com.

[gmhwxi]

>>You may be right. Can you provide some scatch of your view just to check it out? :)

Unfortunately, I don't have concrete stuff to show at this moment.

To me, effect-tracking is not type-theoretic; it is just a form of so-called flow analysis.

The approach described in your message traverses the syntax tree by piggy-backing

on the Haskell type-checker.

Tracking exceptions has been done many times by many different people (e.g., David Gifford,

Alex Aiken, K-G. Yi). I remember attending a POPL talk (about 20 years ago) by Xavier Leroy;

it was about some kind of effect-tracking system he implemented for OCaml. Immediately after

he finished the talk, Matthias Felleison, who was standing behind me, shouted out a comment

claiming that they did something similarly for Racket(?) and found it to be USELESS :)

In the presence of higher-order functions, accurate flow analysis is very difficult to achieve if not

practically impossible. To me, the key to success lies in flow-analyzing code containing very few

higher-order functions (if they cannot be completely removed). Instead of performing effect-tracking

on source code, it is likely more effective to do it on intermediate representations (e.g., XATSCML and

XATSCL0).

Cheers!

--Hongwei