[polyml] [RFC]: Modules to support C FFIs -- a proposal and a minor patch

[Domagoj Stolfa]

Hi all:


I've only been using Poly for a few days and haven't done too much SML
before a project I'm working on now -- but I've noticed a couple of
things that seemed a little tedious while implementing some modules as a
part of that project. I may have missed something, and if that's the
case please do point it out to me. However, in case what I've observed
is in fact the current state of the world, I've written a small proposal
and a patch to eliminate these little annoyances (suggested to me by
DGASAU on freenode).


In essence, I've been building an FFI in the past few days and noticed
an absence of a number of things. Namely, there seems to be a lack of
support for standard C types such as uint16_t, int16_t, int8_t, int64_t
and float (not sure about int64_t). This can make building FFIs a bit of
a hassle sometimes, as it requires explicit checks of what value the
integer/word in SML might contain before deciding to try and write it.


An example of such a workaround would be:

        if (#NOFFS a) > 0w65535 orelse (#NENOFFS a) > 0w65535
        then raise RunCall.Conversion "Invalid Word16 constant"
        else (...)

where #NOFFS a and #NENOFFS a are otherwise manipulated as Word32.words.


Moreover, this seems to sometimes cause people developing software or
extracting executable specifications from proof assistants such as
Isabelle that depend on things like Word16 to discard or impose a
limitation on SML used with PolyML as it simply does not support these
types out of the box [1, 2]


Would it make sense to support these types in PolyML, namely through
Word16.word, Int16.int, Int8.int and Int64.int, where Word16 would be of
WORD signature, while Int16, Int8 and Int64 would be of INTEGER signature.


I've attached a sample patch for supporting Word16, very heavily based
on David Matthews' work on Word8 in order to demonstrate what a very
crude implementation of the proposal would look like.


Is this a real problem, and if so, is implementing these things a
sensible way forward?


Thanks!


[1]: http://rohandrape.net/?t=smlsc3&e=README

[2]:
https://www.isa-afp.org/browser_info/current/AFP/Native_Word/outline.pdf

[David Matthews]

Hi,
Thank you for your comments and the patch. Apologies for the delay in
replying; I wanted to give it some thought.

I'm not convinced that adding Int16 etc would help that much with FFI
calls. Currently the code checks that the values are in range when the
foreign function is called. Using an appropriate fixed precision
integer type would essentially move the range checks elsewhere. There
might be some other uses for Int16 etc. I'll consider adding your
Word16 code.

Real32 (i.e. float) might be useful on X86/64 because it could be
implemented using tagging rather than needing real numbers to be stored
in heap cells. Currently the need to allocate memory to hold a "real"
is a significant overhead.

Regards,
David

Post by Domagoj Stolfa
I've only been using Poly for a few days and haven't done too much SML
before a project I'm working on now -- but I've noticed a couple of
things that seemed a little tedious while implementing some modules as a
part of that project. I may have missed something, and if that's the
case please do point it out to me. However, in case what I've observed
is in fact the current state of the world, I've written a small proposal
and a patch to eliminate these little annoyances (suggested to me by
DGASAU on freenode).
In essence, I've been building an FFI in the past few days and noticed
an absence of a number of things. Namely, there seems to be a lack of
support for standard C types such as uint16_t, int16_t, int8_t, int64_t
and float (not sure about int64_t). This can make building FFIs a bit of
a hassle sometimes, as it requires explicit checks of what value the
integer/word in SML might contain before deciding to try and write it.
        if (#NOFFS a) > 0w65535 orelse (#NENOFFS a) > 0w65535
        then raise RunCall.Conversion "Invalid Word16 constant"
        else (...)
where #NOFFS a and #NENOFFS a are otherwise manipulated as Word32.words.
Moreover, this seems to sometimes cause people developing software or
extracting executable specifications from proof assistants such as
Isabelle that depend on things like Word16 to discard or impose a
limitation on SML used with PolyML as it simply does not support these
types out of the box [1, 2]
Would it make sense to support these types in PolyML, namely through
Word16.word, Int16.int, Int8.int and Int64.int, where Word16 would be of
WORD signature, while Int16, Int8 and Int64 would be of INTEGER signature.
I've attached a sample patch for supporting Word16, very heavily based
on David Matthews' work on Word8 in order to demonstrate what a very
crude implementation of the proposal would look like.
Is this a real problem, and if so, is implementing these things a
sensible way forward?
Thanks!
[1]: http://rohandrape.net/?t=smlsc3&e=README
https://www.isa-afp.org/browser_info/current/AFP/Native_Word/outline.pdf
_______________________________________________
polyml mailing list
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[Domagoj Stolfa]

Hi David:

Thanks for the reply & review. That's a fair point regarding FFI and Int16. I do think Real32 could be useful, and I'm willing to take a look at a potential implementation when I get time (it's a bit hectic right now :-().

As for Word16, if you find something you dislike in the code while considering adding it into Poly, I'm happy to adjust it :-).

—
Domagoj

Hi,
Thank you for your comments and the patch. Apologies for the delay in replying; I wanted to give it some thought.
I'm not convinced that adding Int16 etc would help that much with FFI calls. Currently the code checks that the values are in range when the foreign function is called. Using an appropriate fixed precision integer type would essentially move the range checks elsewhere. There might be some other uses for Int16 etc. I'll consider adding your Word16 code.
Real32 (i.e. float) might be useful on X86/64 because it could be implemented using tagging rather than needing real numbers to be stored in heap cells. Currently the need to allocate memory to hold a "real" is a significant overhead.
Regards,
David

I've only been using Poly for a few days and haven't done too much SML before a project I'm working on now -- but I've noticed a couple of things that seemed a little tedious while implementing some modules as a part of that project. I may have missed something, and if that's the case please do point it out to me. However, in case what I've observed is in fact the current state of the world, I've written a small proposal and a patch to eliminate these little annoyances (suggested to me by DGASAU on freenode).
In essence, I've been building an FFI in the past few days and noticed an absence of a number of things. Namely, there seems to be a lack of support for standard C types such as uint16_t, int16_t, int8_t, int64_t and float (not sure about int64_t). This can make building FFIs a bit of a hassle sometimes, as it requires explicit checks of what value the integer/word in SML might contain before deciding to try and write it.
if (#NOFFS a) > 0w65535 orelse (#NENOFFS a) > 0w65535
then raise RunCall.Conversion "Invalid Word16 constant"
else (...)
where #NOFFS a and #NENOFFS a are otherwise manipulated as Word32.words.
Moreover, this seems to sometimes cause people developing software or extracting executable specifications from proof assistants such as Isabelle that depend on things like Word16 to discard or impose a limitation on SML used with PolyML as it simply does not support these types out of the box [1, 2]
Would it make sense to support these types in PolyML, namely through Word16.word, Int16.int, Int8.int and Int64.int, where Word16 would be of WORD signature, while Int16, Int8 and Int64 would be of INTEGER signature.
I've attached a sample patch for supporting Word16, very heavily based on David Matthews' work on Word8 in order to demonstrate what a very crude implementation of the proposal would look like.
Is this a real problem, and if so, is implementing these things a sensible way forward?
Thanks!
[1]: http://rohandrape.net/?t=smlsc3&e=README
[2]: https://www.isa-afp.org/browser_info/current/AFP/Native_Word/outline.pdf
_______________________________________________
polyml mailing list
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

_______________________________________________
polyml mailing list
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml