Changeset 2517 for Papers/polymorphic-variants-2012/polymorphic-variants.tex

Timestamp:

Dec 3, 2012, 11:51:17 AM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/polymorphic-variants-2012/polymorphic-variants.tex (modified) (1 diff)

Papers/polymorphic-variants-2012/polymorphic-variants.tex

@@ -426 +426 @@
 the extension.
 
+Thus we accept the following limitation, together with an additional requirement
+to mitigate the limitation:
+\begin{enumerate}
+ \item[3] We only encode \emph{bounded polymorphic variants}, whose typing
+  rules are given in Figure~\ref{???}.
+ \item[4] Bounded polymorphic variants are characterized by a universe, i.e.
+  a set of fields together with their type. Every bounded polymorphic variant
+  is a sub-variant of the universe, obtained by selecting only certain fields.
+  We ask that adding a new field to the universe should have no impact on
+  pre-existing code that does not use it. More precisely, it should be possible
+  to add a field to the universe and recompile all pre-existing developments
+  without further modifications.
+\end{enumerate}
+
+\subsection{Discussion on the requirements and alternative approaches}
+The set of requirements we have imposed drastically restrict the set of possible
+solutions for the encoding. Moreover, they clearly represent a trade off between
+flexibility and efficiency. We discuss here alternative approaches based on
+different set of requirements.
+
+Maximal flexibility is only obtained dropping the boundedness limitation.
+One of the benefits or open polymorphic variants is separate compilation:
+the developers of libraries can use their own set of constructors and the
+user can freely mix them when the types of the different fields are coherent.
+Moreover, separate compilation can be made efficient if one accepts that
+correct programs can be rejected with very low probability at linking
+time~\cite{guarriguexxx}.
+
+Requirement 4 has been imposed to recover the flexibility of open variants.
+Suppose that every library starts with a file that declares its own universe.
+Then, to mix two libraries, one needs to merge the two universe declarations
+together, which is only possible if the universes are coherent. Once this is
+done, the library files will keep compiling because of the requirement. What
+is irremediably lost is separate compilation. We believe that this loss can
+be withstood in many practical situations, because 1) merging of different
+libraries that need to share at least some constructor is rare and needs to
+be done just once; 2) the addition of new fields to the universe of a library
+under development usually requires a significant effort to fix the library that
+should make the recompilation time of the other libraries negligible.
+
+If separate compilation is considered fundamental, then the only possible
+approach seems that of introducing a syntactic data type (a universe) of
+descriptions of polymorphic variants type, which is then interpreted by
+dependent functions (type formers) to the appropriate sums of types.
+The problem, generalized to that of giving a universe to the full syntax of
+inductive types, is being studied by the groups of Altenkirch and
+Ghani~\cite{aa,bb,cc,dd}. This approach, which is mathematically
+very elegant, is in conflict with requirements 1 and 2. The conflict can be
+solved by devising an ad-hoc extraction procedure which targets a programming
+language that already implements polymorphic variants efficiently. As far as
+we know, this has not been done yet. The next generation of Epigram, however,
+is supposed to be implemented around this idea. Instead of an ad-hoc extraction
+procedure, Epigram will be directly compiled to executable code, optimizing the
+poor encodings that are generated by the syntactic universe.
+
+
 \subsection{Simulation (reduction + type checking)}
 \subsection{Examples}