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 <javascript:>> > 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 <javascript:>. >> To post to this group, send email to ats-lan...@googlegroups.com >> <javascript:>. >> 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/274cb026-c389-4846-9c8b-8719a3ada381%40googlegroups.com.
