Technical Report: No Type Stamps and No Structure Stamps - A Referentially-Transparent Higher-Order Module Language

A language for programming-in-the-large should support architectural descriptions of an entire product line. The evaluation of programs-in-the-large should generate the architecture of individual products and should link implementations-in-the-small to form an executable product. The Standard ML (SML) module language could serve this task, but it is not referentially transparent. Furthermore, it does not distinguish between architectural and implementational concerns. This paper presents a general module language that is based on a typed lambda calculus extended by systems . Overcoming SML's drawbacks, the module language permits syntactic control of type and structure generativity resulting in referential transparency. Furthermore, splitting up architectural and implementational concerns, the implementation of elementary modules is not part of the module language. The module calculus is essentially simply typed, with elementary modules and types as simple values, and interfaces and kinds as types. Function and system interfaces are value-dependent types.