jeudi 15 juin 2000 à 14h00

Safe value I/O in Caml

Jun Furuse (INRIA/Cristal)

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.

Page maintenue par Emmanuel Chailloux, dernière modification le 12/05/00 à 10h02

<<< PPS <<< UFR P6