SML# - Resources/ProgrammingExamples/PolyC Diff

  • Added parts are displayed like this.
  • Deleted parts are displayed like this.

Many useful C library functions are polymorphic.
Properly representing them is a key to interoperability with C.

As a typical example. let us consider a commonly used C library
function '''FREAD(3)''.
According to the manual, its type is defined as follows:
  #include <stdio.h>
  size_t  fread(void  *ptr,
                size_t size,
                size_t nmemb,
                FILE *stream);
The meanings of its arguments are:
* void  *ptr : a pointer to an array to which the input data are stored.
* size_t size : the size of each input data element
* size_t nmemb : the maximal number of elements´╝Ä
* FILE *stream : input stream
Using the size of element type, this function can
reads input stream of
various types and store them to an array of the corresponding type quite efficiently by advancing the array element pointer.
This function is ''polymorphic'' in the type of data elements.
As a statically typed polymorphic language, ML should treat this as a
function of the following type:
fread : 'a array * int * stdIn -> int
where
* 'a array : an array to which the input data are stored
* int : the maximal number of data elements´╝Ä
* stdIn : input stream
The size argument required by the original C function should be
computed and inserted by the compiler.

This is indeed possible in SML#.
Based on the polymorphic record compilation theory, SML#
compiler is capable of computing the size of each data type,
passing the necessary size information to polymorphic functions.
SML# system makes a part of this mechanism available to the programmer
that write C FFI interface for type safe linking of polymorphic C
functions.

FREAD can be used by the following declaration.
  type c_file = unit ptr
  val libc = DynamicLink.dlopen "/lib/libc.so.6"
  val c_fread = DynamicLink.dlsym (libc, "fread")
  fun fread (dst, len, file) =
      _ffiapply c_fread (dst : 'a array,
                         _sizeof('a),
                         len : int,
                         file : c_file)
                 : int
The body of '''fread''' is the SML# special form having the following syntax:
_ffiapply e (arg1,...,argn) : t
Each argument '''agri''' is either of the form
  exp : t
  _sizeof(t)
The former is an ordinary expression and its type to be passed to the
C function.
The latter is the reference to the size information SML# compiler
maintain.
This term is automatically replaced with the term denoting the size of
the type and passed to the C function.
Conceptually, this construct allows the programmer to write the result
of the type directed compilation.

The above declaration yields the following binding.
val fread = fn : ['a .'a Array.array * int * unit ptr  -> int]
After this, '''fread''' can be used as a polymoprhic function of this
type. Its behavior is to call the raw C function that perform binary IO
and direct data transfer to the specified array in the SML# heap.

By declaring '''fopen''', '''fclose''', '''fwrite''' etc, one can use
efficient C binary IO from SML# in a type safe manner.