Tagless Staged Interpreters for Simpler Typed Languages
Finally Tagless, Partially Evaluated, Tagless Staged Interpreters for Simpler Typed Languages.
It seems like a common wisdom that an embedding of a typed object language (e.g., DSL) to a typed meta-language so that all and only typed object terms can be represented requires dependent types, GADTs or other such advanced type systems. In fact, this problem of writing (tagless) type-preserving typed interpreters has been the motivation for most of the papers on GADTs. We show that regardless of merits and conveniences of GADTs, type-preserving typed interpretation can be achieved with no GADTs whatsoever, using very simple type systems of ML or Haskell98. We also show the same approach lets us perform statically type-preserving partial evaluation and call-by-value or call-by-name CPS tansformations. The latter transformations, too, are often claimed impossible in Haskell98 or ML - requiring instead quite advanced type systems or language features.
One of features of our approach is writing the DSL code in a form that can be interpreted in multiple ways. Recently we have become aware the very same approach underlies `abstract categorial grammars' (ACG) in linguistics. Chung-chieh Shan has written an extensive article on this correspondence. That post itself can be interpreted in several ways: the file can be read as plain text, or it can be loaded as it is in Haskell or OCaml interpreters.
It should be noted that the linguistic terms `tectogrammatics' and `phenogrammatics' were coined by none else but Haskell Curry, in his famous 1961 paper 'Some Logical Aspects of Grammatical Structure'. The summary of the ESSLLI workshop describes further connections to linear lambda-calculus.
The paper has been accepted for APLAS; the authors appreciate any comments indeed.
Active forum topics
New forum topics