Dependent vector types for data structuring in multirate Faust

作者：Jouvelot Pierre^*; Orlarey Yann

来源：Computer Languages, Systems and Structures, 2011, 37(3): 113-131.

DOI：10.1016/j.cl.2011.03.001

• Domain specific languages
• Synchronous signal processing
• Multirate computing
• Dependent type systems
• Static semantics
• Denotational semantics

Faust is a functional programming language dedicated to the specification of executable monorate synchronous musical applications. To extend Faust capabilities to important domains such as FFT-based spectral processing, we introduce here a multirate extension of the core Faust language. The novel idea is to link rate changes to data structure manipulation operations. Creating a vector-valued output signal divides the rate of input signals by the vector size, while serializing vectors multiplies rates accordingly. As duals to vectors, we also introduce record-like data structures, which are used to gather data but do not change signal rates. This interplay between data structures and rates is made possible in the language static semantics by the introduction of dependent types. We present a typing semantics, a denotational semantics and correctness theorems that show that this data structuring/multirate extension preserves the language synchronous characteristics. This new design is under implementation in the Faust compiler.

• 出版日期2011-7