Re: Tracking effects in ATS

2019-08-08 Thread Kiwamu Okabe
Dear Hongwei, On Thu, Aug 8, 2019 at 10:03 PM gmhwxi wrote: > In practice, I feel that tracking effects in ATS2 is NOT very useful: > too many false positives; increased complexity in programming; etc. Yes. I don't use such mark for my functions. I love just ML style programming. In the past,

Re: Read IO and Write IO

2019-08-08 Thread 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,

Re: Read IO and Write IO

2019-08-08 Thread 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

Re: Read IO and Write IO

2019-08-08 Thread 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.

Re: Read IO and Write IO

2019-08-08 Thread 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

Read IO and Write IO

2019-08-08 Thread Richard
Wow. So simple yet powerfully insightful. -- 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-users+unsubscr...@googlegroups.com. To view this discussion

Read IO and Write IO

2019-08-08 Thread 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 |

Tracking effects in ATS

2019-08-08 Thread gmhwxi
In ATS2, the type system is supposed to track the following effects: ref: this roughly corresponds to the IO effect wrt: this means modifying "owned" memory (vs. shared memory) exn: raising exceptions ntm: non-termination In practice, I feel that tracking effects in ATS2 is NOT very useful: too

ATS as a runtime-less and library-less language

2019-08-08 Thread gmhwxi
Over the years, I have been trying to turn ATS into a runtime-less and library-less language. Runtime-less means that a runtime can be provided by the user. Similar, library-less means that different styles of libraries can be chosen by the user. I don't have more to say right now. Just want to

Re: Referential transparency in ATS

2019-08-08 Thread Artyom Shalkhakov
Hi Brandon, Alexander, On Wednesday, August 7, 2019 at 5:31:04 AM UTC+3, Brandon Barker wrote: > I just want to say this is quite intriguing, I think it would be very > appealing to have a standard library built on this idea (a modification of > Temptory?), perhaps with some more fleshed out