Changeset 2515 for Papers

Dec 2, 2012, 5:20:39 PM (9 years ago)


1 edited


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

    r2427 r2515  
    355355\section{Bounded polymorphic variants via dependent types}
    356 Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
     356The 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
     358theory. The final aim is to provide a solution to the expression problem
     359that is implementable in user space into interactive theorem provers
     360based on dependent type theories, in particular Coq, Agda and Matita.
     361Moreover, we are only interested into an encoding that satisfies a number
     362of constraints listed below. Essentially, the constraints ask that code
     363automatically extracted from the system should be compiled efficiently
     364without any change to the extraction machine. The encoding has been tested
     365in the interactive theorem prover Matita, but we believe that it should be
     366easily ported to the other cited systems.
     368\subsection{Code extraction}
     369Since our requirements have code extraction in mind, we briefly recall here
     370what code extraction is in our context.
     372Code extraction, as implemented in Coq, Matita and other systems, is the
     373procedure that, given a proof term, extracts a program in a functional
     374programming language that implements the computational content of the proof
     375term. In particular, all proof parts that only establish correctness of the
     376answer, totality of functions, etc. are to be erased. In particular, given
     377a precondition $P$ and a postcondition $Q$, from a
     378constructive proof of a $\forall x:A.P(x) \to \exists y:B. Q(x,y)$ statement
     379one extracts a (partial) function $f$ from the encoding of $A$ to the encoding
     380of $B$ that satisfies $\forall x. P(x) \to Q(x,f(x))$.
     382Code extraction, as implemented by the above systems, does not attempt any
     383optimization of the representation of data types. The only modification allowed
     384is 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
     386possibly 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
     390Thus, if a polymorphic variant is encoded in type theory as an n-ary sum of
     391n-ary products, these being inefficiently represented using binary sums and
     392products, the same holds for the extracted code.
     394\subsection{The requirements}
     396We list the following requirements.
     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 sub-type into the super-type.
     406   What matters is that the computational content of these coercions should be
     407   the identity.
     409The first requirements prevents the encoding of polymorphic variants
     410using binary sums and products. For example, a constructor of an inductive
     411type with four constructors requires one memory cell, but the same constructor
     412for a binary sum of binary sums requires two memory cells, and twice the time
     413to inhabit the data type. The solution is to force the code extracted from the
     414polymorphic variant $\tau$ to be an inductive type. In turn this forces the
     415encoding of polymorphic variants to be based on inductive types.
     417The second requirement is in contrast with the possibility to extend a
     418polymorphic variant type: when a type $\tau$ is extended to $\tau + a:T$,
     419an inhabitant of the extraction of $\tau$ should already be an inhabitant of
     420the extraction of $\tau + a:T$. This is possible if polymorphic variants were
     421extracted to polymorphic variants in the target language, but this is not
     422actually the case in any of the considered systems (e.g. Coq or Matita).
     423Indeed, because of the first requirement, $\tau$ and $\tau + a:T$ are to be
     424extracted to two inductive types. The only way to obtain subtyping is to
     425already use the same representation: we need to anticipate or \emph{bound}
     426the extension.
    357428\subsection{Simulation (reduction + type checking)}
Note: See TracChangeset for help on using the changeset viewer.