<div dir="ltr"><div>I'm not quite following, but sure, if you want high performance you should bind against the Haskell binary library (your first option). FFI bindings are type checked so you don't have to worry about mistaking the representation of a builtin type.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 25, 2018 at 4:57 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@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>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="HOEnZb"><div class="h5"><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="m_-7987373631047977948HOEnZb"><font color="#888888"><br><br></font></span></div><span class="m_-7987373631047977948HOEnZb"><font color="#888888">/ Ulf<br></font></span></div><div class="m_-7987373631047977948HOEnZb"><div class="m_-7987373631047977948h5"><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@gma<wbr>il.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_-7987373631047977948m_-6182819955835919347HOEnZb"><div class="m_-7987373631047977948m_-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_-7987373631047977948m_-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_-7987373631047977948m_-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>
</div></div></blockquote></div><br></div>