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

**URL:** <https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852>\
**Category:** Google Group\
**Created:** [April 16, 2015, 11:52am UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852 "2015-04-16T11:52:47Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 11:52am UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/1 "2015-04-16T11:52:47Z")

</div>

Hi all,

In version 1.1.0.0 of my file descriptor library, I introduced a view for  
partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
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

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 17, 2015, 1:58am UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/2 "2015-04-17T01:58:42Z")

</div>

OK, fair enough. Thanks!\> On Apr 16, 2015, at 5:04 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> 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](https://github.com/githwxi/ATS-Postiats/tree/master/utils/atspkgreloc)
> 
> On Thursday, April 16, 2015 at 4:06:02 PM UTC-4, Shea Levy wrote:  
> 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?
> 
> On Apr 16, 2015, at 15:39, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > 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.
> > 
> > On Thursday, April 16, 2015 at 2:48:46 PM UTC-4, Shea Levy wrote:  
> > 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
> > 
> > > On Apr 16, 2015, at 10:51 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<\>\> wrote:
> > > 
> > > 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#”
> > > 
> > > On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> > > 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46) [https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46](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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58) [https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58)
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com) \<\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users) [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%40googlegroups.com) [https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com) \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users) [http://groups.google.com/group/ats-lang-users](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/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com) [https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%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-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com) [mailto:ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com) [mailto:ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users) [http://groups.google.com/group/ats-lang-users](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/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com) [https://groups.google.com/d/msgid/ats-lang-users/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com?utm_medium=email&utm_source=footer).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 16, 2015, 9:04pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/3 "2015-04-16T21:04:59Z")

</div>

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/atspkgrelocOn](https://github.com/githwxi/ATS-Postiats/tree/master/utils/atspkgrelocOn) Thursday, April 16, 2015 at 4:06:02 PM UTC-4, Shea Levy wrote:

> 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?
> 
> On Apr 16, 2015, at 15:39, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> 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.
> 
> On Thursday, April 16, 2015 at 2:48:46 PM UTC-4, Shea Levy wrote:
> 
> > 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
> > 
> > > On Apr 16, 2015, at 10:51 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > > 
> > > 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#”
> > > 
> > > On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> > > Hi all,
> > > 
> > > In version 1.1.0.0 of my file descriptor library, I introduced a view  
> > > for  
> > > partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> > > 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
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com).  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com)  
> > [https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 16, 2015, 7:39pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/4 "2015-04-16T19:39:02Z")

</div>

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.On Thursday, April 16, 2015 at 2:48:46 PM UTC-4, Shea Levy wrote:

> 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
> 
> > On Apr 16, 2015, at 10:51 AM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> > 
> > 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#”
> > 
> > On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> > Hi all,
> > 
> > In version 1.1.0.0 of my file descriptor library, I introduced a view  
> > for  
> > partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> > 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
> > 
> > –  
> > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 16, 2015, 2:51pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/5 "2015-04-16T14:51:32Z")

</div>

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#"On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:

> Hi all,
> 
> In version 1.1.0.0 of my file descriptor library, I introduced a view for  
> partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> 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

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 18, 2015, 12:39pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/6 "2015-04-18T12:39:51Z")

</div>

By the way, based on this discussion version 1.2.0.0 of my file descriptor  
library added some view-changing functions [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46) 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.1.0.0/include/elvysh/filedes.sats#L26-L46): [https://github.com/shlevy/elvysh-filedes/blob/v1.2.0.0/include/elvysh/partially-initialized-array.sats#L23-L71](https://github.com/shlevy/elvysh-filedes/blob/v1.2.0.0/include/elvysh/partially-initialized-array.sats#L23-L71)\> On Apr 16, 2015, at 9:58 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> OK, fair enough. Thanks!
> 
> > On Apr 16, 2015, at 5:04 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > 
> > 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](https://github.com/githwxi/ATS-Postiats/tree/master/utils/atspkgreloc)
> > 
> > On Thursday, April 16, 2015 at 4:06:02 PM UTC-4, Shea Levy wrote:  
> > 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?
> > 
> > On Apr 16, 2015, at 15:39, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > 
> > > 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.
> > > 
> > > On Thursday, April 16, 2015 at 2:48:46 PM UTC-4, Shea Levy wrote:  
> > > 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
> > > 
> > > > On Apr 16, 2015, at 10:51 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > > > 
> > > > 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#”
> > > > 
> > > > On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> > > > Hi all,
> > > > 
> > > > In version 1.1.0.0 of my file descriptor library, I introduced a view for  
> > > > partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> > > > 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
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com).  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%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...@googlegroups.com](mailto:ats-lang...@googlegroups.com).  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/537977b8-637e-4e7d-8f9b-c9811f3d715e%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/537977b8-637e-4e7d-8f9b-c9811f3d715e%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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/EDBF81EF-5F7C-4804-A98A-2488CB5A3900%40shealevy.com](https://groups.google.com/d/msgid/ats-lang-users/EDBF81EF-5F7C-4804-A98A-2488CB5A3900%40shealevy.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 6:48pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/7 "2015-04-16T18:48:44Z")

</div>

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\> On Apr 16, 2015, at 10:51 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> 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#”
> 
> On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> Hi all,
> 
> In version 1.1.0.0 of my file descriptor library, I introduced a view for  
> partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> 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
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 8:01pm UTC](https://discourse.ats-lang.org/t/adding-a-view-for-partially-initialized-arrays-to-the-prelude-libats/852/8 "2015-04-16T20:01:44Z")

</div>

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?\> On Apr 16, 2015, at 15:39, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> 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.
> 
> On Thursday, April 16, 2015 at 2:48:46 PM UTC-4, Shea Levy wrote:
> 
> > 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
> > 
> > > On Apr 16, 2015, at 10:51 AM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > > 
> > > 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#”
> > > 
> > > On Thursday, April 16, 2015 at 7:52:50 AM UTC-4, Shea Levy wrote:  
> > > Hi all,
> > > 
> > > In version 1.1.0.0 of my file descriptor library, I introduced a view for  
> > > partially initialized arrays [1](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L26-L46), 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](https://github.com/shlevy/elvysh-filedes/blob/v1.1.0.0/include/elvysh/filedes.sats#L57-L58),  
> > > 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
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com).  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/edd706ea-8cba-4b64-88d8-c39b23f41e83%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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/55da5425-5385-4345-a388-e69004c04c72%40googlegroups.com).