>>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.
On Tue, Nov 24, 2020 at 2:23 PM Brandon Barker <brandon.bar...@gmail.com>
wrote:
> 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.
>
> On Tuesday, November 24, 2020 at 1:24:10 AM UTC-5 gmhwxi wrote:
>
>> 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.
>>
>> On Monday, November 23, 2020 at 10:57:41 PM UTC-5 ice.r...@gmail.com
>> wrote:
>>
>>> 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/
>>>
>> --
> 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-users+unsubscr...@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
> <https://groups.google.com/d/msgid/ats-lang-users/af4c0df6-de79-4319-a716-d17a5a98625fn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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 on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpfbx9z%3D1uR_xm3HOk4BwkXFU22%3D4rBYQMMYjVp%3DDPQaw%40mail.gmail.com.
