Type Isomorphism for Flexible Data Transport between Clients and Servers

This is a multifaceted problem with many existing approaches. An excellent survey of the current state of the art is given by Wileden, et al  [#!WWRT-CACM91!#]. Most current systems support what one might call data structure isomorphism (DSI) which is used in data transport among components based on different platforms (languages, processors, operating systems). The typical solution is to define a universal data type definition notation (e.g., IDL [#!OMG-CORBA!#] or XDR [#!Sun-Networking!#]) along with language bindings to translate data to and from the standard format. Data transformations necessary for transport can then be automated—typical RPC stub generation techniques already automate such transformations during transport for distributed client-server interactions [#!Sun-Networking!#]. The main shortcoming of DSI is its lack of support for bridging the differences between alternative representations of abstract types, such as the polar and cartesian representations of points in a plane. We need abstract type isomorphism (ATI) to fully support data mobility in a heterogeneous environment when data formats differ in more than platform-specific idiosyncrasies. I am interested in exploring an approach where user knowledge about the equivalence of various representations can be expressed declaratively in the form of equational laws (seen as bijections with two-way coercions) between representation types. The problem of establishing equivalence between representation types then reduces to the word problem in algebraic theories for which there are well-established automated techniques based on canonical term-rewriting. There are good research tools available to experiment with these techniques [#!Kapur-Zhang-RRL!#,#!Larch-LP-TR!#]. Inefficiencies due to multistage transformations can be eliminated by using techniques such as deforestation [#!Wadler-deforestation!#] if the transformations are themselves expressed declaratively using a functional language. Note that such transformations are of interest whether or not encapsulation of data-representation is important.

For a discussion of a closely related problem in the context of type reconstruction in functional languages, and the associated equational unification theory, see [#!Thatte-fpca91!#,#!Thatte-FAU93!#].