[Agda] Serialization to ByteString

[Apostolis Xekoukoulotakis]

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.
Wouldn't that last step require us to recursively add +1 to the integer?


On Sun, Feb 25, 2018 at 1:28 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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.
>
> / Ulf
>
> On Sun, Feb 25, 2018 at 11:38 AM, Apostolis Xekoukoulotakis <
> apostolis.xekoukoulotakis at gmail.com> wrote:
>
>> I could use haskell' Binary library, but that would require me to know
>> the haskell type of the builtin types.
>>
>> 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.
>>
>> 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.
>>
>> I would prefer the second option. To add primitive functions that make
>> the transformation.
>>
>> On Sun, Feb 25, 2018 at 12:12 PM, Ulf Norell <ulf.norell at gmail.com>
>> wrote:
>>
>>> Philipp added the Bytes type in https://github.com/UlfNorell/a
>>> gda-prelude/commit/6214370064f14b to do binary IO, but it doesn't look
>>> like he added any functions to create them other than reading from file.
>>>
>>> / Ulf
>>>
>>> On Sun, Feb 25, 2018 at 10:55 AM, Apostolis Xekoukoulotakis <
>>> apostolis.xekoukoulotakis at gmail.com> wrote:
>>>
>>>> There is a Bytes Type in agda-prelude,
>>>> https://github.com/UlfNorell/agda-prelude/blob/2e3addb9a434e
>>>> d121805fa571f1dd0a077076a29/src/Prelude/Bytes.agda
>>>>
>>>> but there is no defined way to encode/decode a builtin type to/from
>>>> Bytes.
>>>> Is there a way to perform the serialization with the builtin types or
>>>> do I have to define my own pragmas?
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180225/0bb4aefb/attachment.html>