Supporting parameterized syntax and parsing would be helpful for implementing compilation by micro-passes. E.g. consider a fragment of C with local variables, expressions, statements, and function definitions; we might want to implement the following passes:
Scope: the type checker replaces symbolic local variables by addresses into an environment (e.g., array).
Expressions are compiled to stack machine instructions.
Statements are compiled to control flow (labels and jumps).
We would like to parameterize statements over the kind of expressions they contain (either trees or stack machine instructions) and the kind of variables (names or addresses). Likewise, expressions should be parameterized by the kind of variables.
This could be realized by a module system like Agda's.
module File A B C where -- top-level module parameterized by A B C
import OtherFile -- bring external module OtherFile into scope
type D = OtherFile.E -- use and export OtherFile.E as D
type DA = OtherFile.E A -- instantiate
type DA' = D A -- same
module M X where -- local module
...
module N = M A -- instantiated version of M
open N -- short for type Z = N.Z (for all Z)
A parameterized module would create parameterized data types for ASTs and likewise parameterized printers. Parsers would only be created for types (=categories) that are not parameterized.
Supporting parameterized syntax and parsing would be helpful for implementing compilation by micro-passes. E.g. consider a fragment of C with local variables, expressions, statements, and function definitions; we might want to implement the following passes:
We would like to parameterize statements over the kind of expressions they contain (either trees or stack machine instructions) and the kind of variables (names or addresses). Likewise, expressions should be parameterized by the kind of variables.
This could be realized by a module system like Agda's.
A parameterized module would create parameterized data types for ASTs and likewise parameterized printers. Parsers would only be created for types (=categories) that are not parameterized.