# Converting an int to a byte?

**URL:** <https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834>\
**Category:** Google Group\
**Created:** [February 13, 2015, 11:52am UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834 "2015-02-13T11:52:12Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![Artyom\_Shalkhakov](https://avatars.discourse-cdn.com/v4/letter/a/6bbea6/32.png) [@Artyom\_Shalkhakov](https://discourse.ats-lang.org/u/Artyom_Shalkhakov)\
**Post date:** [February 13, 2015, 11:52am UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/1 "2015-02-13T11:52:12Z")

</div>

Here goes a simple question: I need a function to convert an int to a byte.

Either I’m not searching hard enough, or there is no such function in the  
prelude. Which is it?

---

<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:** [February 16, 2015, 3:45pm UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/2 "2015-02-16T15:45:33Z")

</div>

> 

> > I added several casting functions for bytes. See the end of the following  
> > file:
> > 
> > [http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char\_sats.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html)
> > 
> > The type byte is treated in ATS as a completely opaque type whose size  
> > equals that of a char.
> 
> Is there a praxi or prfun somewhere that indicates that sizeof(byte) ==  
> sizeof(char)?

I added some lemmas in char.sats. For instance,

praxi  
lemma\_char\_size () : [sizeof(char)==sizeof(byte)] void

However, the names of these lemmas are difficult to remember. So be  
“programmer-centric” 🙂

prval () = $UN.prop\_assert{sizeof(char)==sizeof(byte)}()

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [February 13, 2015, 1:36pm UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/3 "2015-02-13T13:36:03Z")

</div>

My guess is that there may not be such a function, other than $UN.cast. But  
I hardly know for sure. I feel like this was talked about recently: does  
int size still vary from platform to platform according to the C standard?  
But in ATS you can specify the size of the int if you really need to, so I  
guess it isn’t an issue if you go this route.On Fri, Feb 13, 2015 at 6:52 AM, Artyom Shalkhakov \< [artyom.s...@gmail.com](mailto:artyom.s...@gmail.com)\> wrote:

> Here goes a simple question: I need a function to convert an int to a byte.
> 
> Either I’m not searching hard enough, or there is no such function in the  
> prelude. Which is it?
> 
> –  
> 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/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

Brandon Barker  
[brandon...@gmail.com](mailto:brandon...@gmail.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:** [February 13, 2015, 4:43pm UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/4 "2015-02-13T16:43:30Z")

</div>

I added several casting functions for bytes. See the end of the following  
file:

[http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char\_sats.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html)

The type byte is treated in ATS as a completely opaque type whose size  
equals that of a char.

If you want to manipulate/modify bytes, try to use types like int8 and  
uint8.On Friday, February 13, 2015 at 6:52:12 AM UTC-5, Artyom Shalkhakov wrote:

> Here goes a simple question: I need a function to convert an int to a byte.
> 
> Either I’m not searching hard enough, or there is no such function in the  
> prelude. Which is it?

---

<div class="post-metadata">

**Author:** ![Artyom\_Shalkhakov](https://avatars.discourse-cdn.com/v4/letter/a/6bbea6/32.png) [@Artyom\_Shalkhakov](https://discourse.ats-lang.org/u/Artyom_Shalkhakov)\
**Post date:** [February 16, 2015, 8:11am UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/5 "2015-02-16T08:11:21Z")

</div>

> I added several casting functions for bytes. See the end of the following  
> file:
> 
> [http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char\_sats.html](http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html)
> 
> The type byte is treated in ATS as a completely opaque type whose size  
> equals that of a char.

Is there a praxi or prfun somewhere that indicates that sizeof(byte) ==  
sizeof(char)?

> If you want to manipulate/modify bytes, try to use types like int8 and  
> uint8.

Thanks! I switched to uint8 + unsafe casts for now.\> On Friday, February 13, 2015 at 6:52:12 AM UTC-5, Artyom Shalkhakov wrote:

> > Here goes a simple question: I need a function to convert an int to a  
> > byte.
> > 
> > Either I’m not searching hard enough, or there is no such function in the  
> > prelude. Which is it?

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [February 13, 2015, 1:40pm UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/6 "2015-02-13T13:40:23Z")

</div>

Actually, $UN.cast may not be the exact function you want since I guess  
byte will have some views that need to be constructed, but something in $UN  
would hopefully work.On Fri, Feb 13, 2015 at 8:36 AM, Brandon Barker [brandon...@gmail.com](mailto:brandon...@gmail.com) wrote:

> My guess is that there may not be such a function, other than $UN.cast.  
> But I hardly know for sure. I feel like this was talked about recently:  
> does int size still vary from platform to platform according to the C  
> standard? But in ATS you can specify the size of the int if you really need  
> to, so I guess it isn’t an issue if you go this route.
> 
> On Fri, Feb 13, 2015 at 6:52 AM, Artyom Shalkhakov \< [artyom.s...@gmail.com](mailto:artyom.s...@gmail.com)\> wrote:
> 
> > Here goes a simple question: I need a function to convert an int to a  
> > byte.
> > 
> > Either I’m not searching hard enough, or there is no such function in the  
> > prelude. Which is it?
> > 
> > –  
> > 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/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com)  
> > [https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .
> 
> –  
> Brandon Barker  
> [brandon...@gmail.com](mailto:brandon...@gmail.com)

Brandon Barker  
[brandon...@gmail.com](mailto:brandon...@gmail.com)

---

<div class="post-metadata">

**Author:** ![Artyom\_Shalkhakov](https://avatars.discourse-cdn.com/v4/letter/a/6bbea6/32.png) [@Artyom\_Shalkhakov](https://discourse.ats-lang.org/u/Artyom_Shalkhakov)\
**Post date:** [February 13, 2015, 1:56pm UTC](https://discourse.ats-lang.org/t/converting-an-int-to-a-byte/834/7 "2015-02-13T13:56:36Z")

</div>

> Actually, $UN.cast may not be the exact function you want since I guess  
> byte will have some views that need to be constructed, but something in $UN  
> would hopefully work.

Well, I could always implement it in C. I guess that it would be quite  
useful to have it included in the prelude, though.