Changeset 2517 for Papers

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


1 edited


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

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