[Agda] Serialization to ByteString

[Apostolis Xekoukoulotakis]

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/
> agda-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/18e93a51/attachment.html>