Adding a view for partially initialized arrays to the prelude/libats?

[Shea Levy]

Hi all,

In version 1.1.0.0 of my file descriptor library, I introduced a view for
partially initialized arrays [1], which allows me to cleanly represent a
contiguous array that may have some elements initialized but may not have all
elements initialized. This is used in the type of the POSIX read function [2],
which may increase (but not decrease) the number of initialized values in the
array.

It seems like this is a generally useful concept applicable outside of this
library, so I was wondering: Would this be welcome in the prelude or in libats?
If so, where does it best fit?

Thanks,
Shea

[1]: https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46
[2]: https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58

[gmhwxi]

Personally, I feel max(fill, res) in the following interface for read
is problematic:

If you call 'read', the buffer gets overwritten. Logically, there isn't
obvious justification for combining old buffer content and new buffer
content in this way.

fn read { fd: nat } { buf: addr } { fill, total: nat | fill <= total }

( ev: !errno_v ( free ) >> neg1_errno ( res )

, fdprf: !readable_filedes ( fd )

, !partially_initialized_array_v ( byte, fill, total, buf ) >>

partially_initialized_array_v ( byte, max ( fill, res ), total, buf )

| fd: int ( fd )

, buf: ptr buf

, total: size_t total

): #[ res: int ] ssize_t ( res ) = "ext#"

[Shea Levy]

The way I look at it, read is a very generic function whose semantics support a
wide array of use cases. Using partially_initialized_array reflects the full
generality of those semantics. Surely no one would dispute that if I want the
behavior of any old bytes remaining initialized, that behavior is indeed
guaranteed by the standard and all implementations?

One particular possible use case that comes to mind: Perhaps I store some
default value in my buffer, and then allow it to be overridden by something I
read from a file descriptor. Then if read returns 0 or -1, my buffer is still
ready to go to use however I wanted.

~Shea

> --
> 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 http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%40googlegroups.com.

[gmhwxi]

As I see it, the question is not whether we can find a scenario where
the type is actually useful. It is a trade-off. In generally, the more informative
a type is, the more effort is needed to actually use it.

[Shea Levy]

Actually, without partially_initialized_array I'm not sure how to write the type signature of read at all. I need to know how many bytes are initialized after the call, don't I?

Or is your objection just to the presence of max? In that case, the array view itself can still go into the standard library, right?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com.

[gmhwxi]

I can see some value of having partially_initialized_array_v.
However, in order to use it, I must know it first. I could be wrong, but
I don't feel it is realistic to expect a programmer to learn the names of
such "secondary" concepts.

Also, I feel that contributions made to ATS should in general be done in
a distributed manner (vs. centralized manner).

The 'atspkgreloc' command allows on-line ATS packages to be directly
referred in one's program. See:

https://github.com/githwxi/ATS-Postiats/tree/master/utils/atspkgreloc

[Shea Levy]

OK, fair enough. Thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com.

[Shea Levy]

By the way, based on this discussion version 1.2.0.0 of my file descriptor
library added some view-changing functions [1] for collapsing a max constraint
in a partially initialized array to the older or newer value. Most of the time
partially_initialized_array_unmax_after will be used, which takes the value
returned by read and ignores however many values were initialized beforehand.

~Shea

[1]: https://github.com/shlevy/elvysh-filedes/blob/v1.2.0.0/include/elvysh/partially-initialized-array.sats#L23-L71

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/EDBF81EF-5F7C-4804-A98A-2488CB5A3900%40shealevy.com.