[Agda] Serialization to ByteString

[Ulf Norell]

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.

/ Ulf

On Sun, Feb 25, 2018 at 4:57 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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/d7bbe495/attachment-0001.html>