Safe value I/O in Caml
We name ``value I/O'' a programming language input/output facility that is not restricted to elementary characters but can handles complex structured values as atomic writable entities. In a strongly-typed setting, this kind of high-level input/output raises new kind of safety problems: once a program has written a structured value to a file, any other unrelated program can read this value back in a completely different type context; to ensure type safety, it must be proven that the value read has a type that is compatible with the local context of the reader program. We studied what kind of type information must be accompanied with the written values, how to provide this type information to the input/output primitives, and the run-time type-checking mechanisms that ensure the type safety when reading the structured value. Based on the generic polymorphism framework, we constructed a mechanism that allows a safe value I/O facility that supports data exchange between distributed Caml programs. This system provides us two more additional results: on a practical level, dynamic values without any extra implementation cost, and on a more theoretical level, a new typing rule which can treat essentially polymorphic compositions of generic functions.
PPS | UFR P6 |