Finally Tagless, Partially Evaluated Export

@incollection{citeulike:2703232, abstract = {We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers. Our main idea is to encode HOAS de Bruijn or higher-order abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck. To achieve self hyp interpretation and show Jones hyp optimality, we relate this exemplar of higher-rank and higher-kind polymorphism (provided by ML functors and Haskell\ 98 constructor classes) to plugging a term into a context of let hyp polymorphic bindings.}, author = {Carette, Jacques and Kiselyov, Oleg and Shan, Chung-Chieh}, citeulike-article-id = {2703232}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-76637-7_15}, citeulike-linkout-1 = {http://www.springerlink.com/content/346745075694944p}, doi = {10.1007/978-3-540-76637-7_15}, journal = {Programming Languages and Systems}, keywords = {functional}, pages = {222--238}, posted-at = {2008-04-23 02:22:07}, priority = {2}, title = {Finally Tagless, Partially Evaluated}, url = {http://dx.doi.org/10.1007/978-3-540-76637-7_15}, year = {2009} }

TY - CHAP ID - citeulike:2703232 L3 - citeulike-article-id:2703232 N2 - We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers. Our main idea is to encode HOAS de Bruijn or higher-order abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck. To achieve self hyp interpretation and show Jones hyp optimality, we relate this exemplar of higher-rank and higher-kind polymorphism (provided by ML functors and Haskell 98 constructor classes) to plugging a term into a context of let hyp polymorphic bindings. JF - Programming Languages and Systems EP - 238 TI - Finally Tagless, Partially Evaluated SP - 222 KW - functional AU - Carette, Jacques AU - Kiselyov, Oleg AU - Shan, Chung-Chieh PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-540-76637-7_15 ER -