>>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
>>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
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)
-
You may be right. Can you provide some scatch of your view just to check it
out? :)
вт, 24 нояб. 2020 г. в 06:24, 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
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
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
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
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,
On Friday, August 9, 2019 at 9:34:32 PM UTC-4 gmhwxi wrote:
>
> >>So practically speaking, not much
>>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
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
>>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
On Sat, Aug 10, 2019 at 10:17 AM Hongwei Xi 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.
--
Kiwamu Okabe at METASEPI DESIGN
--
You received this message because you are subscribed to the Google Groups
>>I can write my code without any IO?
Yes, you should be able to program in the same way as you do now.
--Hongwei
On Fri, Aug 9, 2019 at 8:43 PM Kiwamu Okabe wrote:
> Dear all,
>
> On Fri, Aug 9, 2019 at 8:53 PM gmhwxi wrote:
> > If you don't want to track IO effects, then you don't really
>
Dear all,
On Fri, Aug 9, 2019 at 8:53 PM gmhwxi 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
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,
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,
>
> On Thu, Aug 8, 2019 at 10:24 PM gmhwxi <...> wrote:
> > We can
Dear Hongwei,
On Thu, Aug 8, 2019 at 10:24 PM gmhwxi 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
>>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,
>>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
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.
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
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
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 |
23 matches
Mail list logo
