Discussion:
Serialization to ByteString
(too old to reply)
Apostolis Xekoukoulotakis
2018-02-25 09:55:56 UTC
Permalink
Raw Message
There is a Bytes Type in agda-prelude,
https://github.com/UlfNorell/agda-prelude/blob/2e3addb9a434ed121805fa571f1dd0a077076a29/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?
Ulf Norell
2018-02-25 10:12:26 UTC
Permalink
Raw Message
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 <
Post by Apostolis Xekoukoulotakis
There is a Bytes Type in agda-prelude,
https://github.com/UlfNorell/agda-prelude/blob/
2e3addb9a434ed121805fa571f1dd0a077076a29/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
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-02-25 10:38:18 UTC
Permalink
Raw Message
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.
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 <
Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell
2018-02-25 11:28:29 UTC
Permalink
Raw Message
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 <
Post by 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.
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 <
Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-02-25 15:57:21 UTC
Permalink
Raw Message
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?
Post by 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 <
Post by 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.
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 <
Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell
2018-02-25 16:20:37 UTC
Permalink
Raw Message
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 <
Post by 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?
Post by 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 <
Post by 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.
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 <
Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-02-25 17:04:45 UTC
Permalink
Raw Message
Thanks, I will do that.
Post by 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 <
Post by 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?
Post by 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 <
Post by 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.
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 <
Post by Apostolis Xekoukoulotakis
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
https://lists.chalmers.se/mailman/listinfo/agda
Loading...