implement
main0 () = {
val () = let
val ha = print("ha")
in
(ha; ha) // How to get two ha's here?
end
}
I think that might have do with laziness? If you have a
side-effecting expression and you try to pretend it's
call-by-need, then bad things happen (beta reduction is no longer
valid!)
Do you have an example in OCaml? I admit I am curious as to why
their compiler would do such a thing.
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com.
I think that might have do with laziness? If you have a side-effecting expression and you try to pretend it's call-by-need, then bad things happen (beta reduction is no longer valid!)
Do you have an example in OCaml? I admit I am curious as to why their compiler would do such a thing.
let val ha = (print "ha") in ha; ha end
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com.
--
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b5eac771-323c-da14-e639-b7e1822a4185%40iohk.io.
>>ATS doesn't seem to allow a sequence expression in the "in" position of a let expression,It does. You can write:implement
main0 () =
let
val ha = print("ha")
in
ha; ha
end
$ patscc -o haha haha.dats
In file included from haha_dats.c:15:0:
haha_dats.c: In function 'mainats_void_0':
haha_dats.c:179:26: error: 'tmp1' undeclared (first use in this function)
ATSINSmove_void(tmpret0, tmp1) ;
^
/nix/store/q8ll64apv4nn6x4dxprkjx29n3kwsraw-ats2-0.3.11/lib/ats2-postiats-0.3.11/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of macro 'ATSINSmove_void'
#define ATSINSmove_void(tmp, command) command
^~~~~~~
haha_dats.c:179:26: note: each undeclared identifier is reported only once for each function it appears in
ATSINSmove_void(tmpret0, tmp1) ;
^
/nix/store/q8ll64apv4nn6x4dxprkjx29n3kwsraw-ats2-0.3.11/lib/ats2-postiats-0.3.11/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of macro 'ATSINSmove_void'
#define ATSINSmove_void(tmp, command) command
^~~~~~~
implement
main0 () = {
val () = let
val ha = print("ha")
in
ignoret(ha; ha)
end
}
I'm a little rusty, so can't come up with many good examples.Apparently it is possible to do something like this in OCaml:
implement
main0 () = {
val () = let
val ha = print("ha")
in
(ha; ha) // How to get two ha's here?
end
}
let ha = (print_string "ha") in ha; ha
Hi Artyom,I'm also grappling with the issue of RT in this case as I'd so far only thought about it in terms of function calls, but what you and Vanessa say helped me to understand the issue. Though I haven't managed to get ATS to have the same behavior as OCaml in the "let expression" above, I suspect it is possible. The key phrase here seems to be "side-effecting expression", and relates to the fact that functions in ATS can perform side effects without having any effect type or IO monad ascribed to the value (again, iirc).
I'm not sure what the point of an IO monad is in a strict
language - Haskell has good reason to employ them, but I don't
think it's really worth it in other cases (at least, I actually
know much about PureScript, but I don't think ATS needs it).
I think the way that ATS uses linear types for IO is slightly
different - it uses them to e.g. ensure a handle is closed.
Linearity does also have the curious benefit of making it possible
to have lazy/strict evaluation be the same; you can rule out the
example you provide and you can rule out the bottom type.
Cheers,
Vanessa McHale
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5391973a-4bd4-4238-a007-4dc08d1d9d4d%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b21006ff-bc7e-d828-1462-4d9c7103feae%40iohk.io.
One can definitely build a monad-based library to support IO:absvtype IO(a:vt@ype) = ptr
The problem with IO monad is that it is so broad. With linear types,a programmer can specify a lot more precisely.
>>is that ATS doesn't (by default?) model an IO effect.No, it doesn't if you use the default library. But nothing prevents youfrom tracking IO effects in ATS.
In the book you mentioned in your message, I was really thinking ofviews for specifying memory layouts. With linear views, a programmercan be very precise in describing what memory a function can access/update.Compared to state monads, this kind of precision is unmatched.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.
module Main
import Effects
import Effect.StdIO
hello : Eff () [STDIO]
hello = let ha = StdIO.putStr "ha" in ha *> ha
main : IO ()
main = run hello
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/85a9cc71-d4e1-4168-94fa-ba64ae53561d%40googlegroups.com.
And for what it's worth, here is an Idris program for haha using Effects:
module Main
import Effects
import Effect.StdIO
hello : Eff () [STDIO]
hello = let ha = StdIO.putStr "ha" in ha *> ha
main : IO ()
main = run helloIt prints "ha" twice, despite being a strict language. I presume, but am not sure, this is because the effect time requires it to be re-evaluated each time.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.
Hi Brandon,This is a very lively discussion, thanks for bringing it up.
On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:And for what it's worth, here is an Idris program for haha using Effects:
module Main
import Effects
import Effect.StdIO
hello : Eff () [STDIO]
hello = let ha = StdIO.putStr "ha" in ha *> ha
main : IO ()
main = run helloIt prints "ha" twice, despite being a strict language. I presume, but am not sure, this is because the effect time requires it to be re-evaluated each time.Well, the type of "hello" says that the computation will use the STDIO effect as many times as is necessary. The way the computation is constructed, it is meant to issue commands in a given sequence.One peculiarity of PureScript is that of handling effects via the algebraic effects approach. It's not easy to do in a high-performance way, because you need a call/cc construct present in the language, and moreover a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, once or more times by the effect interpreter). In ATS a simpler way is to use template functions to define effects differently (e.g. during testing and during the actual execution) -- it's constrained compared to the call/cc for sure, but then you don't have to pay the price of the call/cc plumbing. Another thing about PureScript is that it uses row types to track the set of effects that a given Eff computation may involve during its evaluation.
So in short, if we view the programs as creating commands, and then some kind of external interpreter that executes them, then it all matches up. The programs might be quite pure and non-side-effecting (except for non-termination aka infinite looping runtime exceptions), the interpreter will perform the effects. Here's a pseudocode for the interpreter:// the command sub-languagedatatype Command = Print of string | Nop | Seq of (command, command)externfun runCommand (c:Command): voidexternfun seq (c:Command, Command): Commandexternfun cprint (s:string): Commandimplementseq (c1, c2) = Seq (c1, c2)implementcprint (s) = Print s// the interpreter itselfimplementrunCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | Seq (c1, c2) => (runCommand(c1); runCommand(c2))Now let's assume the Command is abstract for the rest of the program (and only the runCommand, seq and print are exposed). We can now write:val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the effect!implementmain0 () = runCommand helloThe "hello" itself is free of side-effects (or so it seems to me!). We might need to lazily evaluate stuff here (e.g. to enable looping, where you need to give the interpreter the chance to run side-by-side with your expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" operator for stitching together the commands such that the left-hand side has to be evaluated to a value that is then fed to the right-hand side -- i.e. incrementally built-up as it's being evaluated by the interpeter).In Haskell, the type Command is termed "IO" (with an additional type parameter to signify the result type of the command) and the interpreter is somewhere in the runtime system.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com.
Function effects tags (not real keywords):
ntm
exn
ref
wrt
all
Special functions/values (not keywords and invalid as identifiers):
$effmask
Do you have or plan on having a repo to play around with this idea? If not I may try to start one (at some point).
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9ff2fb00-6790-4541-9bc0-0a949a0c46e3%40googlegroups.com.
Sounds like I have to fix atspkg :p
If you want to use the monads package with npm + Makefiles, I
suppose I could upload to npm (it might even be a good idea given
the permanence of packages there).
As an aside: I suspect that what makes IO so nice in the context
of Haskell is that you get the same result for the same inputs,
every time. It turns out that many operations involving
reads/writes to memory still satisfy this - and one would like to
be able to express that, though I suspect it would be difficult.
Cheers,
Vanessa McHale
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2a3ab922-0844-484e-8131-24f76f61cf96%40googlegroups.com.
Hey Artyom,Thanks for the very interesting analysis and response.
On Fri, Mar 22, 2019 at 4:06 AM Artyom Shalkhakov <artyom.s...@gmail.com> wrote:Hi Brandon,This is a very lively discussion, thanks for bringing it up.
On Friday, March 22, 2019 at 5:48:07 AM UTC+2, Brandon Barker wrote:And for what it's worth, here is an Idris program for haha using Effects:
module Main
import Effects
import Effect.StdIO
hello : Eff () [STDIO]
hello = let ha = StdIO.putStr "ha" in ha *> ha
main : IO ()
main = run helloIt prints "ha" twice, despite being a strict language. I presume, but am not sure, this is because the effect time requires it to be re-evaluated each time.Well, the type of "hello" says that the computation will use the STDIO effect as many times as is necessary. The way the computation is constructed, it is meant to issue commands in a given sequence.One peculiarity of PureScript is that of handling effects via the algebraic effects approach. It's not easy to do in a high-performance way, because you need a call/cc construct present in the language, and moreover a 'multi-shot' one at that (i.e. the continuation *may* be invoked zero, once or more times by the effect interpreter). In ATS a simpler way is to use template functions to define effects differently (e.g. during testing and during the actual execution) -- it's constrained compared to the call/cc for sure, but then you don't have to pay the price of the call/cc plumbing. Another thing about PureScript is that it uses row types to track the set of effects that a given Eff computation may involve during its evaluation.Not that it will invalidate anything you just said, but the above code was Idris, but they may be similar in this regard (not sure). I need to look into call/cc more at some point - not very familiar with this idea. But I like where you are going with templates in ATS!
So in short, if we view the programs as creating commands, and then some kind of external interpreter that executes them, then it all matches up. The programs might be quite pure and non-side-effecting (except for non-termination aka infinite looping runtime exceptions), the interpreter will perform the effects. Here's a pseudocode for the interpreter:// the command sub-languagedatatype Command = Print of string | Nop | Seq of (command, command)externfun runCommand (c:Command): voidexternfun seq (c:Command, Command): Commandexternfun cprint (s:string): Commandimplementseq (c1, c2) = Seq (c1, c2)implementcprint (s) = Print s// the interpreter itselfimplementrunCommand (c) = case+ c of Nop => (*done!*) | Print s => print (s) | Seq (c1, c2) => (runCommand(c1); runCommand(c2))Now let's assume the Command is abstract for the rest of the program (and only the runCommand, seq and print are exposed). We can now write:val hello = let val h = cprint "hi" in seq (h, h) end // here. twice the effect!implementmain0 () = runCommand helloThe "hello" itself is free of side-effects (or so it seems to me!). We might need to lazily evaluate stuff here (e.g. to enable looping, where you need to give the interpreter the chance to run side-by-side with your expression). Or we need a more poweful "seq" (i.e. the Haskell's "bind" operator for stitching together the commands such that the left-hand side has to be evaluated to a value that is then fed to the right-hand side -- i.e. incrementally built-up as it's being evaluated by the interpeter).In Haskell, the type Command is termed "IO" (with an additional type parameter to signify the result type of the command) and the interpreter is somewhere in the runtime system.Nice to see that the basis of an interpreter can be created so easily! I guess to make it feasible to program in, in addition to the issues you just mentioned, some primitive standard library functions would need to be wrapped up as 'Command' functions just as you did with cprint; another way to do this might be to ascribe certain effect types to these primitives using e.g praxi. Functions that build on these primitives could then accumulate effects - perhaps some effects could even be consumed, but not sure. Also not sure how the interpreter would deal with some values have more than one effect type: Haskell seems to use the idea of monad transformers to get around this but I do not find it particularly satisfying so far
Still need to look into effects and how to encode different effect types - I seem to recall ATS actually had build in support for effects at the type level at some point.
Do you have or plan on having a repo to play around with this idea? If not I may try to start one (at some point).
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/73270adc-4327-470b-b900-ae20e3b36cea%40googlegroups.com.
Here is a linear version:Also, Command is a linear datatype (i.e., dataviewtype).
Nice!But I am very surprised that this code actually works.My understanding is that It works because of a bug in patsopt :)
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/fd79538d-97ac-4f54-b62d-ceeb08794036%40googlegroups.com.
>> Now, what about boxing, can we do something with boxing?Do you mean that you want to have 'a:t@ype' instead of 'a:type'?
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2367999b-fb1e-420e-b966-42c6f4aced66%40googlegroups.com.
A "standard" solution is to use call-by-reference:extern
fun
runCommand
{a:vt@ype}
(c:Command(a:vt@ype), &a? >> a): void
datavtype
Command(vt@ype) =
| Nop(unit)
| Read(string)
| Print(unit) of string
| Seq(unit) of (Command(unit), Command(unit))
| {a,b:vtype} Bind(b) of (Command(a), a?, (&a >> a?) -<cloptr1> Command(b))
This is a bit more involved but only an implementer like you (not user) needs to deal with it :)
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9ee1b434-b31e-4bca-9a24-c2a240a46172%40googlegroups.com.
Admittedly I don't really understand what RT is, but from what I understand, in Haskell the expression like [print "ha"] is basically a command to the top-level interpreter (which is the language runtime) to perform an effect on the console (moreover, it will be evaluated on as-needed basis).
I like to imagine an interpreter that sits in the Haskell's runtime. Values of IO type are commands to this interpreter. Typical Haskell IO-based programs are building up these commands as they are being evaluated by the runtime. The runtime starts evaluation at the "main" expression defined by the programmer.
newtype IO a
= IO (State# RealWorld -> (# State# RealWorld, a #))
main :: IO ()
main = putStrLn "hello"
putStrLn :: String-> IO ()
putStrLn str = IO $ \state0->
case ffi_call_to_putStrLn str of
IO next-> -- here we bind function of `ffi_call_to_putStrLn` as `next`
case next state0 of -- evaluate `next` here as it now has `s` argument
(# state1, () #) -> (# state1, () #) -- force evaluation of `next`, as this pattern match is strict
main :: IO ()
main = IO $ \state0->
case putStrLn "hello" of
IO next-> -- here we bind function of `putStrLn` as `next`
case next state0 of -- evaluate `next` here as it now has `s` argument
(# state1, () #)-> (# state1, () #) -- force evaluation of `next`, as this pattern match is strict
Moreover, the ";" is itself another comand, the explicit sequencing command, the meaning of which is "perform the left-hand side effects, then perform the right-hand side effects". Such a command is a value, so it can be passed as a value and reused as many times as is necessary. In ATS, the expression like [print "ha"] evaluates right there to a void/"no value", and the ";" is also NOT a value at all, but rather a "shortcut" syntax to a "let-in-end" form.
class Monad base where
(>>=) :: base left_type-> (left_type-> base right_type)-> base right_type
(>>) :: base left_type-> (left_type-> base right_type)-> base right_type
(>>) first second = first >>= \_ -> second
instance Monad IO where
(>>=) (IO first) second = IO $ \state0->
case first state0 of
(# state1, first_value #)->
case second first_value of
IO next->
next state1
main = do
let shortcut = putStrLn "hello"
shortcut
shortcut
main =
let shortcut = putStrLn "hello" in
shortcut >> shortcut
main = IO $ \state0->
let shortcut = putStrLn "hello" in
case (shortcut >> shortcut) state0 of
(# state1, () #)-> (# state1, () #)
So, being pure, Haskell pretends that "program is started with some unknown RealWorld state of value0 and each IO action modifies this state and thus, this value is unique for all expressions and thus. complier should evaluate them all instead of caching result of the first evaluation of `hostcut`"
```mermaidsequenceDiagramparticipant userparticipant side_panelparticipant main_windowuser->>side_panel:1 click on hidden directorygtk->>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 iteratorside_panel->>gtk:7 g_signal_emit("CHDIR")gtk->>tab_page:8 "CHDIR" signaltab_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=0tab_page->>tab_page:12 page->show_hidden=0tab_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=0side_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)```
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
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)
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
--
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-user...@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.
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 untilthe iterator is returned. For instance, the 'minus' view in PATSHOME/prelude/SATS/extern.satsis precisely introduced for this purpose.
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
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, thenthey can execute in parallel (assuming that IO1 and IO2 are disjoint). If we lump IO1 and IO2 intoIO, then parallel execution of P1 and P2 is no longer considered type-safe.
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 ()
--
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-user...@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.
One can definitely build a monad-based library to support IO:absvtype IO(a:vt@ype) = ptr
The problem with IO monad is that it is so broad. With linear types,a programmer can specify a lot more precisely.
>>is that ATS doesn't (by default?) model an IO effect.No, it doesn't if you use the default library. But nothing prevents youfrom tracking IO effects in ATS.
In the book you mentioned in your message, I was really thinking ofviews for specifying memory layouts. With linear views, a programmercan be very precise in describing what memory a function can access/update.Compared to state monads, this kind of precision is unmatched.
On Thursday, March 21, 2019 at 1:28:42 PM UTC-4, Brandon Barker wrote:
On Thursday, March 21, 2019 at 9:30:40 AM UTC-4, Brandon Barker wrote:Hi Artyom,I'm also grappling with the issue of RT in this case as I'd so far only thought about it in terms of function calls, but what you and Vanessa say helped me to understand the issue. Though I haven't managed to get ATS to have the same behavior as OCaml in the "let expression" above, I suspect it is possible. The key phrase here seems to be "side-effecting expression", and relates to the fact that functions in ATS can perform side effects without having any effect type or IO monad ascribed to the value (again, iirc).Well, maybe that isn't the real key - the real key, I now think, is that ATS doesn't (by default?) model an IO effect. In section 6.9 of http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/PDF/main.pdf it is mentioned that using both linear and dependent types may be used to do this, though I think the suggestion here is for more than printing to e.g. STDOUT.If anyone has looked at modeling/enforcing an IO-like effect type in ATS, I'd be interested to see it.
Perhaps tonight I should try out the same in Idris or PureScript, which are not lazily evaluated by default but do use IO, to get a better understanding.
On Thursday, March 21, 2019 at 3:17:46 AM UTC-4, Artyom Shalkhakov wrote:
Hi Brandon,Admittedly I don't really understand what RT is, but from what I understand, in Haskell the expression like [print "ha"] is basically a command to the top-level interpreter (which is the language runtime) to perform an effect on the console (moreover, it will be evaluated on as-needed basis). Moreover, the ";" is itself another comand, the explicit sequencing command, the meaning of which is "perform the left-hand side effects, then perform the right-hand side effects". Such a command is a value, so it can be passed as a value and reused as many times as is necessary. In ATS, the expression like [print "ha"] evaluates right there to a void/"no value", and the ";" is also NOT a value at all, but rather a "shortcut" syntax to a "let-in-end" form.
I like to imagine an interpreter that sits in the Haskell's runtime. Values of IO type are commands to this interpreter. Typical Haskell IO-based programs are building up these commands as they are being evaluated by the runtime. The runtime starts evaluation at the "main" expression defined by the programmer.
чт, 21 мар. 2019 г. в 03:45, Brandon Barker <brandon...@gmail.com>:
I'm a little rusty, so can't come up with many good examples.Apparently it is possible to do something like this in OCaml:
implement
main0 () = {
val () = let
val ha = print("ha")
in
(ha; ha) // How to get two ha's here?
end
}After running the program, you would only see one "ha", which violates RT.However, ATS doesn't seem to allow a sequence expression in the "in" position of a let expression, as this doesn't compile. Admittedly I'm just trying to see if ATS2 doesn't have RT in this particular case, but it would also be good to know about the sequence expressions here.
--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com.
--
--Cheers,
Artyom Shalkhakov
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%40googlegroups.com.
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 examples of IO splits before really digging in.
g_signal_emit( "CHDIR")
to invalidate all iterators to the tree (and moreover, to track this statically), but it doesn't even mention the tree to begin with.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.
Hi Artyom - would you mind sharing the repo URL, assuming it is open?