On Sunday, August 18, 2019 at 7:10:26 AM UTC+3, Brandon Barker wrote: > > Hi Artyom - would you mind sharing the repo URL, assuming it is open? > > Well, here it is:
https://github.com/ashalkhakov/libatsc > On Thursday, August 8, 2019 at 2:49:43 AM UTC-4, Artyom Shalkhakov wrote: >> >> Hi Brandon, Alexander, >> >> On Wednesday, August 7, 2019 at 5:31:04 AM UTC+3, Brandon Barker wrote: >> >>> 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. >>> >> >> I'm writing such a library in my spare time, but I find that HX did most >> of the work back in ATS0/ATS1 days. >> >> Getting back to the problem Alexander mentioned, we could try using >> fractional permissions. I'll take an array as an example. >> >> We could still try to use fractional permissions (similarly to what is >> described here >> <http://www.cs.uwm.edu/faculty/boyland/papers/iterators.pdf>, PDF) >> >> - a collection gets one more type index, k:int (k >= 0) >> - k stands for fraction 2^(-k) (e.g. k=0 is 1, k=1 is 1/2, etc.) >> >> Let's make a fractional dynamically-resizeable array: >> >> absview farray_v(a:vtflt, l:addr, n:int, k:int) >> >> Examples: >> >> farray_v(a,l,n,0) <- whole permission to array, allows writing! >> farray_v(a,l,n,k) <- k > 0, this is a read-only permission, can't reassign >> >> Basically, it's OK to *split* the view in half. >> >> praxi split : {a:vtflt}{l:addr}{n:int}{k:nat} farray_v(a,l,n,k) -> >> (farray_v(a,l,n,k+1), farray_v(a,l,n,k+1)) >> praxi unsplit : {a:vtflt}{l:addr}{n:int}{k:pos} (farray_v(a,l,n,k), >> farray_v(a,l,n,k)) -> farray_v(a,l,n,k-1) >> >> Allocation and deallocation only deal with the whole permission: >> >> fun{a:tflt} >> farray_free {l:addr;n:int} (farray_v(a,l,n,0) | ptr l): void >> fun{a:vtflt} >> farray_alloc (capacity: int): [l:addr] (farray_v(a,l,0,0) | ptr l) >> >> Now we can imagine that some array operations are destructive, so we >> require k=0 for the view, but the read-only operations can be used with any >> k. >> >> fun{a:tflt} >> farray_get_at {l:addr;n:int;k:int;i:nat | i < n} (!farray_v(a,l,n,k) | >> ptr l, int i): a >> fun{a:vtflt} >> farray_insert_before {l:addr;n:int;k:int;i:nat | i <= n} >> (!farray_v(a,l,n,0) >> farray_v(a,l,n+1,0) | ptr l, int i, a): void >> >> Basically: >> >> - destructive operations can only be called if you have the whole >> permission (i.e. k=0) >> - destructive operations are: insert, append, prepend, delete >> >> However, if we are to give safe types to C++-style iterators, we'd still >> need lots more precision... It isn't enough to have an farray(a,n), you >> have to ensure that the iterator is from *this* array not *that* array. >> This will be very painful to work with. I'll sketch out an iterator API >> below. >> >> // basically a pointer to array element (but may point past the end of >> array: this is the "end" iterator) >> absvtbox >> fiter (a:vtflt,l:addr,k:int,b:bool) // b=true: this is the end iterator, >> i.e. it can't be read from/written to >> >> // simple pointer equality >> fun >> eq_fiter {a:vtflt}{l:addr}{k1,k2:int} (!fiter(a,l,k1,b1), >> !fiter(a,l,k2,b2)): bool (b1 == b2) >> >> // taking pointers out >> fun{a:vtflt} >> farray_begin {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> >> farray_v(a,l,n,k+1) | ptr l): [b:bool] fiter(a,l,k+1,b) >> fun{a:vtflt} >> farray_end {l:addr}{n:int}{k:int} (!farray_v(a,l,n,k) >> >> farray_v(a,l,n,k+1) | ptr l): fiter(a,l,k+1,true) >> >> // putting pointers back >> prfun >> fiter_putback {a:vtflt}{l:addr}{n:int}{k:pos}{b:bool} (!farray_v(a,l,n,k) >> >> farray_v(a,l,n,k-1), fiter(a,l,k,b)): void >> >> fun{a:vtflt} >> fiter_succ {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b) >> fun{a:vtflt} >> fiter_pred {l:addr}{k:int} (fiter(a,l,k,b)): fiter(a,l,k,b) >> fun{a:tflt} >> fiter_get {l:addr}{k:int} (!fiter(a,l,k,false)): a >> fun{a:tflt} >> fiter_set {l:addr}{k:int} (!fiter(a,l,k,false), a): void >> >> For trees, it's going to be pretty similar, I think: if you have parent >> links in this tree, then an iterator is again simply a pointer, and the >> "end" iterator is the NULL pointer (so again pretty simple to check). >> >> Oh my, this above doesn't directly address the question, sorry! If there >> was some way for 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. >> >> >>> On Thu, Mar 21, 2019, 8:18 PM gmhwxi <gmh...@gmail.com> wrote: >>> >>>> >>>> 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 you >>>> from tracking IO effects in ATS. >>>> >>>> In the book you mentioned in your message, I was really thinking of >>>> views for specifying memory layouts. With linear views, a programmer >>>> can 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 >>>>>>>> >>>>>>>> <https://groups.google.com/d/msgid/ats-lang-users/5eba6b86-4146-4ba2-a87f-f8c511d902f0%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>>>>> . >>>>>>>> >>>>>>> >>>>>>> >>>>>>> -- >>>>>>> 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-lan...@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 >>>> >>>> <https://groups.google.com/d/msgid/ats-lang-users/3d13aac1-2f28-47af-afbd-6d9eced901db%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/4f0608cf-1e3d-402e-8544-68893888db0b%40googlegroups.com.
