Changeset 2515 for Papers/polymorphicvariants2012
 Timestamp:
 Dec 2, 2012, 5:20:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2427 r2515 354 354 355 355 \section{Bounded polymorphic variants via dependent types} 356 Requirements (i.e. O(1) patternmatching, natural extracted code, etc.) 356 The topic of this paper, and this section in particular, is to present an 357 \emph{encoding} of a subclass of polymorphic variants into dependent type 358 theory. The final aim is to provide a solution to the expression problem 359 that is implementable in user space into interactive theorem provers 360 based on dependent type theories, in particular Coq, Agda and Matita. 361 Moreover, we are only interested into an encoding that satisfies a number 362 of constraints listed below. Essentially, the constraints ask that code 363 automatically extracted from the system should be compiled efficiently 364 without any change to the extraction machine. The encoding has been tested 365 in the interactive theorem prover Matita, but we believe that it should be 366 easily ported to the other cited systems. 367 368 \subsection{Code extraction} 369 Since our requirements have code extraction in mind, we briefly recall here 370 what code extraction is in our context. 371 372 Code extraction, as implemented in Coq, Matita and other systems, is the 373 procedure that, given a proof term, extracts a program in a functional 374 programming language that implements the computational content of the proof 375 term. In particular, all proof parts that only establish correctness of the 376 answer, totality of functions, etc. are to be erased. In particular, given 377 a precondition $P$ and a postcondition $Q$, from a 378 constructive proof of a $\forall x:A.P(x) \to \exists y:B. Q(x,y)$ statement 379 one extracts a (partial) function $f$ from the encoding of $A$ to the encoding 380 of $B$ that satisfies $\forall x. P(x) \to Q(x,f(x))$. 381 382 Code extraction, as implemented by the above systems, does not attempt any 383 optimization of the representation of data types. The only modification allowed 384 is that parts of the data that are propositional and thus bare no content 385 (being isomorphic to the unit type) are simplified to the unit type and 386 possibly completely erased using the categorical properties of unit types 387 ($1 * T \symeq T$, $1 \to T \symeq T$, etc.). For more information, one can 388 read~\cite{berardi,christinemohring,letouzey}. 389 390 Thus, if a polymorphic variant is encoded in type theory as an nary sum of 391 nary products, these being inefficiently represented using binary sums and 392 products, the same holds for the extracted code. 393 394 \subsection{The requirements} 395 396 We list the following requirements. 397 \begin{enumerate} 398 \item The representation of a polymorphic variant type in the extracted code 399 should be as efficient, in memory and time, as the isomorphic inductive 400 type. Efficiency should here be considered up to constants, and not 401 asymptotic. 402 \item Polymorphic types in the subtyping relation should be encoded using 403 data types that, once extracted, are in the subtyping relation too. 404 Before code extraction, instead, it is allowed to use explicit non identity 405 functions to coerce inhabitants of the subtype into the supertype. 406 What matters is that the computational content of these coercions should be 407 the identity. 408 \end{enumerate} 409 The first requirements prevents the encoding of polymorphic variants 410 using binary sums and products. For example, a constructor of an inductive 411 type with four constructors requires one memory cell, but the same constructor 412 for a binary sum of binary sums requires two memory cells, and twice the time 413 to inhabit the data type. The solution is to force the code extracted from the 414 polymorphic variant $\tau$ to be an inductive type. In turn this forces the 415 encoding of polymorphic variants to be based on inductive types. 416 417 The second requirement is in contrast with the possibility to extend a 418 polymorphic variant type: when a type $\tau$ is extended to $\tau + a:T$, 419 an inhabitant of the extraction of $\tau$ should already be an inhabitant of 420 the extraction of $\tau + a:T$. This is possible if polymorphic variants were 421 extracted to polymorphic variants in the target language, but this is not 422 actually the case in any of the considered systems (e.g. Coq or Matita). 423 Indeed, because of the first requirement, $\tau$ and $\tau + a:T$ are to be 424 extracted to two inductive types. The only way to obtain subtyping is to 425 already use the same representation: we need to anticipate or \emph{bound} 426 the extension. 427 357 428 \subsection{Simulation (reduction + type checking)} 358 429 \subsection{Examples}
Note: See TracChangeset
for help on using the changeset viewer.