[Agda] Serialization to ByteString

[Ulf Norell]

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/0c9c95fa/attachment.html>