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.
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.
On Mon, Aug 5, 2019 at 11:41 AM Dambaev Alexander <ice.redm...@gmail.com>
wrote:
> Hi all, I want to popup this topic again.
> And I will start with some context: recently, I had debugged pcmanfm file
> manager's segmentation faults, that happen during navigation through hidden
> folders. I found out, that the cause of this error is in per-directory
> settings of displaying hidden files, which means, that if you will enable
> showing of hidden files in $HOME directory, it will be stored only for this
> directory. So $HOME/another_dir will not display hidden files, until you
> will enable this option for directory explicitly.
>
> Here is sequence diagram of calls, that leads to segfaults (you can
> copy-paste it to stackedit.io, which will render it):
> ```mermaid
> sequenceDiagram
> participant user
> participant side_panel
> participant main_window
> user->>side_panel:1 click on hidden directory
> gtk->>side_panel:2 on_sel_change()
> side_panel->>main_window:3 cancel_pending_chdir()
> side_panel->>gtk:4 emit_chdir_if_needed()
> side_panel->>gtk:5 gtk_tree_selection_get_selected()
> gtk->>side_panel:6 item iterator
> side_panel->>gtk:7 g_signal_emit("CHDIR")
> gtk->>tab_page:8 "CHDIR" signal
> tab_page->>tab_page:9 fm_tab_page_chdir_without_history()
> tab_page->>app_config:10 fm_app_config_get_config_for_path()
> app_config->>tab_page:11 show_hidden=0
> tab_page->>tab_page:12 page->show_hidden=0
> tab_page->>fm_folder:13 fm_folder_view_set_show_hidden(0)
> fm_folder->>fm_folder:14 fm_folder_model_set_show_hidden(0)
> fm_folder->>fm_folder:15 fm_folder_apply_filters()
> fm_folder->>gtk:16 g_signal_emit("row-deleting")
> fm_folder->>gtk:17 g_signal_emit("filter-changed")
> gtk->>fm_folder:18 signal "filter-changed"
> fm_folder->>gtk:19 g_signal_emit("filter-changed")
> gtk->>main_window:20 signal "filter-changed"
> main_window->>main_window:21 on_folder_view_filter_changed()
> main_window->>app_config:22
> fm_app_config_save_config_for_path(show_hidden=0)
> tab_page->>side_panel:23 fm_side_pane_set_show_hidden(0)
> side_panel->>side_panel:24 fm_dir_tree_view_set_property(0)
> side_panel->>side_panel:25 fm_dir_tree_model_set_show_hidden(0)
> side_panel->>side_panel:26 item_hide_hidden_children()
> side_panel->>tab_page:27 show_hidden=0
> side_panel->>gtk:28 g_signal_emit("CHDIR")
> gtk->>main_window:29 signal "CHDIR"
> main_window->>main_window:30 on_side_pane_chdir()
> main_window->>main_window:31 fm_tab_page_chdir()
> side_panel->>side_panel:32 gtk_tree_model_get_path(item iterator)
> side_panel->>side_panel:33 fm_dir_tree_model_load_row(item iterator)
> ```
>
> In this diagram, at step 6 folders gets **iterator**, which will be used
> at steps 32 and 33, but this iterator is already invalid, because at step
> 26 hidden directories will be removed from side panel. This may cause a
> segfault.
> So, I have started to think about how should look gtk2 API(in non-C
> language, for GtkTreeIter, as a small example) to prevent such issues,
> given those requirements:
> 1. usage of ffi calls to gtk2 library(nobody wants to reimplement a wheel,
> right?);
> 2. When GtkTreeIter is in the scope, it should be impossible to add/delete
> content to/from GtkTreeView;
> 3. gtk is not thread-safe library, so don't bother with it in API for now.
>
> Initially, I thought that linear types may be helpful here, but then, I
> had realized, that g_signal_emit() is ffi call, which calls another signal
> handler, which and I doubt, that linear types will be able to track such
> behavior.
> Here is, obviously incorrect snippet(due to my lack of knowledge of ATS2):
> extern fn g_signal_emit(string): void = "ext#"
> extern fn g_signal_connect(name: string, handler: ptr->void, ptr): void =
> "ext#"
>
> fn handler(tree: ptr): void =
> let
> val () = gtk_tree_view_delete_by_index(tree, 0) (* for simplicity,
> let's consider, that this is how it is being deleted *)
>
> implement main0(argc,argv) =
> let
> val (tvpf1 | tv) = gtk_tree_view_new_with_model ()
> (* insert 1 row into tree view *)
> val () = g_signal_connect( "CHDIR", handler, tv)
> val (p | iter) = gtk_tree_selection_get_selected( tvpf1 | tv) (* get
> iterator on a row 0 *)
> val () = g_signal_emit( "CHDIR") (* handler will delete row 0 *)
> val (p | iter) = gtk_tree_model_get_path( p | iter) (* iter is invalid
> here, can ats catch this? *)
> in
> end
>
> So I came to conclusion, that (with my skills), only
> Haskell/Idris/Agda(/Coq?) way of referential transparency is the only way
> to prevent such errors by allowing side effects only inside `IO` "actions".
> Example solution in Haskell (not compilable, just to get the idea):
> Iterator.hs:
> module Iterator
> ( IteratorM -- constructor is not being exported - IteratorM values can
> only be created inside this module
> , Iterator
> , gtk_tree_selection_with_selected
> , gtk_tree_model_get_path
> ) where
> import Foreign.Ptr
> import GtkTreeView
>
> newtype Iterator = Iterator (Ptr ())
>
> newtype IteratorM a = IteratorM
> {
> runIterator :: IO a
> }
>
> -- just
> instance Monad IteratorM where
> (>>=) (IteratorM left) second = IteratorM $
> left >>= \arg->
> case second arg of
> IteratorM next-> next
> return v = IteratorM (return v)
>
> instance Applicative IteratorM where
> pure v = IteratorM (pure v)
> -- :: f (a -> b) -> f a -> f b
> (<*>) (IteratorM first) (IteratorM second) =
> IteratorM ( first <*> second)
>
> instance Functor IteratorM where
> -- :: (a -> b) -> f a -> f b
> fmap f (IteratorM first) = IteratorM (fmap f first)
>
> foreign import ccall "gtk_tree_selection_get_selected" :: Ptr () -> IO
> (Ptr ())
> gtk_tree_selection_with_selected :: GtkTreeView-> (Iterator-> IteratorM
> a)-> IO a
> gtk_tree_selection_with_selected (GtkTreeView tree) nested
> = c_gtk_tree_selection_get_selected tree >> \ptr-> nested (Iterator ptr)
>
> gtk_tree_view_iter_set_color :: Iterator-> Color-> IteratorM ()
> gtk_tree_view_iter_set_color (Iterator iter) color = IteratorM
> (c_gtk_tree_view_iter_set_color iter color)
>
> foreign import ccall "gtk_tree_model_get_path" :: Ptr ()-> Ptr ()-> IO
> (Ptr ())
> gtk_tree_model_get_path :: GtkTreeView-> Iterator-> IteratorM GtkTreePath
> -- let's pretend, that it uses GtkTreeView for simplicity
> gtk_tree_model_get_path (GtkTreeView tree) (Iterator iter) = IteratorM
> (c_gtk_tree_model_get_path tree iter)
> Main.hs
> module Main where
> import Iterator
> import GtkTreeView
>
> foreign import ccall "g_signal_emit" g_signal_emit:: Ptr CChar -> IO ()
> foreign import ccall "g_signal_connect" g_signal_connect :: Ptr CChar->
> (Ptr ()-> IO ())-> Ptr () -> IO ()
>
>
> handler :: GtkTreeView-> IO ()
> handler tree = gtk_tree_view_delete_by_index tree 0 -- deleting first row
>
> main :: IO ()
> main = do
> tree <- gtk_tree_view_new_with_model
> g_signal_connect "CHDIR" handler tree
> -- insert 1 row into tree here ...
> gtk_tree_selection_with_selected tree $ \iter-> do
> let a = 1 + 2 -- valid, can use pure expressions inside IteratorM
> path <- gtk_tree_model_get_path iter -- valid
> gtk_tree_view_set_color iter Blue -- valid
> {- g_signal_emit "CHDIR" -- compile time error here, as it not
> IteratorM -}
> g_signal_emit "CHDIR" -- valid here, as we are not anymore inside
> gtk_tree_slection_with_selected nested: iter is out of scope now
>
>
> One possible issue here is that Iterator value can escape from
> `gtk_tree_selection_with_selected` function, but this can be fixed with
> return type of `IO ()`.
>
> So this example motivates me to search for ability to have similar
> modeling of side effects in ATS2 by using something like `datatype IO
> (a:t@ype) = IO of (RealWorld-> (RealWorld, a)`.
> Or am I missing something and this issue can be solved in ATS2 as well,
> without rewriting standard library and patching compiler?
>
>
>
> --
> 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/3a2e5526-0dc7-41f0-b992-340b0e6a5564%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/3a2e5526-0dc7-41f0-b992-340b0e6a5564%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/CAPPSPLp%2BofZarS6h0ZNN5zhbnyYd97-T-cY3b367BzPhvXwcng%40mail.gmail.com.
