Thanks!
There are quite a few issues mentioned in your message. Let me address them
separately.
>>The point of `IO` data type in pure language is not about precision. It's
purpose is to control where the source and distribution of side-effects in
your program.
In haskell, it is done in an opposite way: you have one `IO`, that can do
anything and you can split some subset of actions into `IO1`, `IO2` and so
on and the rules how to evaluate (in parallel or in sequence). In fact, it
is very common approach in haskell to define typeclasses for each IO
effect, that is being used in program, like ...
Like Haskell, ATS can be used as a pure language, too.
What is really IO(T) for some type T?
In ATS, we can introduce a linear type IO (for the so-called 'world').
IO(T) in Haskell corresponds to the function type IO -> (IO, T) in ATS.
A type like 'a -> IO(b)' corresponds to a -> IO -> (IO, b), which
corresponds to (IO, a) -> (IO, b)
(uncurrying), which can be written as (!IO, a) -> b. So we have
Haskell: a -> IO(b) corresponds to (!IO, a) -> b in ATS.
A function of the type (!IO, a) -> b is pure in the sense that it can
use/modify the resource it owns.
Here comes what I consider a big advantage of ATS: IO(T) is now separated
into IO and T; in
particular, IO is a linear type, or more precisely, a linear view (linear
type for proofs); we could introduce
so-called view-change functions (which are proof functions) to manipulate
IO. For illustration, we can
have the following proof functions:
prfun IO_split: IO -> (IO1, IO2)
prfun IO_unsplit: (IO1, IO2) -> IO
for some other linear types IO1 and IO2.
We can also have the following locking functions:
fun IO_lock(): IO
fun IO_unlock(IO): void
fun IO_try_lock(): Option_vt(IO)
which make essential use of IO being a linear type (instead of a monad).
When I said that the IO monad lacks precision, I should have probably said
that the IO monad
lacks the kind of directness and expressiveness offered by a linear IO type.
Of course, monads can also offer what linear types cannot. But a stateful
monad like the IO monad
can be readily handled like what is outlined above.
On Tue, Aug 6, 2019 at 12:44 AM Dambaev Alexander <ice.redm...@gmail.com>
wrote:
> Thanks for response.
>
> понедельник, 5 августа 2019 г., 17:56:43 UTC пользователь gmhwxi написал:
>>
>> If I understand correctly, I think I have dealt with this issue before.
>>
>> When an iterator is taken out, you can stop the object from being used
>> until
>> the iterator is returned. For instance, the 'minus' view in
>> PATSHOME/prelude/SATS/extern.sats
>> is precisely introduced for this purpose.
>>
>
> Unfortunately, I am only starting to learn ATS2, so if you can provide a
> simple snippet (not compilable, just to get an idea), which will contain
> main points how `minus` will prevent such errors, that will be great
> starting point for me to investigate another working approaches, that can
> address described issue.
>
> From your description, I imagine, that we can define
> gtk_tree_selection_with_selected (like in Haskell example above), which we
> can use like this:
> fn handler(tree: ptr) = gtk_tree_view_delete_by_index(tree, 0)(* ffi call,
> which removes first row, any iterator is now point to invalid row*)
> implement main0(argc,argv) =
> let
> val tree = gtk_tree_view_new_with_model (...)
> val () = g_signal_connect ("CHDIR", handler, tree)
> val () = gtk_tree_view_selection_with_selected( lam iterator =>
> let
> val () = gtk_tree_view_set_color iterator Blue (* some
> valid action with iterator *)
> val () = g_signal_emit ("CHDIR") (* valid, because ATS is
> not pure, but ATS is somehow will know, that handler will make `iterator`
> to be invalid? *)
> val () = gtk_tree_view_set_color iterator Green (*
> compile time error: iterator is invalid ? *)
> in
> end)
> in
> end
> Given, that iterator is represented as a pointer to GtkTreeIter from gtk2
> and `gtk_tree_view_delete_by_index` is ffi call to some gtk2 function,
> that actually deletes row, which makes any iterator to be invalid. Am I got
> it right? It seems quite optimistic.
>
>
>>
>> To me, a fundamental issue with the IO monad is its lack of precision.
>> Why just one IO? Not IO1,
>> IO2, etc. Say we have two programs P1 and P2; if P1 only uses IO1 and P2
>> only uses IO2, then
>> they can execute in parallel (assuming that IO1 and IO2 are disjoint). If
>> we lump IO1 and IO2 into
>> IO, then parallel execution of P1 and P2 is no longer considered
>> type-safe.
>>
>> The point of `IO` data type in pure language is not about precision. It's
> purpose is to control where the source and distribution of side-effects in
> your program.
> In haskell, it is done in an opposite way: you have one `IO`, that can do
> anything and you can split some subset of actions into `IO1`, `IO2` and so
> on and the rules how to evaluate (in parallel or in sequence). In fact, it
> is very common approach in haskell to define typeclasses for each IO
> effect, that is being used in program, like
> class Monad m => UsesFileSystem m where
> openFile :: String-> IOMode-> m Handle
>
> class Monad m => UsesNetwork m where
> socket :: SocketFamily-> SocketType-> m Socket
>
>
> some_custom_action
> :: ( UsesFileSystem m
> , UsesNetwork m
> , Monad m
> )
> => m ()
> some_custom_action = do
> h <- openFile "test" ReadOnly
> s <- socket AF_UNIX Datagram
> return ()
> which helps with mock tests by allowing usage of `some_custom_action` for
> any monad, that has appropriate instances
>
> In the haskell example above, I had defined `IteratorM` datatype and
> monad, which can be treated as subset of IO (or IO1 from your example) with
> number of actions in it (like `gtk_tree_view_iter_set_color`). The whole
> purpose of it is to forbid composition such `IO1` with other `IO` actions
> (including any other `IO2` actions) and to consider such composition as not
> type-safe. I see no point to run `IteratorM` and `IO2` in parallel as such
> uncontrolled mixing is the source of described issue in a first place.
>
> But, maybe, I just didn't get what you mean in your example with `IO1` and
> `IO2`?
>
> --
> 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/4a5064b4-357e-4055-b1af-44373e076592%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/4a5064b4-357e-4055-b1af-44373e076592%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/CAPPSPLqrHvOYBepyEz%2BmT6K-k%2BPVWHx6cDVm2RquDLk4ZmZDoA%40mail.gmail.com.
