Martin Elsman

Troels Henriksen

Danil Annenkov
email: danil.annenkov@inria.fr

Cosmin E Oancea
email: coancea@di.ku.dk.

Static interpretation of higher-order modules in Futhark: functional GPU programming in the large

Keywords: CCS Concepts:, Software and its engineering → Abstraction, modeling and modularity, Parallel programming languages, Functional languages, Modules / packages, Semantics, modules, GPGPU, functional languages, compilers

come   L'archive ouverte pluridisciplinaire

INTRODUCTION

Programming massively parallel hardware is increasingly becoming a central aspect of developing computational software kernels. Research in developing programming abstraction mechanisms for effectively utilizing massively parallel hardware has resulted in a number of available tools, ranging from low-level programming models, such as CUDA and OpenCL, over domain-specific languages and libraries, such as Accelerate [START_REF] Manuel Mt Chakravarty | Accelerating Haskell array codes with multicore GPUs[END_REF][START_REF] Mcdonell | Optimising Purely Functional GPU Programs[END_REF], Obsidian [START_REF] Claessen | Expressive Array Constructs in an Embedded GPU Kernel Programming Language[END_REF][START_REF] Svensson | Obsidian: GPU Kernel Programming in Haskell[END_REF], Lift [START_REF] Steuwer | Generating Performance Portable Code Using Rewrite Rules: From High-level Functional Expressions to High-performance OpenCL Code[END_REF][START_REF] Steuwer | Lift: A Functional Data-parallel IR for High-performance GPU Code Generation[END_REF], and CUBLAS, to full programming languages, such as SaC [START_REF] Guo | Breaking the GPU Programming Barrier with the Auto-parallelising SAC Compiler[END_REF] and Futhark [Henriksen et al. 2014;Henriksen and Oancea 2014;[START_REF] Henriksen | Futhark: Purely Functional GPU-programming with Nested Parallelism and In-place Array Updates[END_REF].

With software components that utilise massively parallel hardware getting larger and more complicated, an increasing need emerges in this area for good software structuring mechanisms and high reusability of developed software components. In the last decades, a number of abstraction mechanisms have been introduced that allow programmers to reason at a high level about the composition of developed software components. Such mechanisms include object-oriented class-based programming mechanisms, type class structuring mechanisms, as found in Haskell [START_REF] Wadler | How to Make Ad-hoc Polymorphism Less Ad Hoc[END_REF], module-languages as found in Standard ML [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF]] and OCaml [START_REF] Leroy | Applicative Functors and Fully Transparent Higher-order Modules[END_REF], and extensions [START_REF] Rossberg | Mixin' Up the ML Module System[END_REF] and combinations [START_REF] Dreyer | Modular Type Classes[END_REF][START_REF] White | Modular implicits[END_REF] thereof.

A common issue with the work on modules, and abstraction mechanisms in general, is that the mechanisms seldom give guarantees about their overhead. Often, the mechanisms introduce runtime overhead in terms of, for instance, dynamic method invocation, or packages (e.g., dictionaries or modules) being passed around at runtime. At best, an optimizing compiler can eliminate much of this overhead statically, but the interaction between the core language and the language for programming in the large is often subtle and without paying attention to the interaction mechanisms, it will be difficult for a compiler to provide guarantees that refactoring for increasing modularity will not affect performance.

One promising technique for solving some of these issues is the work on embedded domain-specific languages (EDSLs), which provide a structuring mechanism based on host language features for structuring and composing components. Examples of such approaches to orchestrate programming for massively parallel hardware include Accelerate, Obsidian, and Firepile [START_REF] Nystrom | Firepile: Run-time Compilation for GPUs in Scala[END_REF], which are libraries, written in Haskell and Scala, for synthesizing code for running on GPGPUs. However, designing a well-working EDSL is not a trivial task as the developer needs to work hard, for instance to avoid unintended code duplication [START_REF] Mainland | Nikola: Embedding Compiled GPU Functions in Haskell[END_REF]. Another issue with EDSLs is that they can be difficult to incorporate in code generation pipelines as the language cannot necessarily be understood in isolation from its host-language, which may cause both practical problems and reasoning problems with respect to guaranteeing correctness of a compilation pipeline.

In this paper, we introduce the notion of higher-order static interpretation. The work is based on earlier work on static interpretation for Standard ML [START_REF] Elsman | Static Interpretation of Modules[END_REF]], which provides a technique for complete static elimination of modules, including first-order modules (called functors in Standard ML). The technique is similar to how C++ templates are eliminated at compile time with the difference that modules are type checked before they are compiled. The present paper extends the previous work to higher-order modules. We demonstrate the usefulness of the added functionality and argue for the need for higher-order modules and type abstraction. The module language is implemented on top of the monomorphic, first-order functional data-parallel language Futhark, which features a number of polymorphic second-order array combinators (SOACs) with parallel semantics, such as map, reduce, scan, and filter. The Futhark core language makes it possible to write data-parallel kernels that are often competitive with hand-written CUDA or OpenCL applications [START_REF] Andreetta | FinPar: A Parallel Financial Benchmark[END_REF]Henriksen et al. 2016b[START_REF] Henriksen | Futhark: Purely Functional GPU-programming with Nested Parallelism and In-place Array Updates[END_REF][START_REF] Rasmus | Strategies for Regular Segmented Reductions on GPU[END_REF]. We show that the practical implications of the module language give rise to highly reusable components, which, for instance, form the grounds of a Basis Library for Futhark.

Although the basic module language that we present is both elegant and simple, it features a number of derived forms, which makes the language practical while keeping the technical details minimal. Special derived forms allow programmers to declare certain kinds of polymorphic higher-order functions and types. The declarations are turned into parameterised modules, which are then instantiated at the module level for each use.

An essential property of static interpretation of higher-order modules is that it is strongly normalizing, which is based on a logical-relation argument, similar to an argument for strongnormalisation of the simply-typed lambda-calculus [START_REF] Tait | Intensional interpretations of functionals of finite type[END_REF]]. The important properties of the module language (e.g., normalisation of static interpretation) has been proven in Coq and both the Futhark compiler, featuring the full module language, and the Coq implementation are available online.

In summary, we claim the following novel contributions:

(1) We show how the concept of static interpretation can be extended to higher-order modules and present an implementation as part of a compiler for Futhark.

(2) We demonstrate the usefulness of a higher-order module system for GPU programming by presenting a number of modularised Futhark examples and by arguing (and demonstrating) that the modularisation has no influence on performance.

(3) Using a novel adaptation of a logical-relation argument, we show that static interpretation terminates and that target and source programs are typed consistently. (4) We provide a formal development in Coq, which uses a novel encoding of semantic objects for modules based on products, sets, and finite maps. The encoding closely resembles the paper formalisation and the implementation for Futhark.

The paper is organised as follows. In the next section, we introduce the higher-order module language and present a motivating example demonstrating the use of higher-order modules in Futhark. In Section 3, we give an overview of how static interpretation turns higher-order modules into monomorphic core language Futhark code. In Section 4, we present the static semantics for the module language and show how the module language interacts with the core language. Section 5 presents the technicalities of static interpretation and Section 6 presents the main technical result, namely that static interpretation terminates and that the resulting program, from a type perspective, is consistent with the source program, which may possibly contain declarations and applications of higher-order modules. In Section 7, we briefly discuss the type inference algorithm. In Section 8, we present a number of derived forms for allowing programmers to use traditional syntax for polymorphic functions and function application for generating parameterised code at the module level and for instantiating this code also at the module level. In Section 9, we discuss the Coq development and in Section 10, we discuss the application of the module language in the concrete setting of the Futhark compiler. We present a few larger examples of Futhark modules and demonstrate that, in practice, the module language is a useful technology for improving code reuse and code abstraction and that it introduces no overhead with respect to performance of the generated code. In Section 11 and Section 12, we discuss related work and conclude.

THE MODULE LANGUAGE

The module language can be considered parameterised over a core language, which, for the purpose of the presentation, is a simple functional language. In the practical implementation, the core language is a full-fledged programming language for data-parallel programming featuring a number of second-order polymorphic array combinators (SOACs) with parallel semantics but with no support for user-defined polymorphic higher-order functions.

For the core language considered here, we assume denumerably infinite sets of type identifiers (tid), value identifiers (vid), and module identifiers (mid). For each of the above identifier sets 𝑋, we define the associated set of long identifiers Long𝑋, inductively with 𝑋 as the base set and mid.long𝑥 as the inductive case with long𝑥 ∈ Long𝑋 and mid being a module identifier. For the module language, we also assume a denumerably infinite set of module type identifiers (mtid). Long identifiers, such as 𝑥.𝑦.𝑧, allow users to use traditional dot-notation for accessing components deep within modules and the separation of identifier classes makes it clear in what syntactic category an identifier belongs.

The simple core language is defined by notions of type expressions (ty), core language expressions (exp), and core language declarations (dec): The core language can be understood entirely in isolation from the module language except that long identifiers may be used to access values and types in modules. As will become apparent in the typing rules for the core language, the construct 𝜆vid → exp binds vid in exp and the declaration of a value identifier in a val-declaration allows for other declarations to depend on it. For simplicity, composition of core language constructs are handled entirely by the module language and so is the possibility for declaring types. An important aspect here is that the dependency structure between declarations is not allowed to be cyclic.

The grammar for the module language is given in Figure 1. The module language is separated into a language for specifying module types (mty) and a language for declaring modules (mdec). The language for module types is a two-level language with sub-languages for specifying module components and for expressing module types. Similarly, the language for declaring (i.e., defining) modules is a two-level language for declaring module components and for expressing module manipulations. At the toplevel, a program is a module declaration, possibly consisting of a sequence of module declarations where later declarations may depend on earlier declarations. To resolve ambiguities, parentheses are allowed around module type expressions and around module expressions. As will become apparent from the typing rules, in declarations of the form mdec 1 mdec 2 , identifiers declared by mdec 1 are considered bound in mdec 2 (similar considerations hold for composing specifications and programs).

Without lack of generality, a number of additional constructs are supported by considering them derived forms, following [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF]] and [START_REF] Rossberg | F-ing modules[END_REF]. Such derived forms include constructs for local module bindings, direct application of a module expression to another module expression, constructs for opaque matching (in Standard ML terms), and support for type abbreviations in module type specifications: Although the derived form of Equation 5, for matching a module expression to a module type expression, allows us to simplify the semantic treatment of the module language, we shall later present a specialised typing rule specifying how a module expression mexp is classified by a given module type expression mty under some environment. Type abbreviations in module type specifications are also considered a derived form (Equation 8) using an include construct and a with-constrained module type expression, which in itself is arguably more expressive than a type abbreviation, as it resembles a substitution and allows for reuse of module types. Another possible derived form introduces a construct for modeling the semantics of OCaml's open construct (not shown here), which opens a module in a local scope contrary to the semantics of open defined here, which resembles the semantics of open in Standard ML.

module 𝐹 ( 𝑋 : mty ) = mexp mdec =⇒ module 𝐹 = 𝜆𝑋 : mty → mexp (1) local mdec in mexp mdec =⇒ open let mdec in mexp (2) let mdec in mexp mexp =⇒ { mdec module 𝑋 = mexp } . 𝑋 (3) mexp 1 ( mexp 2 ) mexp =⇒ let module 𝐹 = mexp 1 in 𝐹 (mexp 2 ) (4) mexp : mty mexp =⇒ (𝜆𝑋 : mty → 𝑋) (mexp) (5
As described in more detail in Section 8, certain kinds of polymorphic higher-order functions and polymorphic types, as known from traditional higher-order polymorphic languages such as Standard ML, OCaml, and Haskell, can also be introduced as derived forms together with derived forms for instantiating such declared higher-order modules. By introducing derived forms only at the module level, we can be sure that all modules are indeed eliminated entirely at compile time.

We conclude this section by discussing a practical example, shown in Figure 2, in which the module language is used to extend, at library level, the set of SOACs supported in Futhark. Notice that the syntax for types is extended to also support array types, which take the form []𝜏 , for some 𝜏 , which may possibly also be an array type. Here, the aim is to implement segmented scan based on the natively supported scan bulk-parallel operator,1 which is applied in the main function. The implementation starts by declaring a Numeric module type that exports a numeric type t, a zero element (of type t), and various numeric operations such as addition. A possible implementation is given by module i32, which instantiates t to 32-bit integers.

Next, the Monoid module type is declared to export a type t, together with a binary associative operator op with neutral element ne:t. A potential implementation for Monoid is the parameterised module Plus, which receives a module parameter N implementing Numeric and instantiates Monoid's t, zero and op with N.t, N.zero and N.+, respectively. Finally, new SOACs are derived from the ones natively supported by Futhark in the parameterised module SOACs, which receives as parameter a monoid E corresponding to the array element type, and declares an inner parameterised module for each new SOAC. For example, SgmScan takes as parameter a monoid-implementing module M, and implements the segmented-scan operator bulkop based on Futhark's scan (not shown). Function main computes a segmented scan with the plus operator on a (segmented) array of 32-bit integers.

EXECUTIVE SUMMARY

For the purpose of demonstrating static interpretation in action, consider the (contrived) example Futhark program in Figure 3a. Compared to the motivating example in Section 2, the program here makes no use of derived forms and it therefore serves well as a running example demonstrating the technique. The program declares a module type MT and a Static Interpretation of Higher-Order Modules in Futhark 97:7 higher-order module H, which is applied to a module containing a parameterised module F. The result of the module application is a module containing a function f of type i32 → i32. The contained function is called in the main function with the input to the program.

The static semantics of the language, which we shall later define in terms of a set of elaboration rules, provides evidence that the code in Figure 3a is well-typed with the intended guarantee that the program can be executed without dynamic type errors occurring. Static interpretation for the example in Figure 3a partially evaluates the program to achieve the three code snippets shown in Figure 3b. Each of the three code snippets contains monomorphic target code, which can be composed, analysed, and compiled without any module language considerations. This feature provides the target language implementor with the essential meta-level abstraction property that the module language features are orthogonal to the domain of the source language. In other words, the target language implementor need not worry that the added modularity constructs will have any influence on composing the generated code. This property is essential for targeting data-parallel architectures, such as GPUs, but may also be essential for a variety of other domain specific languages, including languages for financial contracts [START_REF] Simon | Composing Contracts: an Adventure in Financial Engineering (functional pearl)[END_REF], probabilistic programming, hardware design, signal processing, and formal reasoning.

At the technical side, static interpretation takes care of renaming identifiers properly to resolve scope-issues. In Section 6, we demonstrate that if the source language is well-typed then (1) static interpretation will generate target language code and (2) the generated target language code will be consistent with the source language code with respect to the types of declared identifiers. An essential aspect of the approach is that the generation of target code is shown to be terminating using a logical-relations argument, which is properly formalised and backed up by a proof in Coq. For limiting the scope of the presentation, we shall not here provide the reader with a direct dynamic semantics for the module language. Instead, the dynamic semantics for the language can be understood as the composition of static interpretation and the dynamic semantics of the target language. Providing a direct dynamic semantics for the module language, along the lines of the dynamic semantics of [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF], would be straightforward and would resemble closely the rules for static interpretation.

In what follows, we develop the precise formalism that makes static interpretation possible, including a proper treatment of abstract types at the module language level.

STATIC SEMANTICS

The static semantics that we present here elaborates well-typed syntactic constructs into so-called semantic objects, which are based on well-established mathematical constructs such as products, finite maps, and sets. This style of elaboration approach resembles closely the style of elaboration set forward by [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF], although modified to use universal and existential quantification for treating certain objects equal up-to 𝛼-renaming, as set forward by [START_REF] Russo | Non-dependent Types for Standard ML Modules[END_REF] and [START_REF] Elsman | Static Interpretation of Modules[END_REF].

For the static semantics, we assume a denumerably infinite set TSet of type variables (t). A semantic type (or simply a type), ranged over by 𝜏 , takes the form:

𝜏 ::= 𝑡 | 𝜏 1 → 𝜏 2
Types relate straightforwardly to syntactic types with the difference that syntactic types contain type identifiers and semantic types contain type variables. This difference is essential in that it enables the support for type parameterisation and type abstraction. At the core level, a value environment (VE ) maps value identifiers (vid) to types and a type environment (TE ) maps type identifiers (tid) to types.

𝐸 = (TE , VE , ME , 𝐺) ∈ Env = TEnv × VEnv × MEnv × MTEnv ME ∈ MEnv = Mid fin → Mod 𝑀 ∈ Mod = Env ∪ FunSig 𝐹 = ∀𝑇.(𝐸, Σ) ∈ FunSig = Fin(TSet) × Env × MTy Σ = ∃𝑇.𝑀 ∈ MTy = Fin(TSet) × Mod 𝐺 ∈ MTEnv = MTid fin → MTy
The module language semantic objects are shown in Figure 4. The semantic objects constitute a number of mutually dependent inductive definitions. An environment (𝐸) is a quadruple (TE , VE , ME , 𝐺) of a type environment TE , a variable environment VE , a module environment (ME ), which maps module identifiers to modules, and a module type environment (𝐺), which maps module type identifiers to module types. A module is either an environment 𝐸, representing a non-parameterised module, or a parameterised module type 𝐹 , which is an object ∀𝑇.(𝐸, Σ), for which the type variables in 𝑇 are considered bound. A module type (Σ) is a pair, written ∃𝑇.𝑀 , of a set of type variables 𝑇 and a module 𝑀 . In a module type ∃𝑇.𝑀 , type variables in 𝑇 are considered bound and we consider module types identical up-to renaming of bound variables and removal of type variables that do not appear in 𝑀 . When 𝑇 is empty, we often write 𝑀 instead of ∃∅.𝑀 . We consider module function types ∀𝑇.(𝐸, Σ) identical up-to renaming of bound type variables and removal of type variables in 𝑇 that do not occur free in (𝐸, Σ).

When 𝑋 is some tuple and when 𝑥 is some identifier, we shall often write 𝑋(𝑥) for the result of looking up 𝑥 in the appropriate projected finite map in 𝑋. Moreover, when long𝑥 is some long identifier, we write 𝑋(long𝑥) to denote the lookup in 𝑋, possibly inductively through module environments.

When 𝑋 and 𝑌 are finite maps, the modification of 𝑋 by 𝑌 , written 𝑋 + 𝑌 , is the map with Dom(𝑋 + 𝑌 ) = Dom 𝑋 ∪ Dom 𝑌 and values

(𝑋 + 𝑌 )(𝑥) = { 𝑌 (𝑥) if 𝑥 ∈ Dom 𝑌 𝑋(𝑥) otherwise
The notion of modification is extended point-wise to tuples, as are operations such as Dom, ∩, and ∪. A finite map 𝑋 extends another finite map 𝑋 ′ , written

𝑋 ⊒ 𝑋 ′ , if Dom 𝑋 ⊇ Dom 𝑋 ′ and 𝑋(𝑥) = 𝑋 ′ (𝑥) for all 𝑥 ∈ Dom 𝑋 ′ .
Given a particular kind of environment, such as a module environment ME , we shall often be implicit about its injection ({}, {}, ME , {}) into environments of type Env. Moreover, given an identifier, such as tid, its class specifies exactly that, given some type 𝜏 , {tid ↦ → 𝜏 } denotes a type environment of type TE , which again, by the above convention, can be injected implicitly into an environment of type Env.

As an example, if t is a type identifier, a and b are value identifiers, and A is a module identifier, we can write {t ↦ → 𝑡} + {A ↦ → {a ↦ → 𝑡}} for specifying the environment 𝐸 = ({t ↦ → 𝑡}, {}, {A ↦ → 𝐸 ′ }, {}), where 𝐸 ′ = ({}, {a ↦ → 𝑡}, {}, {}) and where 𝐸 ⊒ {t ↦ → 𝑡}. Moreover, looking up the long identifier A.a in 𝐸, written 𝐸(A.a), yields 𝑡.

Static Interpretation of Higher-Order Modules in Futhark 97:9 Figure 5 shows the outer-level environment for the code example in Figure 3, which are obtained by applying the elaboration (typing) rules, which are presented in the remainder of this section.

𝐸 𝑃 𝑟𝑔 = ( {}, {main ↦ → (i32 → i32)}, ME 𝑃 𝑟𝑔 , {MT ↦ → Σ 𝑀 𝑇 } ) where ME 𝑃 𝑟𝑔 = {Main ↦ → M 𝑓 , H ↦ → ∀∅.( ({}, {}, {F ↦ → Σ 𝐹 }, {}), ∃∅.M 𝑓 )} Σ 𝑀 𝑇 = ∃∅.({}, {}, {F ↦ → Σ 𝐹 }, {}) Σ 𝐹 = ∀∅.( ({}, {b ↦ → i32}, {}, {}), ∃∅.M 𝑓 ) M 𝑓 = ( {}, {f ↦ → (i32 → i32)}, {}, {} )

Enrichment

Enrichment specifies that an environment, in an inductive sense, has the same or more elements than another environment. Enrichment is mutually and inductively defined on module environments, modules, and environments. The concept is central to the understanding of parameterised module application and matching. An environment

𝐸 ′ = (TE ′ , VE ′ , ME ′ , 𝐺 ′ ) enriches another environment 𝐸 = (TE , VE , ME , {}), written 𝐸 ′ ≻ 𝐸, if VE ′ ⊒ VE , TE ′ ⊒ TE , and ME ′ ≻ ME . A module environment ME ′ enriches another module envi- ronment ME , written ME ′ ≻ ME , if Dom ME ′ ⊇ Dom ME and ME ′ (mid) ≻ ME (mid) for each mid ∈ Dom ME . A module 𝑀 ′ = 𝐸 ′ enriches another module 𝑀 = 𝐸, written 𝑀 ′ ≻ 𝑀 , if 𝐸 ′ ≻ 𝐸. Moreover, a module 𝑀 ′ = ∀𝑇 ′ .(𝐸 ′ , Σ ′ ) enriches another module 𝑀 = ∀𝑇.(𝐸, Σ), written 𝑀 ′ ≻ 𝑀 , if 𝑇 ′ = 𝑇 and 𝐸 ≻ 𝐸 ′ and Σ ′ ≻ Σ.
Notice that enrichment for parameterised modules is contravariant in parameter environments. Notice also the special treatment of module type environments. Because a module type cannot specify bindings of module types (such a possibility creates a number of problems that are complementary to static interpretation), we can safely require that when 𝐸 ′ ≻ 𝐸, the module type environment in 𝐸 is empty. A simpler approach was chosen than a more rigid semantic object structure that would capture precisely the non-supportedness of module type bindings inside modules.

Instantiation

Another central concept for understanding parameterised module application and module matching is the notion of instantiation, which is used for capturing that a particular module is a concrete instance of a generic module type. Instantiation is based on the notion of a substitution (𝑆), which maps type variables to types. The result of applying a substitution 𝑆 to an object 𝑋, written 𝑆(𝑋), is first to extend the substitution to be the identity outside its domain and then simultaneously substitute each type variable 𝑡 in 𝑋 with 𝑆(𝑡), after appropriately renaming bound type variables in 𝑋. The support of a substitution 𝑆, written Supp 𝑆, is the set of elements 𝑡 for which 𝑆(𝑡) ̸ = 𝑡.

Formally, then, an object 𝐴 instantiates another object 𝐵, written 𝐴 ≤ 𝐵, if the judgement can be derived according to the following rules:

𝐸 ≤ 𝐸 ′ Dom(ME ) = Dom(ME ′ ) ∀mid ∈ Dom(ME ), ME (mid) ≤ ME ′ (mid) (TE , VE , ME , 𝐺) ≤ (TE , VE , ME ′ , 𝐺) 𝐹 ≤ 𝐹 ′ (𝐸, Σ) ≤ ∀𝑇 ′ .(𝐸 ′ , Σ ′ ) 𝑇 ∩ tvs(∀𝑇 ′ .(𝐸 ′ , Σ ′ )) = ∅ ∀𝑇.(𝐸, Σ) ≤ ∀𝑇 ′ .(𝐸 ′ , Σ ′ ) Type Expressions. 𝐸 ⊢ ty : 𝜏 𝐸(longtid) = 𝜏 𝐸 ⊢ longtid : 𝜏 (9) 𝐸 ⊢ ty 𝑖 : 𝜏 𝑖 𝑖 = [1, 2] 𝐸 ⊢ ty 1 → ty 2 : 𝜏 1 → 𝜏 2 (10) Core Language Expressions. 𝐸 ⊢ exp : 𝜏 𝐸(longvid) = 𝜏 𝐸 ⊢ longvid : 𝜏 (11) 𝐸 ⊢ exp : 𝜏 𝐸 ⊢ ty : 𝜏 𝐸 ⊢ exp : ty : 𝜏 (12) 𝐸 + {vid ↦ → 𝜏 } ⊢ exp : 𝜏 ′ 𝐸 ⊢ 𝜆vid → exp : 𝜏 → 𝜏 ′ (13) 𝐸 ⊢ exp 1 : 𝜏 → 𝜏 ′ 𝐸 ⊢ exp 2 : 𝜏 𝐸 ⊢ exp 1 exp 2 : 𝜏 ′ (14)
Fig. 6. Elaboration rules for the core language. The rules are straightforward but illustrate the interaction between the module language and the core language through the concept of long identifiers.

𝐸 ≤ Σ Supp(𝑆) ⊆ 𝑇 𝐸 ≤ 𝑆(𝐸 ′ ) 𝐸 ≤ ∃𝑇.𝐸 ′ Σ ≤ Σ ′ 𝑇 ∩ tvs(∃𝑇 ′ .𝐸 ′ ) = ∅ 𝐸 ≤ ∃𝑇 ′ .𝐸 ′ ∃𝑇.𝐸 ≤ ∃𝑇 ′ .𝐸 ′ (𝐸, Σ) ≤ ∀𝑇 ′ .(𝐸 ′ , Σ ′ ) Supp(𝑆) ⊆ 𝑇 𝑆(𝐸 ′ ) ≤ 𝐸 Σ ≤ 𝑆(Σ ′ ) (𝐸, Σ) ≤ ∀𝑇 ′ .(𝐸 ′ , Σ ′ )
Notice the contravariance in the rule for instantiating a parameterised module type and that instantiation is applied inductively in the rules, which differs from how instantiation is defined in the case for first-order modules [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF]]. For instance, with this revised instantiation relation, given that {t ↦ → 𝜏 } represents an environment mapping a type constructor to a type 𝜏 , a concrete parameterised module type ∀∅.({}, {t ↦ → i32}) instantiates the more abstract parameterised module type ∀∅.({}, ∃{𝑡}.{t ↦ → 𝑡}).

The notion of matching combines the notions of enrichment and instantiation. An environment 𝐸 matches a module type Σ if there exists another environment 𝐸 ′ such that 𝐸 ≻ 𝐸 ′ and 𝐸 ′ ≤ Σ. Matching is central in the elaboration rule for applications of parameterised modules and to the notions of encapsulation and abstraction, in general.

Elaboration

Elaboration of the module language is based on elaboration rules for the core language, which are straightforward and presented in Figure 6. The rules are split into rules for type expressions and rules for value expressions and allow for inferences of the forms 𝐸 ⊢ ty : 𝜏 and 𝐸 ⊢ exp : 𝜏 , which are read "under assumptions 𝐸, the type expression ty (or value expression exp) is elaborated to have type 𝜏 ". Notice how the core language interacts with the module language through the use of long identifiers in Rule 9 and Rule 11.

Elaboration of module types and specifications is defined as a mutual inductive relation allowing inferences among sentences of the forms 𝐸 ⊢ mty : Σ and 𝐸 ⊢ spec : ∃𝑇.𝐸 ′ . The rules are presented in Figure 7. There is a subtle difference between module type expressions (mty) and specifications (spec). Whereas module type expressions may elaborate to parameterised module types, specifications only elaborate to non-parameterised module types, which may, however, contain parameterised modules inside. Thus, in Rule 22, we require that the included module is a non-parameterised module type.

The most interesting of the rules are Rule 16, the rule for with-types, and Rule 18, the rule for expressing parameterised modules as dependent products [START_REF] Harper | A Type-Theoretic Approach to Higher-Order Modules with Sharing[END_REF].

Static Interpretation of Higher-Order Modules in Futhark 97:11 Module Types.

𝐸 ⊢ mty : Σ

𝐸(mtid) = Σ 𝐸 ⊢ mtid : Σ (15) 𝐸 ⊢ ty : 𝜏 𝐸 ′ (longtid) = 𝑡 𝑡 ∈ 𝑇 𝐸 ⊢ mty : ∃𝑇.𝐸 ′ Σ = ∃(𝑇 ∖ {𝑡}).(𝐸 ′ [𝜏 /𝑡]) 𝐸 ⊢ mty with longtid = ty : Σ (16) 𝐸 ⊢ spec : Σ 𝐸 ⊢ { spec } : Σ (17) 𝐸 ⊢ mty 1 : ∃𝑇.𝐸 ′ 𝑇 ∩ (tvs(𝐸) ∪ 𝑇 ′ ) = ∅ 𝐸 + {mid ↦ → 𝐸 ′ } ⊢
𝐸 ⊢ spec 1 : ∃𝑇 1 .𝐸 1 𝐸 + 𝐸 1 ⊢ spec 2 : ∃𝑇 2 .𝐸 2 𝑇 1 ∩ (tvs(𝐸) ∪ 𝑇 2 ) = ∅ Dom 𝐸 1 ∩ Dom 𝐸 2 = ∅ 𝐸 ⊢ spec 1 spec 2 : ∃(𝑇 1 ∪ 𝑇 2 ).(𝐸 1 + 𝐸 2 ) (23) 𝐸 ⊢ 𝜖 : ∃∅.{} (24)
Fig. 7. Elaboration rules for module types and module specifications. This sub-language does not directly depend on the rules for module expressions and module declaration.

The rule for with-types (also called where-types in Standard ML) allows a programmer to refine a module type to a more concrete module type. The rule for expressing parameterised module types allow a programmer to express dependencies between the parameter module and the result module by referring to the module identifier associated with the parameter.

As an example, consider the module type expression

X:{ type t val a : t } → { val b : X.t }
This module type expression elaborates, using, among others, Rule (16), to the module type

∀{𝑡}.({t ↦ → 𝑡, a ↦ → 𝑡}, ∃∅.{b ↦ → 𝑡})
An essential aspect of the semantic technique is that of requiring, for instance, that the sets 𝑇 1 and 𝑇 2 in Rule (23) are disjoint. This property can always be satisfied by 𝛼-renaming, which is applied often (and in the Coq implementation, explicitly) when proving properties.

Elaboration Rules for Module Expressions and Module Declarations

The elaboration rules for module language expressions and declarations are given in Figure 8 and allow inferences among sentences of the forms 𝐸 ⊢ mdec : Σ and 𝐸 ⊢ mexp : ∃𝑇.𝐸. The rules make use of the previously introduced rules for module type expressions and core language declarations and types. Similarly to the elaboration difference between module type expressions and specifications, module expressions elaborate to general module types ∃𝑇.𝑀 , whereas module declarations elaborate to non-parameterised module types ∃𝑇.𝐸.

The by far most complicated rule is Rule (29), the rule for application of a parameterised module. The rule looks up a parameterised module type ∀𝑇 0 .(𝐸 0 , Σ 0 ) for the long module Module Expressions.

𝐸 ⊢ mexp : Σ identifier in the environment and seeks to match the parameter module type ∃𝑇 0 .𝐸 0 against a cut-down version (according to the enrichment relation) of the module type resulting from elaborating the argument module expression. The result of elaborating the application is the result module type, perhaps with additional abstract type variables stemming from elaborating the argument module expression. The need for also quantify over the type set 𝑇 in the result module type comes from the desire to prove a property that if 𝐸 ⊢ mexp : ∃𝑇.𝐸 ′ then tvs(𝐸 ′ ) ⊆ tvs(𝐸) ∪ 𝑇 . The remainder of the rules cover the other constructs of the language, which include Rule 26, for module projection, and Rule 28, for parameterised modules. In the rule for parameterised modules, the side condition 𝑇 ∩ tvs(𝐸) = ∅ expresses that 𝑇 should be chosen sufficiently fresh. Notice in particular that, due to 𝛼-renaming, the judgement 𝐸 ⊢ mty : ∃𝑇.𝐸 ′ does not by itself entail this property. Another important aspect to notice is that both Rule 26 and Rule 36 are implicit about removal of bound type variables that do not occur under the binder, as objects are considered identical up-to removal of superfluous type variables. In Rule 36, for instance, due to shadowing of identifiers, a type variable in the set 𝑇 1 ∪ 𝑇 2 may not necessarily occur in the environment 𝐸 1 + 𝐸 2 .

𝐸 ⊢ mdec : Σ 𝐸 ⊢ { mdec } : Σ (25) 𝐸 ⊢ mexp : ∃𝑇.𝐸 ′ 𝐸 ′ (mid) = 𝐸 ′′ 𝐸 ⊢ mexp . mid : ∃𝑇.𝐸 ′′ (26) 𝐸(mid) = 𝐸 ′ 𝐸 ⊢ mid : ∃∅.𝐸 ′ (27) 𝐸 ⊢ mty : ∃𝑇.𝐸 ′ 𝐸 + {mid ↦ → 𝐸 ′ } ⊢ mexp : Σ 𝑇 ∩ tvs(𝐸) = ∅ 𝐹 = ∀𝑇.(𝐸 ′ , Σ) 𝐸 ⊢ 𝜆mid : mty → mexp : ∃∅.𝐹 (28) 𝐸 ⊢ mexp : ∃𝑇.𝐸 ′ 𝑇 ∩ 𝑇 ′ = ∅ (𝐸 ′′ , ∃𝑇 ′ .𝐸 ′′′ ) ≤ 𝐸(longmid) 𝐸 ′ ≻ 𝐸 ′′ (𝑇 ∪ 𝑇 ′ ) ∩ tvs(𝐸) = ∅ 𝐸 ⊢ longmid ( mexp ) : ∃(𝑇 ∪ 𝑇 ′ ).𝐸 ′′′ (
𝑇 1 ∩ (tvs(𝐸) ∪ 𝑇 2 ) = ∅ 𝐸 ⊢ mdec 1 : ∃𝑇 1 .𝐸 1 𝐸 + 𝐸 1 ⊢ mdec 2 : ∃𝑇 2 .𝐸 2 𝐸 ⊢ mdec 1 mdec 2 : ∃(𝑇 1 ∪ 𝑇 2 ).(𝐸 1 + 𝐸 2 ) (36)
To specify how a module expression mexp is classified by a module type expression mty, a specialised rule can be given:

𝐸 ⊢ mexp : ∃𝑇.𝐸 ′ 𝐸 ⊢ mty : Σ 𝑇 ∩ tvs(𝐸) = ∅ 𝐸 ′ ≻ 𝐸 ′′ 𝐸 ′′ ≤ Σ 𝐸 ⊢ mexp : mty : Σ (37)
We see here that mexp is allowed to declare more identifiers than are specified by mty (expressed using ≻) and that declared identifiers in mexp may be less abstract than specified by mty (expressed using ≤). Formally, this rule is subsumed by the derived form in Equation 5, which turns matching into an application of a constrained identity functor. In the context of constructing libraries and modular applications for Futhark, we have not suffered from the lack of so-called transparent module type matching, for which the resulting module type Σ in Rule 37 needs to be changed to ∃𝑇.𝐸 ′′ . If needed, there is no technical reason for restricting static interpretation to support only opaque matching.

Demonstrating the Elaboration Rules on the Code Example of Figure 3

This section briefly discusses the manner in which the environments shown in Figure 5 were derived by the application of the elaboration rules. The module type MT in Figure 3 We conclude by discussing the rules for module Main, which is defined as the application of the parameterised module H to the module expression {module F = 𝜆X:{val b:i32} → {let f(x:i32)=X.b+x}}. The type of F is derived by Rule 28 to be Σ 𝐹 in a manner similar to the derivation discussed before. Rule 29 then derives the type ∃∅.M 𝑓 for the application of the parameterised module H to the specification {module F=. . .}, and, finally, Rule 32 adds the new binding Main ↦ → M 𝑓 to the ME environment.

STATIC INTERPRETATION

Static interpretation is the process of eliminating modules at compile time by translating modules into a sequence of target language definitions. The interpretation ensures that the target language declarations refer to previous declarations as specified by the source program. In the process, abstract types are eliminated, which results in a specialised program.

Target Language

We assume a denumerably infinite set LSet of labels, ranged over by 𝑙. Target expressions are basically identical to core level expressions with the modification that value identifiers are replaced with labels. For the simple core language that we are considering, target expressions (ex) and target code (𝑐) take the form:

ex ::= 𝑙 | 𝜆𝑙 → ex | ex 1 ex 2 𝑐 ::= val 𝑙 = ex | 𝑐 1 ; 𝑐 2 | 𝜖
The type system for the target language is simple (for the purpose of this paper) and allows inferences among sentences of the forms Γ ⊢ ex : 𝜏 and Γ ⊢ 𝑐 : Γ ′ , which are read: "In the context Γ, the expression ex has type 𝜏 " and "in the context Γ, the target code 𝑐 declares the context Γ ′ ". Contexts Γ map labels to types. The type system for the target

Γ(𝑙) = 𝜏 Γ ⊢ 𝑙 : 𝜏 (38) Γ + {𝑙 ↦ → 𝜏 } ⊢ ex : 𝜏 ′ Γ ⊢ 𝜆𝑙 → ex : 𝜏 → 𝜏 ′ (39) Γ ⊢ ex 1 : 𝜏 ′ → 𝜏 Γ ⊢ ex 2 : 𝜏 ′ Γ ⊢ ex 1 ex 2 : 𝜏 (40) Γ ⊢ 𝑐 1 : Γ 1 Γ + Γ 1 ⊢ 𝑐 2 : Γ 2 Γ ⊢ 𝑐 1 ; 𝑐 2 : Γ 1 + Γ 2 (41) Γ ⊢ ex : 𝜏 Γ ⊢ val 𝑙 = ex : {𝑙 ↦ → 𝜏 } (42) Γ ⊢ 𝜖 : {} (43)
Fig. 9. Type rules for the target language. For the purpose of the presentation, the target language is simple (and standard) and mimics closely the source language with the difference that long identifiers are replaced with labels for referring to previously defined value declarations.

language is presented in Figure 9. Rule 41 is the rule for composing target code. The rules are straightforward (and standard) and we shall not describe them in details here.

Interpretation Objects

In the following, we shall use the term name to refer to either a type variable 𝑡 or a label 𝑙.

We write NSet to refer to the disjoint union of TSet and LSet. Moreover, we use 𝑁 to range over finite subsets of NSet.

An interpretation value environment (𝒱𝐸) maps value identifiers to a label and an associated type. An interpretation environment (ℰ) is a quadruple (TE , 𝒱𝐸, ℳ𝐸, 𝐺) of a type environment, an interpretation value environment, an interpretation module environment, and a module type environment. An interpretation module environment (ℳ𝐸) maps module identifiers to module interpretations. A module interpretation (ℳ) is either an interpretation environment ℰ or a functor closure Φ. A functor closure (Φ) is a triple (ℰ, 𝐹, 𝜆mid → mexp) of an interpretation environment, a parameterised module type, and a representation of a parameterised module expression. Finally, an interpretation target object (∃𝑁.(ℰ, 𝑐)) is a triple of a name set, an interpretation environment, and a target code object.

Interpretation Erasure

For establishing a link between interpretation objects and elaboration objects, we introduce the concept of interpretation erasure. Given an interpretation object 𝑂, we define the interpretation erasure of 𝑂, written 𝑂, as follows:

(TE , 𝒱𝐸, ℳ𝐸, 𝐺) = (TE , 𝒱𝐸, ℳ𝐸, 𝐺) (ℰ, 𝐹, 𝜆mid → mexp) = 𝐹 {vid 𝑖 ↦ → 𝑙 𝑖 : 𝜏 𝑖 } 𝑛 = {vid 𝑖 ↦ → 𝜏 𝑖 } 𝑛 {mid 𝑖 ↦ → ℳ 𝑖 } 𝑛 = {mid 𝑖 ↦ → ℳ 𝑖 } 𝑛 ∃𝑁.(ℰ, 𝑐) = ∃(TSet ∩ 𝑁 ).ℰ
As we shall see shortly, the concept of interpretation erasure makes it straightforward to specify various properties of the relation between static interpretation and elaboration.

Core Language Compilation

Core language expressions and declarations are compiled into target language expressions and declarations, respectively. The rules specifying the compilation are given in Figure 10 and allow inferences among sentences of the forms (1) ℰ ⊢ exp ⇒ ex, 𝜏 and (2) ℰ ⊢ dec ⇒ ∃𝑁.(ℰ ′ , 𝑐). There are two interesting aspects to notice about the rules. First, accesses to long identifiers (i.e., in Rule 44) are compiled into label references. Second, core language value declarations are compiled into a label binding (i.e., Rule 48) for which the label is existentially bound. This existential binding allows for the static interpretation process to control the linking process. The remainder of the rules are straightforward.

Static Interpretation of Higher-Order Modules in Futhark 97:15 The rules track type information and it is straightforward to establish the following property of the compilation:

Compiling Expressions. ℰ ⊢ exp ⇒ ex, 𝜏 ℰ(longvid) = (𝑙, 𝜏 ) ℰ ⊢ longvid ⇒ 𝑙, 𝜏 (44) ℰ + {vid ↦ → (𝑙, 𝜏 )} ⊢ exp ⇒ ex, 𝜏 ′ ℰ ⊢ 𝜆vid → exp ⇒ 𝜆𝑙 → ex, 𝜏 → 𝜏 ′ (45) ℰ ⊢ exp 1 ⇒ ex 1 , 𝜏 → 𝜏 ′ ℰ ⊢ exp 2 ⇒ ex 2 , 𝜏 ℰ ⊢ exp 1 exp 2 ⇒ ex 1 ex 2 , 𝜏 ′ (46) ℰ ⊢ exp ⇒ ex, 𝜏 ℰ ⊢ ty : 𝜏 ℰ ⊢ exp : ty ⇒ ex, 𝜏 (47) Compiling Declarations. ℰ ⊢ dec ⇒ ∃𝑁.(ℰ ′ , 𝑐) ℰ ⊢ exp ⇒ ex, 𝜏 𝑙 ̸ ∈ names(ℰ) ℰ ⊢ val vid = exp ⇒ ∃{𝑙}.{vid ↦ → (𝑙, 𝜏 ), val 𝑙 = ex} (48)
Proposition 5.1. If ℰ ⊢ dec ⇒ ∃𝑁.(ℰ ′ , 𝑐) then ℰ ⊢ dec ⇒ ∃𝑁.(ℰ ′ , 𝑐).

Environment Filtering

Corresponding to the notion of enrichment for elaboration, we introduce a notion of filtering for the purpose of static interpretation, which filters interpretation environments to contain components as specified by an elaboration environment. Filtering is essential to the interpretation rule for applications of parameterised modules and is defined mutual inductively based on the structure of elaboration environments and elaboration module environments.

More formally, the filtering of an interpretation environment ℰ to an elaboration environment 𝐸 results in another interpretation environment ℰ ′ with only elements from ℰ that are also present in 𝐸. The filtering relation is defined by a number of inference rules that allow inferences among sentences of the forms (1) ⊢ ℰ :: 𝐸 ⇒ ℰ ′ , (2) ⊢ 𝒱𝐸 :: VE ⇒ 𝒱𝐸 ′ , (3) ⊢ ℳ𝐸 :: ME ⇒ ℳ𝐸 ′ , and (4) ⊢ ℳ :: 𝑀 ⇒ ℳ ′ . The inference rules for filtering are presented in Figure 11. It is a straightforward exercise to demonstrate that if ⊢ ℰ :: 𝐸 ⇒ ℰ ′ then it holds that ℰ ≻ 𝐸.

Static Interpretation Rules

Static interpretation of the module language is defined by a number of mutually inductive inference rules allowing inferences among sentences of the forms (1) ℰ ⊢ mexp ⇒ Ψ and (2) ℰ ⊢ mdec ⇒ ∃𝑁.(ℰ ′ , 𝑐), which state that in an interpretation environment ℰ, static interpretation of a module expression mexp results in an interpretation target object Ψ, and static interpretation of a module declaration mdec results in an interpretation target object ∃𝑁.(ℰ ′ , 𝑐). The rules for static interpretation are presented in Figure 12. In general, the structure of the rules resembles closely the structure of the elaboration rules for modules with the addition that static interpretation takes care of constructing and composing target code. In doing so, the composition of target code is controled using name binding exactly like type variable binding is used in the elaboration rules for controling the composition of elaboration environments. The only two rules that compose target code are Rule 58, the rule for application of a parameterised module, and Rule 65, the rule for sequential

Environments.

⊢ ℰ :: composition of two module declarations. In Rule 58, environment filtering is used for filtering the argument module to hold only those components specified by the module type object. Notice also that the body of the parameterised module is extracted from the functor closure bound to the module identifier in the environment. Rule 57, on the other hand, takes care of constructing a functor closure object, but it also takes special care that the parameterised module elaborates under appropriate assumptions. The remaining rules are straightforward and follow closely the corresponding elaboration rules.

𝐸 ⇒ ℰ ′ ⊢ 𝒱𝐸 :: VE ⇒ 𝒱𝐸 ′ ⊢ ℳ𝐸 :: ME ⇒ ℳ𝐸 ′ TE ≻ TE ′ ⊢ (TE , 𝒱𝐸, ℳ𝐸, {}) :: (TE ′ , VE , ME , {}) ⇒ (TE ′ , 𝒱𝐸 ′ , ℳ𝐸 ′ , {}) (49) Value Environments. ⊢ 𝒱𝐸 :: VE ⇒ 𝒱𝐸 ′ 𝑚 ≥ 𝑛 ⊢ {vid 𝑖 ↦ → 𝑙 𝑖 : 𝜏 𝑖 } 𝑚 :: {vid 𝑖 ↦ → 𝜏 𝑖 } 𝑛 ⇒ {vid 𝑖 ↦ → 𝑙 𝑖 : 𝜏 𝑖 } 𝑛 (50) Module Environments. ⊢ ℳ𝐸 :: ME ⇒ ℳ𝐸 ′ 𝑚 ≥ 𝑛 ⊢ ℳ 𝑖 :: 𝑀 𝑖 ⇒ ℳ ′ 𝑖 𝑖 = 1..𝑛 ⊢ {mid 𝑖 ↦ → ℳ 𝑖 } 𝑚 :: {mid 𝑖 ↦ → 𝑀 𝑖 } 𝑛 ⇒ {mid 𝑖 ↦ → ℳ ′ 𝑖 } 𝑛 (51) Module Interpretations. ⊢ ℳ :: 𝑀 ⇒ ℳ ′ ℳ = ℰ ⊢ ℰ :: 𝐸 ⇒ ℰ ′ ⊢ ℳ :: 𝐸 ⇒ ℰ ′ (52) Φ = (ℰ, 𝐹 ′ , 𝜆mid → mexp) 𝐹 ′ ≻ 𝐹 ⊢ Φ :: 𝐹 ⇒ (ℰ, 𝐹, 𝜆mid → mexp) (53)

PROPERTIES

Before we can establish a static interpretation type soundness property, we first define a type consistency relation that relates interpretation environments, target language contexts, and substitutions providing concrete types for type variables that are considered abstract by elaboration. Due to the presence of higher-order parameterised modules, we shall make use of a logical relation argument [START_REF] Tait | Intensional interpretations of functionals of finite type[END_REF]], which links the relation itself to the static interpretation. The relation is given by a number of inference rules, which are listed in Figure 13. The rules allow inferences among sentences of the forms (1) With local module declarations, mdec may contain both higher-order module declarations and complex applications of such modules. This corollary thus illustrates a non-trivial property, similar to showing for the simply-typed lambda calculus that if ⊢ 𝑒 : i32 then there exists an integer 𝑑 such that 𝑒 ˓→ * 𝑑. Notice also that, because the target language contains no local bindings, all declared labels in 𝑐 escape to top-level and are described by the resulting context Γ + {𝑙 ↦ → i32}.

𝐸 |= 𝑆 ℰ ◁ Γ, (2) ME |= 𝑆 ℳ𝐸 ◁ Γ, (3) 𝑀 |= 𝑆 ℳ ◁ Γ,
DomVE = Dom𝒱𝐸 ∀𝑥 ∈ DomVE , 𝜏 = VE (𝑥) ∧ (𝑙, 𝜏 ) = 𝒱𝐸(𝑥) ∧ 𝑆(𝜏 ) = Γ(𝑙) VE |= 𝑆 𝒱𝐸 ◁ Γ (68) 𝑀 = 𝐸 ℳ = ℰ 𝐸 |= 𝑆 ℰ ◁ Γ 𝑀 |= 𝑆 ℳ ◁ Γ (69) 𝑀 = ∀𝑇.(𝐸, ∃𝑇 ′ .𝐸 ′ ) ℳ = (ℰ 0 , ∀𝑇.(𝐸, ∃𝑇 ′ .𝐸 ′ ), mid, mexp) (∀ℰ, 𝑆 ′ , ℰ = 𝐸 ∧ Dom 𝑆 ′ = 𝑇 ∧ 𝐸 |= 𝑆∘𝑆 ′ ℰ ◁ Γ =⇒ ∃𝑁 ′ , ℰ ′ , 𝑐, 𝑆 ′′ , ℰ 0 + {mid ↦ → ℰ} ⊢ mexp ⇒ ∃𝑁 ′ .(ℰ ′ , 𝑐) ∧ ℰ ′ = 𝐸 ′ ∧ Dom 𝑆 ′′ = 𝑇 ′ ∧ 𝑁 ′ ⊇ 𝑇 ′ ∧ 𝐸 ′ |= 𝑆∘𝑆 ′ ∘𝑆 ′′ ℰ ′ ◁ Γ ′ ∧ Γ ⊢ 𝑐 : Γ ′ ) 𝑀 |= 𝑆 ℳ ◁ Γ (70)

TYPE INFERENCE FOR THE MODULE LANGUAGE

We shall not here give a type inference algorithm for the module language but instead mention that type inference for the language becomes straightforward (i.e., syntax directed) if elaborated module types are what is called type explicit [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF]].

The notion of type explication is mutually inductively defined as follows. A module type Σ = ∃𝑇.𝐸 is type explicit if 𝐸 is type explicit and for all 𝑡 ∈ 𝑇 , there exists a longtid such that 𝐸(longtid) = 𝑡. A module type Σ = ∃𝑇.𝐹 is type explicit if 𝑇 = ∅ and 𝐹 is type explicit. A parameterised module type 𝐹 = ∀𝑇.(𝐸, Σ) is type explicit if ∃𝑇.𝐸 is type explicit. An environment 𝐸 is type explicit if all module types Σ in 𝐸 are type explicit.

The importance of type explication becomes apparent when trying to match a concrete environment 𝐸 ′ against a module type Σ = ∃𝑇.𝐸, which is what is required in the rule for application of parameterised modules. If Σ is type explicit, it becomes straightforward to decide whether there exists a substitution 𝑆 such that Dom 𝑆 = 𝑇 and 𝑆(𝐸 ′ ) ≻ 𝐸.

The following proposition states that our language for specifying module types generates type explicit module types:

Proposition 7.1. (Type Explicit Module Types). If 𝐸 ⊢ mty : Σ or 𝐸 ⊢ spec : Σ then Σ is type explicit if 𝐸 is type explicit.
There are a number of good reasons for extending the language for expressing module types [START_REF] Ramsey | An Expressive Language of Signatures[END_REF] to avoid unnecessary duplication of module type specification code. As long as such extensions come with guarantees that every expressible module type is type explicit, type inference for the module language will be straightforward.

POLYMORPHISM AND HIGHER-ORDER FUNCTIONS

In this section, we show how certain classes of polymorphic functions and polymorphic types at the source level can be treated as derived forms of parameterised modules and how certain instantiations can be treated as parameterised module applications.

Polymorphic Functions

Consider the following Futhark declaration of a function polymorphic in the types t and s:

let imap 't 's (f: (i32,t)→s) (a:[]t) : []s = map f (zip (iota (length a)) a)
This declaration can be treated as a special derived form of a declaration of a parameterised module:

module Imap (X: {type t type s val f:

(i32,t)→s}) = { open X let imap (a:[]t) : []s = map f (zip (iota (length a)) a) }
Now, for obtaining an instantiation of the module, it is possible to instantiate the "polymorphic function" imap to concrete arguments as follows: let main () = imap (𝜆(i,x)→i+x) [1,2,3] This code can then be translated into the following modularised code:

local module Imap_23 = Imap({type t=i32 type s=i32 let f (i,x) = i+x}) in { let main () = Imap_23.imap [1,2,3] }
This special short-hand for instantiating "polymorphic functions" is possible only in certain cases. For simplicity, it can be required that type parameter instantiations can be determined directly from the calling context and that the free variables of the passed arguments (e.g., the free variables in 𝜆(i,x)→i+x) are all bound outside the containing module declaration. With a little more bookkeeping, it is possible to relax this requirement by implementing a version of lambda lifting [START_REF] Johnsson | Lambda Lifting: Transforming Programs to Recursive Equations[END_REF]] that adds additional parameters to the declared function. Finally, with this approach, it is a requirement that the declared polymorphic functions do not themselves return functions; the scheme can support a number of higher-order functions but not first-class functions in general.

Polymorphic Types

Consider the following Futhark declaration of a "polymorphic type": Although this technique has some limitations compared to supporting polymorphism at the core language level, the mechanism is simple and can, for certain application domains, relieve the language implementor from considering polymorphism at the core language level.

In practice, Futhark is relying on separate passes for eliminating core language polymorphism and higher-order functions [Hovgaard 2018]. These passes both occur after static interpretation of modules and do not interfere with static interpretation. The separation of the passes for core language monomorphication and core language elimination of higherorder functions from static interpretation allows for supporting a richer set of polymorphic higher-order functions.

FORMALISING THE DEVELOPMENT IN COQ

We have formalised, in the Coq proof assistant, essential parts of the definitions given in this paper along with the proof of static interpretation normalisation. In the course of the development, we have used additional axioms of functional extensionality and proof irrelevance for propositions. Also, for the development of nominal techniques, we assume a countably infinite set of variable names.

We have taken an extrinsic approach [START_REF] Benton | Strongly Typed Term Representations in Coq[END_REF], as opposed to an intrinsic one, to the representation of the core language, the module language, and the target language, which keeps our implementation close to the approach presented in the paper. The extrinsic encoding has an advantage of being more suitable for code extraction to obtain a certified implementation. That is, we have implemented the abstract syntax as simple inductive data types and given separate inductive definitions for relations such as elaboration, typing, and so on. The semantic objects of Figure 4 have been implemented as mutually defined inductive types using Coq's with clause. The same approach is used for definitions of relations on environments. As described in Section 4, semantic objects are represented using finite maps and sets and indeed, the implementation makes use of Coq's standard library implementations of such objects. Specifically, we use the FMapList and FSetList implementations of the FMap and FSet interfaces, respectively. Both FMapList and FSetList make use of the list data type together with a property that the list is ordered according to a strict order on the underlying data structure. The strict order for the underlying list allows us to prove an extensionality property for environments and sets (assuming proof irrelevance). That is, for any two environments 𝐸 1 and 𝐸 2 we have (∀𝑘, 𝐸 1 (𝑘) = 𝐸 2 (𝑘)) → 𝐸 1 = 𝐸 2 . The equal sign = refers to the Coq propositional equality, which means that we can use all the standard rewriting machinery instead of using setoid equality.

Unfortunately, we cannot use the definition of environments from the standard library to define semantic objects such as MEnv because of Coq's limitation that using type constructors for the environments from the standard library will violate Coq's strict positivity check for inductive definitions. To overcome this complication, we introduce an isomorphic pair-ofvectors representation of environments, where the first vector is an ordered vector of keys and the second vector is a vector of values. Separating keys and values in different vectors allows us to define semantic objects in a way acceptable for Coq's strict-positivity checker. The idea of using an isomorphic representation is very similar to Wadler's notion of views [START_REF] Wadler | Views: A Way for Pattern Matching to Cohabit with Data Abstraction[END_REF]]. We can see the two representations of environments as two views associated with the abstract "type" of environments, which corresponds to a module specifying operations on and properties of environments. Instead of defining all operations on the second representation of environments, we use Coq's coercion mechanism to insert coercion functions automatically, given by the isomorphism between the two representations. Our Coq development shows that it is sufficient to use a few properties of the isomorphism to transfer proofs of the properties from one representation to the other.

In order to theorems by induction over the structure of semantic objects, or relations containing mutual definitions, Coq's Scheme command is used to generate suitable induction principles. For some of the definitions, such as those for semantic objects and interpretation environments, the generated induction principles are not sufficiently strong, which is caused by the presence of nested inductive types; some constructors take environments as parameters, and the environments, being essentially lists, make the whole definition a nested inductive definition. For each of these cases, a suitable induction principle is defined manually, following essentially the same approach as in Section 3.8 of [START_REF] Chlipala | Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant[END_REF]].

For proof automation, we make use of the crush tactic from [START_REF] Chlipala | Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant[END_REF]] and some tactics from [START_REF] Pierce | Software Foundations[END_REF]. The structure of most of the proofs are kept explicit, though, using automation to resolve only the most tedious parts of the proofs.

The proof of static interpretation normalisation is carried out essentially using the same logical relation argument as presented in Figure 13. The logical relation is implemented as a fixpoint rather than as an inductive relation. The reason for this representation is essential. If the relation was defined as an inductive predicate, the definition would not pass the strict positivity constraint for inductive definitions in Coq. From the definition of our logical relation, it is straightforward to establish that the relation is well-formed because it is decreasing structurally in its left argument. For this reason, it can be expressed as a fixpoint definition, using also Coq's anonymous fix-construct, corresponding to the nested structure of the semantic objects. Unfortunately, we cannot keep our environment representation completely abstract, since we define the logical relation recursively on the structure of environments. Restrictions on fixpoint definitions in Coq require us to use a nested fixpoint on underlying structures in the definition of environments. Again, we use a pair-of-vectors view to define a corresponding nested fixpoint in the definition of the consistency relation of Figure 13.

We have kept the Coq development close to the representation in the paper. However, the filtering relation of Figure 11 does not define a filtering algorithm directly but serves as a specification for a filtering algorithm. In the proof of normalisation of static interpretation, we have to show the existence of a filtered environment. Due to the limitations of Coq's fixpoint constructs, we have defined a filtering algorithm as an inductively defined relation. We consider it future work to investigate the use of general recursion in Coq for filtering, which would be useful for applying code extraction to obtain a certified static interpretation implementation. We believe it to be a reasonable approach to separate the relational "declarative" definitions from definitions that compute for code extraction. One can then establish a correspondence between the relational and functional representations to show soundness of the implementation.

We are using a nominal approach [START_REF] Gabbay | A New Approach to Abstract Syntax with Variable Binding[END_REF][START_REF] Pitts | Nominal Sets: Names and Symmetry in Computer Science[END_REF] to define notions of freshness, fresh name generation, and 𝛼-equivalence relations. The approach gives us a uniform structuring principle to deal with variables in various data-structures involved in the formalisation. Since there is no standard package in the Coq distribution implementing nominal techniques (the only available work is Brian Aydemir et al.'s Nominal Reasoning Techniques in Coq [Aydemir et al. 2007], but it is designed only for single variable bindings), we have developed our own implementation covering generalised binding structures such as bindings over sets of variables.

One example of the application of nominal techniques is the condition 𝑙 ̸ ∈ 𝑛𝑎𝑚𝑒𝑠(ℰ) (Rule 48, Figure 10). We define a nominal set of interpretation environments with labels as atoms. Then, the corresponding condition in Rule 48 can be expressed in terms of freshness with the requirement 𝑙 # ℰ (𝑙 is fresh for ℰ). In the proofs, we use the fact that set of atoms is countably infinite to generate fresh (with respect to the appropriate context) labels.

The properties as they are described by propositions and theorems in the paper have not all been completely formalised with proper name abstractions. However, with the developed approach, we believe it is possible to complete the development. Our work-in-progress development contains further examples of the applications of nominal techniques. We use a freshness relation to define conditions involving disjointness of bound variables in such rules as Rule 23 (Figure 7). Notions of 𝛼-equivalence is defined in a general way as in Ranald Clouston's work on Generalised Name Abstraction for Nominal Sets [START_REF] Clouston | Generalised Name Abstraction for Nominal Sets[END_REF]]. We explicitly add 𝛼-conversion in the elaboration rules for functor application (Rule 29) and for the sequence of declarations (Rule 36). We provide examples illustrating when the addition of 𝛼-conversion is important for the elaboration of certain module expressions in the completely formal setting. The Coq development is available as an ACM DL artifact and from the Github repository https://github.com/diku-dk/futhark-icfp18.

FUTHARK LIBRARIES AND APPLICATIONS

We have already in Section 2 presented a Futhark library that makes use of higher-order modules. Steadily, a Basis Library for Futhark emerges. Currently, the library includes modules for operating on various kinds and sizes of numeric values, such as integral numbers, floating point numbers, complex numbers, and rational numbers. Other modules then exist that are parametric over the particular numeric instance. Such modules include a module for linear algebra routines. Other modules provide generic parallel routines for radix-based sorting, sparse matrices, and generation of Sobol sequences [START_REF] Joe | Remark on Algorithm 659: Implementing Sobol's Quasirandom Sequence Generator[END_REF].

At application level, a number of programs have been written that make extensive use of the Futhark module language and for which it is essential that modules are eliminated completely at compile time. One example is an implementation of several variants of Conway's Game of Life, which differ in both rule sets and visualisation algorithms, but utilise the module system to obtain code reuse. The Game of Life is a rank-1 stencil on a two-dimensional grid, with a rule for how one cell changes its value from one (discrete) step to the next based on its current value and those of its neighbours. In Conway's formulation, each cell can be in one of two states (living or dead), but variations can have more states. We can describe the generic concept of a rule set as a module type: A rule set consists primarily of a cell type and a step function. To compute the value of cell 𝑐 in step 𝑖 + 1, the step function is called with the current value of 𝑐 and the sum of all cells within the surrounding 3 × 3 neighbourhood (including 𝑐). This sum is computed by transforming each cell to an integer via value, then multiplying each cell with its corresponding weight in the weights array. An implementation of a full Game of Life can be described as follows:

module type game_of_life = { type cell val step: [][]cell → [][]cell }
The step function runs one evolution of the Game of Life. We can define a parametric module that, given an implementation of the rules module type, gives us an implementation of the game_of_life signature: This setup lets us run instances of the Game of Life, but we would also like to be able to visualise them on the screen. For visualisation, we define module types that describe both rule sets and a mechanism for getting a colour from a cell: The render function accepts an array of cells and produces an array of ARGB colour values encoded as integers (making use of the argb module from the Futhark Basis Library.) We also require that cells can be initialised from booleans, and transformed back into booleans, although these two functions need not be inverses of each other. This facility is useful for random initialisation; we shall see another use of it in Section 10.1.

We can define a parametric module that operates on modules of the above module types: The resulting visualisations are shown on Figures 14a and14c.

Multi-Parameter Parametric Modules

We can build more advanced visualisations on top of the above. For example, let us define a visualisation where cells that switch from being "alive" to "dead" gradually fade to the dead colour, instead of switching immediately. We can implement this feature elegantly as a parametric module, without interfering with any of the previous definitions. First, we define a module type for specifying the behaviour when a cell dies: module type fading = { val dying_speed: f32 } When a cell dies, it will gradually fade away from its last colour as a living cell, over a number of simulation steps controlled by dying_speed. We will treat a cell as dead when As static interpretation performs all module applications at compile-time, followed by vigorous function call inlining, the potential overheads of this high degree of decomposition are negated. Performance is thus equivalent to hand-written specialised implementations of our four Game of Life variants.

RELATED WORK

Related work fall into a number of different categories. As mentioned in the introduction, the concept of static interpretation of modules is not new and have been applied earlier in the context of the MLKit Standard ML compiler [START_REF] Elsman | Static Interpretation of Modules[END_REF]]. The concept of specialising modules (or Ada packages) is also not new and is applied for C++ templates [Veldhuizen 1999], for Ada packages, and also for the MLton compiler [START_REF] Fluet | Contification Using Dominators[END_REF]. Compared to this earlier work, the present work is extended to higher-order modules and the termination argument for static interpretation is more involved, due to the logical-relations argument.

Also related to this work is previous work on elaboration of ML modules. Aiming at typing an increasing class of higher-order modular programs, [START_REF] Leroy | Applicative Functors and Fully Transparent Higher-order Modules[END_REF] presents a distinction between applicative and generative higher-order modules, which provides the foundation for the implementation of higher-order modules in OCaml. Applicative higher-order modules allow for a refined theory of type equality, compared to the traditional generative module semantics provided by [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF], by identifying applications of applicative higherorder modules when applied to identical arguments. Later developments, such as [START_REF] Crary | Modules, Abstraction, and Parametric Polymorphism[END_REF]], model applicative functors using a notion of totality (i.e., pure functions). The present development considers generative higher-order modules only, which are still rich enough to encode most modular patterns including modular type classes using fully transparent modules [START_REF] Dreyer | Modular Type Classes[END_REF]] and modular implicits [START_REF] White | Modular implicits[END_REF]. Leroy also provides a modular modules implementation of a higher-order module system [START_REF] Leroy | A Modular Module System[END_REF]] and shows that this system can be applied to different core languages. He also briefly discusses compiling away modules in the context of first-order modules-related to the compilation of Ada packages, C++ templates, and the previous work on static interpretation of modules [START_REF] Elsman | Static Interpretation of Modules[END_REF]. By supporting elimination of modules entirely at compile time, a modular module system will apply to a richer class of languages, including languages for which compilation does not provide a natural low-cost grouping strategy, which, among other domains, include domain-specific languages for data-parallel architectures, such as FPGAs and GPGPUs. This class of related work also includes the work by [START_REF] Russo | Non-dependent Types for Standard ML Modules[END_REF], which also, as in the present work, use universal and existential quantification as essential objects in the elaboration rules of the module language. In particular, modeling the generation of fresh type variables (type names in Standard ML) as existential quantification leads to an important scalable technique for proving properties about the language. Other related work in this area include the body of work on obtaining a type-theoretic account of ML modules and, in particular, of higher-order modules [START_REF] Harper | A Type-Theoretic Approach to Higher-Order Modules with Sharing[END_REF]. Because a module system can be understood as a limited dependently typed language, researchers has early on aimed at securing a phase-distinction between the static and dynamic aspects of modules [START_REF] Harper | Higher-order Modules and the Phase Distinction[END_REF]]. Compared to our work, we go a step further and show that also the dynamic aspects of a higher-order module language can be executed (and the process expected to terminate) at compile time. The classical phase distinction is, however, still of absolute importance for a module language (to be distinguished from C++ templates) as it allows for programmers to design and reason about components in isolation. Related to this aspect and complementary to our work, [START_REF] Crary | Modules, Abstraction, and Parametric Polymorphism[END_REF] demonstrates a module system abstraction theorem, which says that an application context cannot distinguish two logically equivalent modules. This body of work also includes the work on elaborating the Standard ML module language into an internal module language [START_REF] Harper | Proof, Language, and Interaction[END_REF]. Recently this work has led to a compilation of higher-order modules into F 𝜔 , the higher-order polymorphic lambda calculus [START_REF] Rossberg | F-ing modules[END_REF]]. Compared to our work, which eliminates all module language constructs at compile time, [START_REF] Rossberg | F-ing modules[END_REF] make no distinction between core language and module language constructs in the target code. Moreover, the more complicated mechanisms supported by the language, for interaction between the module language and the core language, makes it difficult to argue that a compiler can effectively eliminate all module language constructs at compile time, by somehow partially evaluate the generated F 𝜔 expressions. The same distinction holds between the present work and earlier work on compiling higher-order modules into an F 𝜔 -like language with existential types [START_REF] Shao | Transparent Modules with Fully Syntatic Signatures[END_REF]], which is the basis for compiling modules in the SML/NJ compiler.

Other work on modules include work on understanding how the module language may interact with mechanisms for separate compilation and smart recompilation [START_REF] Shao | Smartest Recompilation[END_REF]. This body of work includes the work by [START_REF] Swasey | A Separate Compilation Extension to Standard ML[END_REF] on extending the Standard ML language with a mechanism for truly separate compilation. Contrary to our work, the work by [START_REF] Swasey | A Separate Compilation Extension to Standard ML[END_REF] allows for components to be compiled and understood in isolation and yet linked safely with the possibility that a component matching a particular module type can be replaced with another module matching the module type, without the need for recompiling the entire application. The earlier work on static interpretation [START_REF] Elsman | Static Interpretation of Modules[END_REF]] allows for modules, and even specialised version of parameterised modules, to be compiled separately but with the additional feature that implementation choices for exported identifiers would leak module boundaries and allow for special kinds of optimisations (including inlining of small functions) to be performed across module boundaries. The present work does not attempt at providing any mechanism for separate compilation, although a smart-recompilation framework could be useful, in particular for decreasing compile times for very large programs. At present, however, Futhark compile times are manageable and a better understanding of how to track whether a GPU kernel changes upon changes of source code is needed for constructing a reliable smart-recompilation framework for Futhark.

Also related to our work are alternative approaches at providing mechanised meta-theories for module languages, including the work by [START_REF] Rossberg | F-ing modules[END_REF], which comes with a Coq implementation of the work, but also the earlier work on using Twelf to provide a mechanised meta theory for Standard ML [Lee et al. 2007]. Compared to our work, however, none of these approaches attempts at eliminating modules at compile time. Another body of work related to mechanising the meta-theory of ML is the work on CakeML [START_REF] Kiam Tan | A New Verified Compiler Backend for CakeML[END_REF], which, however, supports only non-parameterised modules.

Another body of related work includes other mechanisms for removing abstractions at compile time including techniques for embedded domain specific languages (EDSLs), as discussed in the introduction, quoted domain specific languages [START_REF] Najd | Everything Old is New Again: Quoted Domain-specific Languages[END_REF], techniques for multi-stage programming, such as that by [START_REF] Taha | MetaML and multi-stage programming with explicit annotations[END_REF], and just-in-time compilation techniques in general. Being able to construct programs, in a type-safe way, using meta-level computations (including the application of partial evaluation techniques) is a powerful concept. Static interpretation, however, allows for the user to use a module system to construct and apply powerful abstractions, yet knowing that the mechanism terminates and that the use of abstractions does not introduce any overhead. EDSL approaches leverage a host-language's abstraction mechanisms and its language features for constructing and composing programs at runtime. Such approaches provide the programmer with very powerful tooling. However, when, for instance, the source language is used as a target language for another high-level language, both the host-language compiler and its runtime system is required to be part of the compiler pipeline. In such cases, a simpler approach, based on a self-contained language, may be preferable.

Also related to this work is Reynolds work on applying functor categories to compile the lambda-calculus part of an Algol-like language away at compile time, leaving only target code that is purely imperative [START_REF] Reynolds | Using Functor Categories to Generate Intermediate Code[END_REF]]. Unlike our approach, it is unclear how this approach applies to abstract types and a larger class of (also non-imperative) core languages.

As a final body of related work is the work on using logical relations for expressing normalisation and termination properties for the simply-typed lambda calculus and System F, which has been the inspiring work for establishing the property of termination for static interpretation. This body of work includes the seminal work by [START_REF] Tait | Intensional interpretations of functionals of finite type[END_REF] and Girard [1971] on establishing the basic proof technique based on logical relations, including various adaptations of the technique [START_REF] Donnelly | A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. Electron[END_REF], and applications of the technique in proof assistants [START_REF] Abel | Normalization for the Simply-Typed Lambda-Calculus in Twelf[END_REF]].

CONCLUSION AND FUTURE WORK

We have described a technique for integrating a higher-order module language with a compiler for the data-parallel functional language Futhark. The technique, called static interpretation, eliminates entirely the module language at compile time and it can be established formally that the process terminates and yields well-typed target programs. We have shown, using a number of Futhark examples, that the structuring mechanism provided by the higher-order module language is a useful mechanism for modularity and reuse and that it, also in practice, leads to no overhead in the generated code. The formal development has been implemented and proved in Coq using a novel approach of working with semantic objects such as products, sets, and finite maps. The Coq implementation matches closely the structure of the development in both the paper and in the Haskell implementation for the Futhark language.

There are a number of possibilities for future work. First, it would be interesting to investigate whether it will be possible, perhaps in some limited fashion, to integrate modular type classes [START_REF] Dreyer | Modular Type Classes[END_REF] or some of the modular implicits techniques [START_REF] White | Modular implicits[END_REF] with the module language and still have static interpretation eliminate all module language constructs at compile time. Second, we expect that the work on establishing a standard basis library for Futhark will lead to the desire to extend the language for expressing module types using some of the suggestions given by [START_REF] Ramsey | An Expressive Language of Signatures[END_REF]. Third, Futhark is also used as a target language for compilation of high-level array languages, such as APL [START_REF] Iverson | A Programming Language[END_REF]], into efficient GPU code [START_REF] Annenkov | Certified Compilation of Financial Contracts[END_REF][START_REF] Elsman | Compiling a Subset of APL Into a Typed Intermediate Language[END_REF]Henriksen et al. 2016a]. Using the new module language features, a more natural encapsulation of target language constructs is now possible, which will ease maintainability and simplify high-level code generation phases. Finally, an interesting project would be to extend the Coq implementation to make it possible to extract a certified "modular modules" implementation [START_REF] Leroy | A Modular Module System[END_REF]] for use with other domain specific languages than Futhark.

  Fig.1. Grammar for the module language excluding derived forms.

  ty ::= longtid | ty 1 → ty 2 exp ::= longvid | 𝜆vid → exp | exp 1 exp 2 | exp : ty dec ::= val vid = exp

  ) module 𝑋 : mty = mexp mdec =⇒ module 𝑋 = mexp : mty (6) module 𝐹 ( 𝑋 : mty 0 ) : mty = mexp mdec =⇒ module 𝐹 ( 𝑋 : mty 0 ) = mexp : mty(7) type tid = ty spec =⇒ include ({ type tid } with tid = ty)(8)

Fig. 2 .

 2 Fig. 2. Implementing segmented scan based on scan at library level in Futhark.

Fig. 3 .

 3 Fig. 3. A (contrived) example demonstrating static interpretation in action. The program on the left is turned into the three snippets of declarations on the right.

Fig. 4 .

 4 Fig. 4. Module language semantic objects. Parameterised module types (𝐹 ) and module types (Σ) are parameterised over finite sets of type variables (written Fin(TSet)), ranged over by 𝑇 .

Fig. 5 .

 5 Fig. 5. The semantic objects at outermost (program) level for the code example in Figure 3.

Fig. 8 .

 8 Fig. 8. Elaboration rules for module language expressions and declarations.

  is declared to export a parameterised module F. The type of F is declared in the code to be X:{val b:i32} → {val f:i32→i32}, and is derived by Rule 18 to be Σ 𝐹 = ∀∅.( ({}, {b ↦ → i32}, {}, {}), ∃∅.M 𝑓 ), where M 𝑓 = ({}, {f ↦ → (i32 → i32)}, {}, {}). Elaboration Rule 21 then extends the ME environment with the binding F ↦ → Σ 𝐹 and Rule 34 extends the 𝐺 environment with the binding MT ↦ → Σ 𝑀 𝑇 , where Σ 𝑀 𝑇 = ∃∅.({}, {}, {F ↦ → Σ 𝐹 }, {}). We discuss next the elaboration rules for module H = 𝜆M:MT → M.F {let b=8}. Rule 28 (i) deduces MT:Σ 𝑀 𝑇 (by a lookup in 𝐺), (ii) adds the binding M ↦ → Σ 𝑀 𝑇 to the ME environment, and (iii) computes the type of the application M.F {let b=8}. The latter step uses Rule 29 to derive the type ∃∅.({}, {f ↦ → (i32 → i32)}, {}, {}). It follows that Rule 28 computes the parameterised module's type to be Σ 𝐻 = ∀∅.(({}, {}, {F → Σ 𝐹 }, {}), ∃∅.M 𝑓 ), and Rule 32 adds the new binding H ↦ → Σ 𝐻 to the ME environment.

Fig. 10 .

 10 Fig. 10. Core language compilation.

Fig. 11 .

 11 Fig. 11. Filtering relation specifying how an interpretation environment can be constrained by an elaboration environment to form a restricted interpretation environment.

Fig. 13 .

 13 Fig. 13. Type consistency logical relation.

  type pair 't 's = (t,[]s) This type declaration can be translated into the following module declaration: module Pair (X : {type t type s}) = open X type pair = (t,[]s) } For obtaining an instantiation of the module, it is possible to instantiate the "polymorphic type" pair to concrete arguments as follows: type y = pair i32 bool This code can be translated into the following module-level declaration: local module Pair_33 = Pair({type t=i32 type s=bool}) in { type y = Pair_33.pair }

  module type rules = { type cell val step: cell → i32 → cell val value: cell → i32 val weights: [][]i32 }

  2 module gen_life(R: rules): game_of_life with cell = R.cell = { type cell = R.cell let all_neighbour_sums(world: [][]cell): [][]i32 = ... let step (world: [][]cell): [][]cell = let all_sums = all_neighbour_sums world in map2 (map2 R.step) world all_sums }

  module type vis_rules = { include rules val colour: cell → argb.colour val init: bool → cell val uninit: cell → bool } module type vis_game_of_life = { include game_of_life val render: [][]cell → [][]argb.colour }

  module gen_life_vis(R: vis_rules) : (vis_game_of_life with cell = R.cell) = { open (gen_life R) let render (world: [][]cell): [][]argb.colour = map (map R.colour) world } Using the above infrastructure, we can now define an implementation of the Game of Life: module conway_rules: vis_rules with cell = bool = { type cell = bool let step (alive: cell) (neighbours: i32) = neighbours >= 2 && (neighbours == 3 || (alive && neighbours < 4)) let value (b: cell) = if b then 1 else 0 val weights = [[1,1,1], [1,0,1], [1,1,1]] let init (b: bool) = b let uninit (c: cell) = c let colour (b: cell) = if b then argb.black else argb.white } module conway = gen_life_vis conway_rules We can equally well define a more complex four-state Game of Life variant: module quad_rules: vis_rules = { type cell = i8 let step (_c: cell) (neighbours: i32): i8 = let t in t[neighbours] let value (c: cell) = i32 c val weights = [[1,1,1], [1,1,1], [1,1,1]] let init (b: bool) = if b then 0 else 1 let uninit (c: cell) = c != 1 let colour (c: cell) = let colours = [argb.green, argb.black, argb.red, argb.blue] in colours[i32 c] } module quad = gen_life_vis quad_rules

  mty 2 : ∃𝑇 ′ .𝑀 𝐸 ⊢ mid : mty 1 → mty 2 : ∀𝑇.(𝐸 ′ , ∃𝑇 ′ .𝑀 ) (18)

	Module Specifications.	𝐸 ⊢ spec : ∃𝑇.𝐸 ′
	𝐸 ⊢ type tid : ∃{t}.{tid ↦ → t} (19)	𝐸 ⊢ ty : 𝜏 𝐸 ⊢ val vid : ty : ∃∅.{vid ↦ → 𝜏 }	(20)

𝐸 ⊢ mty : ∃𝑇.𝑀 𝐸 ⊢ module mid : mty : ∃𝑇.{mid ↦ → 𝑀 } (21) 𝐸 ⊢ mty : ∃𝑇.𝐸 ′ 𝐸 ⊢ include mty : ∃𝑇.𝐸 ′ (22)

  29)

	Module Declarations.		𝐸 ⊢ mdec : ∃𝑇.𝐸 ′
	mdec = dec 𝐸 ⊢ mdec : ∃∅.𝐸 ′ 𝐸 ⊢ dec : 𝐸 ′	(30)	𝐸 ⊢ ty : 𝜏 𝐸 ⊢ type tid = ty : ∃∅.{tid ↦ → 𝜏 }	(31)

𝐸 ⊢ mexp : ∃𝑇.𝑀 𝐸 ⊢ module mid = mexp : ∃𝑇.{mid ↦ → 𝑀 } (32) 𝐸 ⊢ mexp : Σ 𝐸 ⊢ open mexp : Σ (33) 𝐸 ⊢ mty : Σ 𝐸 ⊢ module type mtid = mty : ∃∅.{mtid ↦ → Σ} (34) 𝐸 ⊢ 𝜖 : ∃∅.{} (35)

  and (4) VE |= 𝑆 𝒱𝐸 ◁ Γ. An essential property of the rules is that they are decreasing, structurally, in their left argument and therefore define a wellformed inductive relation. The two most interesting rules are Rule 68, which relates variables in elaboration and static interpretation environments with labels in target environments, and Rule 70, which relates parameterised modules in elaboration and static interpretation environments through static interpretation from appropriately related environments to resulting appropriately related results.Based on the established consistency relation, we can now state a general property establishing (1) that static interpretation is possible and terminates for all elaborating programs and (2) that generated target programs are appropriately typed. ℰ = (TE , 𝒱𝐸, ℳ𝐸, 𝐺) VE |= 𝑆 𝒱𝐸 ◁ Γ ME |= 𝑆 ℳ𝐸 ◁ Γ (TE , VE , ME , 𝐺) |= 𝑆 ℰ ◁ Γ (66) DomME = Domℳ𝐸 ∀mid ∈ DomME , ME (mid) |= 𝑆 ℳ𝐸(mid) ◁ Γ ME |= 𝑆 ℳ𝐸 ◁ Γ (67)

Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 97. Publication date: September 2018.

scan ⊙ e [a 1 , . . ., a𝑛] results in the array [e⊙a 1 ,...,e⊙a 1 ⊙ . . . ⊙a𝑛], where ⊙ is a binary associative operator with neutral element e. Segmented scan[START_REF] Blelloch | Scans as Primitive Parallel Operations[END_REF][START_REF] Guy | Vector models for data-parallel computing[END_REF] receives as extra argument a flag array, which records the start of a new segment with a one and zero otherwise, and results in a (flat) array obtained by applying scan on each segment of the input array.Proc. ACM Program. Lang., Vol.

2, No. ICFP, Article 97. Publication date: September 2018.

The function map2 maps over two arrays and invokes a function of two parameters, as zipWith of Haskell. Proc. ACM Program. Lang., Vol. 2, No. ICFP, Article 97. Publication date: September 2018.

ACKNOWLEDGMENTS

This research has been partially supported by the Danish Strategic Research Council, Program Committee for Strategic Growth Technologies, for the research center "HIPERFIT: Functional High Performance Computing for Financial Information Technology" (http: //hiperfit.dk) under contract number 10-092299. Any opinions, findings, and conclusions or

Module Expressions

Each cell is now represented as a triple of some underlying cell, the colour of the cell when it was last alive, and for how long it has been dead. Notice that the fading_life parametric module is curried. We can partially apply it to a module implementing the fading type to obtain another parametric module:


Yoann Brouard
email: yoann.brouard@univ-tours.fr

Naima Belayachi

Mohan Ranganathan

Dashnor Hoxha

Stéphane Méo

Experimental Assessment of Hygrothermal properties of clay -Sunflower (Helianthus annuus) and Rape Straw (Brassica napus) Bio-Composites

Keywords: Agricultural byproducts, clay plaster, lightweight crude earth, sunflower, rape straw, MBV

The purpose of this investigation is the experimental characterization of the hygric and thermal properties of four clay/vegetable aggregates mixtures. In order to evaluate the hygrothermal behavior of these biocomposites based on different aggregates, moisture buffer value, sorption/desorption isotherm and thermal conductivity were investigated here. This work is carried out in the framework of the BIOCOMP project which aims to develop those locally produced biocomposites to be used as building's interior insulating plasters. This, to offer refurbishment solutions for vernacular buildings in Touraine, Center of France. Sunflower stem and rape straw are considered as agricultural byproducts aggregates whereas local clay is used as binder. In this study, the samples were prepared with the following vegetables: rape straw, sunflower bark, sunflower pith and a mix of sunflower pith and bark. For a same binder:aggregates and water;binder weight ratio, we obtained samples with different densities and different properties depending on the aggregates. The hygric and thermal performances of those mixtures make them competitive in comparison to hemp-lime concrete and could therefore offer a wider variety of refurbishment solutions having a low embodied energy.

INTRODUCTION

Implementation of ambitious actions towards the global warming threats beginning to emerge in the building and construction's sector. This appears to be relevant when we consider that this sector is responsible of 1/3 of global greenhouse gases emissions [International Energy Agency 2013]. To reach the "below 2°C" global warming pathway, a Global alliance have been created during the 21 st Conference Of Parties in Paris in December 2015. One of its main objectives is reaching a 50% reduction of greenhouse gases in the building sector by 2050. In France, a focus has been made on the refurbishment needs in a strategic energy transition plan, with the very ambitious target of 500,000 buildings renovations per annum. In this plan, other ambitious quantified guidelines of 50% greenhouse gases reduction by 2030 and 87% reduction by 2050 have been stated. To help meeting those objectives, low carbon construction processes are encouraged by public project owners. A low carbon building label that will prefigure the next public regulation has been implemented in France in 2016 as a pilot phase. It recommends among others, carbon storing materials and encourage circular economy. Consequently, build and renovate with biobased materials having undergone little transformation like crude earth and vegetable aggregates are thus an environmentally appropriate approach. Those materials should now demonstrate their interest in terms of performances and durability. That is the purpose of the work being held in the biocomp project with partnerships involving local communities, group of farmers, bioconstruction masons and two universities: Polytech Tours and Polytech Orléans. Clay/plant aggregates and fibers started to be investigated lately [START_REF] Laborel-Préneron | Plant Aggregates and Fibers in Earth Construction Materials: A Review[END_REF]] but few studies can be found concerning earth plasters [Navarro 2015]. For many of those studies, vegetables are considered as reinforcement for earthen materials to avoid shrinkage. In the biocomp project, crude earth is used to bind the aggregates in small quantities in order to reach low density mixes (200 to 800kg.m -3 ). The purpose of this present work is to provide data about thermal conductivity against densities and used aggregates on one hand and moisture buffering as well as sorption/desorption properties on the other hand. We then position those materials to similar ones that could be hemp concretes, rape-straw concretes or lightweight's earthen materials.

MATERIALS

Aggregates

The vegetable aggregates used in this investigation are rape-straw and sunflower stem. Both are considered as by-products as those crops are cultivated for their seeds to produce canola and sunflower oil. Those plants' straws and stems have no other use but being buried in the fields as organic soil amendment. The sunflower stem is composed by a rigid external part (bark) and a lightweight inner part (pith) see Fig 1 and2. This pith has an honeycomb structure with large pores' size similar as the one observed for corn pith [Palumbo 2015]. The sunflower stem enabled us to use 3 different aggregates by separating its components: pure bark, pure pith and a mix of bark and pith this last one with the same density as the used rape-straw. Those vegetables were grinded with a Retsch SM100 knife mill using a 15mm grid. We had to remove the dust off the bark aggregates using a 2mm sieve.

Binder

The crude earth is excavated from a local quarry. This little factory used to be a production site of refractory bricks for bakery ovens in the beginning of last century. The high amount of clay of this crude earth and its lightness due to the presence of kaolinite naturally brings markets for art pottery and ceramics as well as for biobuilders who use it for finish earth plasters. They have therefore all the equipment in their production site to crush and sieve the raw excavated crude earth. The granulometric analysis (sieving and sedimentation) revealed us the following grain size proportions: 35% clay, 40% silt and 25% sand. The clay composition (kaolinite, montmorillonite, nontronite) has been characterized by X-Ray absorption.

Formulation and manufacturing

We investigated the hygric properties of those mixes at the same 2.4:1 binder:aggregates and 1:1 water:binder weight ratio. The significant differences in aggregates' densities and the variation of compaction strength used during the molding led to huge variations in samples' densities (see Tab. 1). We also have to notice that using the same water:binder ratio for such different aggregates leads to different mixtures' homogeneity as it has also been noticed by Palumbo and Navarro [Palumbo 2016] [Navarro 2015] and the compaction strength had to be modified to reach good enough workability. Crude earth and water were first mixed together at a 1:1 ratio after what we waited 10 min before adding the aggregates in order to let the clay being sufficiently hydrated. By modifying the compaction strength using a Zwick/Roell Z010 press we were able to reach different fresh densities in cylindrical molds. The demolded samples have then been dried in a 23°C 50%HR regulated climatic chamber. Cylindrical samples of 11cm diameter and 6cm thickness were produced for MBV's experiments see Fig. 3, other molds of 5x5x4cm for sorption/desorption purpose and another 11x5x4cm for thermal conductivity measurements has also been used. We measured the thermal conductivity at dry state (the samples were oven dried at 60°C for 24h). The measurement was realized by using the hot-wire technic following the ASTM D5930-97 standard. We used a NEOTIM FP2C conductivity meter equipped with hot wire sensor placed between 2 samples of similar geometry Fig. 4. The thermal conductivity was then the average value of its pair within 5 to 7 values. In our case 3 samples for each formulation were submitted to 75%RH during 8h and 33%RH during 16 hours. This dynamical characterization of the moisture buffering capacities of the materials pretends to simulate indoor climate variations during day and nights and then its ability to regulate indoor climate. We followed the Nordtest protocol [START_REF] Rode | Moisture Buffer Value of Materials in Building[END_REF]], cylindrical samples of 16cm diameter and 6cm thickness were realized and sealed with aluminum tape on all but one side in order to get an exposed area of 0,02m 2 . The air fans velocity was reduced to 10% of its maximum value and samples weren't exposed to the direct air flow. Nevertheless, since anemometric measurement haven't been carried next to the samples, the obtained MBV values could be overestimated. After having carried out 4 cycles, the weight amplitude did vary less than 0.20% from the last 3 days before we stopped the experiment. The unit for MBV is g/(m 2 .%RH). The practical MBV has been calculated using the following equation:

𝑀𝐵𝑉 = ∆𝑚 𝐴.(%𝑅𝐻ℎ𝑖𝑔ℎ-%𝑅𝐻𝑙𝑜𝑤) (1)
Where Δm is an average of the adsorbed and desorbed mass after the system has reached a dynamic equilibrium (g) and A is the exposed surface area (m 2 ).

Sorption/desorption

Sorption/desorption isotherm have been drawn for SBP, SB and RS using salt cup method. To control the relative humidity of the environment, the samples were stored into desiccators containing different mineral salts. Relative humidity rates used for this study are 12, 33, 44, 55, 66, 76, 86, 93 and 98 %. In order to determine the sorption curve, the different samples were first oven-dried (60°C for 24h) before being placed in the corresponding desiccators. In parallel, the other half of the samples were water-saturated by pouring water on them using a wash bottle (this method was employed because the samples tends to disintegrate when immersed in water) and stored in other desiccators at the same relative humidity.

RESULTS

Thermal conductivity

We plotted in Fig. 1 the measured thermal conductivities and densities of the tested samples. In order to compare with other data found in literature for vegetable concretes, we plotted on the same figure the empirical relationship established by Cerezo Eq.2 [START_REF] Cerezo | Propriétés Mécaniques, Thermiques et Acoustiques D'un Matériau à Base de Particules Végétales : Approche Expérimentale et Modélisation Théorique[END_REF]] for lime/hemp concretes for densities ranging from 200 to 800 kg.m -3 . This relationship was in good agreement with clay/straw mixtures experimental results found by Labat [START_REF] Labat | From the Experimental Characterization of the Hygrothermal Properties of Straw-Clay Mixtures to the Numerical Assessment of Their Buffering Potential[END_REF]] and the behavior is similar to our results. Our samples present though lower values of thermal conductivities for densities lowers than 500 kg.m -3. On the contrary, SBR samples experimental results at ρ=700kg.m -3 are very close to the empirical relationship see Fig. 6. [Palumbo 2016], [START_REF] Lima | Eco-Efficient Earthen Plasters . the Influence of the Addition of Natural Fibers[END_REF] which dealt with higher density materials. Labat [START_REF] Labat | From the Experimental Characterization of the Hygrothermal Properties of Straw-Clay Mixtures to the Numerical Assessment of Their Buffering Potential[END_REF]] did study lightweights straw/clay mixtures from 200 to 800 kg.m -3 and reach higher thermal conductivity values closer to those expected by Cerezo's relationship.

Clay

Moisture buffer value

Crude earth is known as a very good hygric regulator. Furthermore, it has been observed that the addition of aggregates like corn pith improved the moisture buffering [Palumbo 2016]. As expected the MBV of our mixtures is then higher than 2 g/(m 2 .%RH) see Tab.2 and can be classified as excellent according to the classification proposed by Rode [START_REF] Rode | Moisture Buffer Value of Materials in Building[END_REF]].

Tab. 2: Practical Moisture buffer values of the tested samples

We can notice that density doesn't seem to have a direct impact in terms of moisture buffering values as observed by McGregor for other earthen materials [McGregor see Fig. 7.

Sorption/desorption

The sorption/desorption curves were drawn for RS, SBR and SB see Fig. 8. All three mixtures show similar behavior and mass water content during the sorption phase. Nevertheless, while SBP still show similar desorption behavior with RS between 30 and 76%HR, SB do store less mass water content at this range of relative humidity leading to smaller hysteresis.

Fig The formulations allow here to reach low densities insulating plasters in order to get better performances in terms of thermal conductivity. As expected, the optimal results with thermal conductivity values below 0,040 W.m -K -1 were obtained by using sunflower pith, a very lightweight aggregate. According to NF P 75-101 standard, these values could allow to classify this material as insulating plaster and not thermal corrector anymore. Thus, further characterizations both at material and wall scales must be performed to fully evaluate those materials' properties.

According to the plant aggregate that will be chosen, the clay mineralogy and ratio used, a large variety of materials can be elaborated both for refurbishment and new construction needs.

ACKNOWLEDGMENTS

This project is granted by Région Centre, France. The author would like to gratefully thanks the groupe de développement agricole de Montrésor which provides the agricultural byproducts, the City of Loches Développement for the coordination and Eric Julien EURL for his support in the formulation and samples' preparation.

Fig. 1 :

 1 Fig. 1: SEM picture of sunflower pith

Fig. 3 :

 3 Fig. 3: Samples from left to right (SP, SBP, SB and RS)

Fig. 4 :

 4 Fig. 4: Hot wire NEOTIM FP2C conductivity meter with SP sample

Fig. 5 :

 5 Fig. 5: Samples in Binder KBF climatic chamber

Fig. 7 :

 7 Fig.7: Comparison of Practical MBV determined on the present test with other materials following NORDTEST protocol.