- Timestamp:
- Dec 3, 2012, 11:51:17 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/polymorphic-variants.tex
r2515 r2517 426 426 the extension. 427 427 428 Thus we accept the following limitation, together with an additional requirement 429 to mitigate the limitation: 430 \begin{enumerate} 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. 440 \end{enumerate} 441 442 \subsection{Discussion on the requirements and alternative approaches} 443 The set of requirements we have imposed drastically restrict the set of possible 444 solutions for the encoding. Moreover, they clearly represent a trade off between 445 flexibility and efficiency. We discuss here alternative approaches based on 446 different set of requirements. 447 448 Maximal flexibility is only obtained dropping the boundedness limitation. 449 One of the benefits or open polymorphic variants is separate compilation: 450 the developers of libraries can use their own set of constructors and the 451 user can freely mix them when the types of the different fields are coherent. 452 Moreover, separate compilation can be made efficient if one accepts that 453 correct programs can be rejected with very low probability at linking 454 time~\cite{guarriguexxx}. 455 456 Requirement 4 has been imposed to recover the flexibility of open variants. 457 Suppose that every library starts with a file that declares its own universe. 458 Then, to mix two libraries, one needs to merge the two universe declarations 459 together, which is only possible if the universes are coherent. Once this is 460 done, the library files will keep compiling because of the requirement. What 461 is irremediably lost is separate compilation. We believe that this loss can 462 be withstood in many practical situations, because 1) merging of different 463 libraries that need to share at least some constructor is rare and needs to 464 be done just once; 2) the addition of new fields to the universe of a library 465 under development usually requires a significant effort to fix the library that 466 should make the recompilation time of the other libraries negligible. 467 468 If separate compilation is considered fundamental, then the only possible 469 approach seems that of introducing a syntactic data type (a universe) of 470 descriptions of polymorphic variants type, which is then interpreted by 471 dependent functions (type formers) to the appropriate sums of types. 472 The problem, generalized to that of giving a universe to the full syntax of 473 inductive types, is being studied by the groups of Altenkirch and 474 Ghani~\cite{aa,bb,cc,dd}. This approach, which is mathematically 475 very elegant, is in conflict with requirements 1 and 2. The conflict can be 476 solved by devising an ad-hoc extraction procedure which targets a programming 477 language that already implements polymorphic variants efficiently. As far as 478 we know, this has not been done yet. The next generation of Epigram, however, 479 is supposed to be implemented around this idea. Instead of an ad-hoc extraction 480 procedure, Epigram will be directly compiled to executable code, optimizing the 481 poor encodings that are generated by the syntactic universe. 482 483 428 484 \subsection{Simulation (reduction + type checking)} 429 485 \subsection{Examples}
Note: See TracChangeset
for help on using the changeset viewer.