[Agda] Serialization to ByteString

[Apostolis Xekoukoulotakis]

Thanks, I will do that.

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

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