Hi Artyom - would you mind sharing the repo URL, assuming it is open? 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/a1c65047-34a2-4484-8738-5a9b19e31a99%40googlegroups.com.
