<div dir="ltr"><div><div>Wouldn't that be inefficient? A Nat would need to be divided by 256 , then we need to take the remainder Nat and transform it into an Integer.<br></div>Wouldn't that last step require us to recursively add +1 to the integer?<br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 25, 2018 at 1:28 PM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I think the simplest approach would be to add a binding to a Haskell function taking a list of Integers (which is how natural numbers are represented) and storing them (mod 256) in a byte string. Then you can do all the encoding on the Agda side and there's no need for any new primitives or worry over how builtin types are represented.<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888">/ Ulf<br></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 25, 2018 at 11:38 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@<wbr>gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>I could use haskell' Binary library, but that would require me to know the haskell type of the builtin types.<br><br></div>The other option is that Agda has primitive functions that make the transformation, this way I do not need to know how builtin types are represented in Haskell.<br><br></div>The other option is to define my my own pragmas for the builtin types. I do not want to do that because the builtin representation was done for a reason.<br><br></div>I would prefer the second option. To add primitive functions that make the transformation.<br></div><div class="m_-6182819955835919347HOEnZb"><div class="m_-6182819955835919347h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 25, 2018 at 12:12 PM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Philipp added the Bytes type in <a href="https://github.com/UlfNorell/agda-prelude/commit/6214370064f14b" target="_blank">https://github.com/UlfNorell/a<wbr>gda-prelude/commit/6214370064f<wbr>14b</a> to do binary IO, but it doesn't look like he added any functions to create them other than reading from file.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="m_-6182819955835919347m_9157390154871439658h5">On Sun, Feb 25, 2018 at 10:55 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_-6182819955835919347m_9157390154871439658h5"><div dir="ltr"><div><div><div><div>There is a Bytes Type in agda-prelude, <br><a href="https://github.com/UlfNorell/agda-prelude/blob/2e3addb9a434ed121805fa571f1dd0a077076a29/src/Prelude/Bytes.agda" target="_blank">https://github.com/UlfNorell/a<wbr>gda-prelude/blob/2e3addb9a434e<wbr>d121805fa571f1dd0a077076a29/sr<wbr>c/Prelude/Bytes.agda<br></a><br></div>but there is no defined way to encode/decode a builtin type to/from Bytes.<br></div></div></div>Is there a way to perform the serialization with the builtin types or do I have to define my own pragmas?<br></div>
<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>