{'fraction_non_alphanumeric': 0.0444985579800838, 'fraction_numerical': 0.006720356967949067, 'mean_word_length': 4.16033696033696, 'pattern_counts': {'":': 0, '<': 59, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 19, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Featherweight Go

We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is widely used, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.


INTRODUCTION
This paper is our response to that question.
Two decades ago, Igarashi, Pierce, and Wadler [1999;2001], introduced Featherweight Java. They considered a tiny model of Java (FJ), extended that model with generics (FGJ), and translated FGJ to FJ (via erasure). In their footsteps, we introduce Featherweight Go. We consider a tiny model of Go (FG), extend that model with generics (FGG), and translate FGG to FG (via monomorphisation).
Go differs in interesting ways from Java. Subtyping in Java is nominal, whereas in Go it is structural. Casting in Java with generics is restricted to support erasure, whereas type assertions in Go with generics are unrestricted thanks to monomorphisation. Monomorphisation is widely used, but we are among the first to formalise it. The Expression Problem was first formulated by Wadler [1998] in the context of Java, though Java never supported a solution; but our design does.
We provide a full formal development: for FG and FGG, type and reduction rules, and preservation and progress; for monomorphisation, a formal translation from FGG to FG that preserves types and is a bisimulation. The appendices contain complete proofs.
Structural subtyping. Go is based on structures and interface types. Whereas most programming languages use nominal subtyping, Go is unique among mainstream typed programming languages in using structural subtyping. A structure implements an interface if it defines all the methods specified by that interface, and an interface implements another if the methods of the first are a superset of the methods specified by the second.
In Java, the superclasses of a class are fixed by the declaration. If lists are defined before collections, then one cannot retrofit collections as a superclass of lists-save by rewriting and recompiling the entire library. In Haskell the superclasses of a type class are fixed by the declaration. If monads are defined before functors, then one cannot retrofit functors as a superclass of monads-save by rewriting and recompiling the entire library. In contrast, in Go one might define lists or monads first, and later introduce collections or functors as an interface that the former implements-without rewriting or recompiling the earlier code.
The Expression Problem. The Expression Problem was formulated by Wadler [1998]. It gave a name to issues described by Cook [1990], Reynolds [1994], and Krishnamurthi et al. [1998], and became the basis of subsequent work by Torgersen [2004], Zenger and Odersky [2004], Swierstra [2008], and many others. Wadler defines The Expression Problem this way: The goal is to define a data type by cases, where one can add new cases to the data type and new functions over the data type, without recompiling existing code, and while retaining static type safety.
And motivates its interest as follows: Whether a language can solve the Expression Problem is a salient indicator of its capacity for expression. One can think of cases as rows and functions as columns in a table. In a functional language, the rows are fixed (cases in a datatype declaration) but it is easy to add new columns (functions). In an object-oriented language, the columns are fixed (methods in a class declaration) but it is easy to add new rows (subclasses). We want to make it easy to add either rows or columns.
One can come close to solving The Expression Problem in Go as it exists now, using dynamic checking via type assertions. We show how to provide a fully static solution in Go with generics.
Monomorphisation. FGJ translates to FJ via erasure, whereas FGG translates to FG via monomorphisation. Two instances List<int> and List<bool> in FGJ both translate to List in FJ (where <> are punctuation), whereas two instances List(int) and List(bool) in FGG translate to separate types List<int> and List<bool> in FG (where () are punctuation, but <> are taken as part of the name).
Erasure is more restrictive than monomorphisation. In Java with generics, a cast (a)x is illegal if a is a type variable, whereas in Go with generics, the equivalent type assertion x.(a) is permitted. Erasure is often less efficient than monomorphisation. In Java with generics, all type variables are boxed, whereas in Go with generics type variables may instantiate to be unboxed. However, erasure is linear in the size of the code, whereas monomorphisation can suffer an exponential blowup; and erasure is suited to separate compilation, whereas monomorphisation requires the whole program. We choose to look at monomorphisation in the first instance, because that is the design favoured by the Go team; other designs may be of interest, as we note in the conclusion.
Template expansion in C ++ [Stroustrup 2013, Chapter 26] corresponds to monomorphisation. Generics in .NET are implemented by a mixture of erasure and monomorphisation [Kennedy and Syme 2001]. The MLton compiler for Standard ML [Cejtin et al. 2000] and the Rust programming language [The Rust Team 2017] both apply techniques closely related to monomorphisation, as described by Fluet [2015] and Turon [2015] on web pages and blog posts. We say more about related work in Section 7, but we have found only a handful of peer-reviewed publications that touch on formalisation of monomorphisation. Monomorphisation is possible only when it requires a finite set of instances of types and methods. We believe we are the first to formalise computation of instance sets and determination of whether they are finite.
The bookkeeping required to formalise monomorphisation of instances and methods is not trivial. Monomorphising an interface with type parameters that contains a method with type parameters may require different instances of the interfaces to contain different instances of the methods. It took us several tries over many months to formalise it correctly. While the method for monomorphisation described here is specialised to Go, we expect it to be of wider interest, since similar issues arise for other languages and compilers such as C ++ , .Net, MLton, or Rust.
Featherweight vs complete. A reviewer of an earlier revision of this paper wrote: It is also quite common for semantics to strive for "completeness", instead of being "featherweight". There is a lot of value in having featherweight semantics, but the argument for completeness is that it helps language designers understand bad interactions between features. We agree with these words. Since the review was a reject, we deduce an implicit claim that it is better to be complete. Here, with respect, we disagree. We argue both "featherweight" and "complete" descriptions have value. As evidence, compare citations counts for the paper on Featherweight Java, Igarashi et al. [2001], with the four most-cited papers on more complete models, Drossopoulou and Eisenbach [1997]; Flatt et al. [1998]; Nipkow and von Oheimb [1998]; Syme [1999]: 1070 as compared with 549, 248, 174, 158, respectively (Google Scholar, April 2020).
Impact. One result of our work has been to shift the design away from contracts-which are syntactically convenient, but lack a clear semantics-and toward interfaces-which are already well defined in Go. Another result is the proposal for covariant receiver typing, a feature required by The Expression Problem. It is not part of the Go team's current design, but they have noted it is backward compatible and are considering adding it in future.
Outline. Section 2 introduces FG and FGG, presents a solution to The Expression Problem, and introduces monomorphisation. Sections 3 and 4 present FG and FGG; we give formal rules for types and reductions, and prove preservation and progress. Section 5 presents monomorphisation, which translates FGG back to FG; we prove the translation preserves types and is a bisimulation. Section 6 describes our prototype implementation. Section 7 describes related work. Section 8 concludes. Appendices provide extra examples and details of all proofs.

FEATHERWEIGHT GO BY EXAMPLE
Formally, FG and FGG are tiny languages, containing only structures, interfaces, and methods. Our examples use features of Go missing in FG and FGG, including booleans, integers, strings, and variable bindings. Appendices A.1 and A.2 show how to declare booleans in FG and FGG.

FG by example
Functions in FG. Figure 1 shows higher-order functions in FG. Interface Any has no methods, and so is implemented by any type. Interface Function has a single method, Apply(x Any) Any, which has an argument and result of type Any. It is implemented by any structure that defines a method with the same name and same signature. In Go structures and methods are declared separately, as compared to Java where they are grouped together in a class declaration. We give three examples.
Structure incr has a single field, n, of type int. Its Apply method has receiver this of type incr, argument x of type Any, and result type Any, and increments its argument by n. You might expect the  argument and result to instead have type int, but then the declared method would not implement the Function interface, because the method name and signature must match exactly. In the method's body, x.(int) is a type assertion that checks its argument is an integer; otherwise it panics, which is Go jargon for raising a runtime error. A structure is created by a literal, consisting of the structure name and its field values in braces. For instance, incr{-5}.Apply(3) returns -2. A field of a structure is accessed in the usual way, this.n. Here this is a variable bound to the receiver, not a keyword.
Structure pos has no fields, and its apply method returns true if given a positive integer. Structure compose has two fields, each of which itself is a function, and its apply method applies the two in succession. The top-level main method composes incr{-5} with pos{} and applies it to 3, yielding false. One cannot pass a value of type Any where a boolean is expected, so the type assertion .(bool) is required.
Variable names are irrelevant when comparing method signatures, but method names and type names must match exactly. For example, the following two signatures are considered equivalent: declaration introduces Int as a synonym for integers, and a method declaration ensures that type supports equality. Since signatures must match exactly, in the method the argument has type Eq and the body uses a type assertion to convert it to int as required.
Interface List has a single method: Map(f Function) List, which applies its argument to each element of its receiver. We define two structures that implement the list interface. Structure Nil has no fields, while structure Cons has two fields, a head of any type and a tail which is a list. The methods to define Map are straightforward, and the main method shows an example of its use.
Go is designed to enable efficient implementation. Structures are layed out in memory as a sequence of fields, while an interface is a pair of a pointer to an underlying structure and a pointer to a dictionary of methods. To ensure layout of a structure is finite, a structure that recurses on itself is forbidden. Thus, the declaration type Bad struct { oops Bad } is not allowed, and similarly for mutual recursion. However, structures that recurse through an interface are permitted, such as Cons with a tail field of type List that itself may contain a Cons.
If we wanted to define equality on lists, we would either need to access the head fields via type assertions .(Eq) in the method that defines equality, or to change the type of the head field to Eq.

FGG by Example
We now adapt the examples of the previous section to generics. Figure 3 shows higher-order functions in FGG. The interface for functions now takes two type parameters, Function(type a Any, b Any). Each type parameter is followed by an interface it must implement, called its bound. In this case, the bounds indicate that the argument and result may be of any type. The signature for the method is now Apply(x a) b, where the first type parameter is the argument type and the second the result type.

Functions in FGG.
Structures incr and pos are as before. However, they now have more natural signatures for their apply methods, where all occurrences of Any are replaced by int or bool as appropriate. Type assertions in the method bodies are no longer needed, and the types ensure a panic never occurs.
The structure for composition now takes three type parameters. In the top-level expression, type parameters are added and the type assertion at the end is no longer required.
Lists in FGG. Figure 4 shows equality and lists in FGG. The interface for equality is now written Eq(type a Eq(a)). It accepts a type parameter a where the bound is itself Eq(a). The method now has signature Equal(that a) bool. In the method declaration, the argument now has type int instead of type Eq, and a type assertion in the method body is no longer required. The situation where a type

Fig. 5. Mutually recursive bounds
parameter appears in its own bound is known as F-bounded polymorphism [Canning et al. 1989], and a similar idiom is common in Java with generics [Bracha et al. 1998;Naftalin and Wadler 2006].
Interface List now takes as a parameter the type of the elements of the list, bounded by Any. The signature for the map method is now Map(type b Any)(f Function(a, b)) List(b). The list interface takes a parameter a for the type of elements of the receiver list, while the map method itself takes an additional parameter b for the type of elements of the result list.
The two structures that implement lists now also take a type parameter, again bounded by Any. It may seem odd that Nil requires a parameter, since it represents a list with no elements. However, without this parameter we could not declare that Nil has method Map, whose signature mentions the type of the list elements.
The main method simply adds type parameters. In Go, no name can be bound to both a value and a type in a given scope, so it is always unambiguous as to whether one is parsing a type or an expression. In practice, writing out all type parameters in full can be tedious, and generic Go permits such parameters to be omitted when they can be inferred. Here we always require type parameters, leaving inference for future work.
Type parameter names and variable names are irrelevant when comparing method signatures, but method names, bounds on type parameters, and type names must match exactly. For example, the following two signatures are considered equivalent: Map(type bob Any)(fred Function(a, bob)) List(bob) If we wanted to define equality on lists without type assertions, we would need to bound the elements of the list so that they support equality, changing every occurrence of (type a Any), in the code to (type a Eq(a)), and similarly for b in the signature of Map.

Fig. 6. Expression problem in FGG
Mutual recursion in type bounds. In a declaration that introduces a list of type parameters, the bounds of each may refer to any of the others. Figure 5 shows two mutually-recursive interface declarations that may be useful in representing graphs. It is parameterised over types for edges and vertexes. Each edge has a source and target vertex, while each vertex has a list of edges.

The Expression Problem
Following Wadler [1998], we present The Expression Problem pared to a minimum. Our solution appears in Figure 6. There are just two structures that construct expressions, Num and Plus, which denote numbers and the sum of two expressions, respectively; and two methods that operate on expressions, Eval and String, which evaluate an expression and convert it to a string, respectively. We show that each constructor and operation can be added independently, proceeding in four steps: (1) define Eval on Num (3) define String on Num (2) define Eval on Plus (4) define String on Plus The order of steps 2 and 3 can be reversed: we may extend either by adding a new constructor or a new operation. We assume availability of the library function fmt.Sprintf to format strings.
Structure Num contains an integer value. Structure Plus contains two fields, left and right, which are themselves expressions. Typically, we might expect the type of these fields to be an interface specifying all operations we wish to perform on expressions. But the whole point of the expression problem is that we may add other operations later! Thus, plus takes a type parameter for the type of these fields. We bound the type parameter with Any, permitting it to be instantiated by any type.
For each operation, Eval and String, we define a corresponding interface to specify that operation, Evaler and Stringer. When defining Eval on Plus, the receiver's type parameter is bounded by interface Evaler, allowing Eval to be recursively invoked on the left and right expressions. Similarly, when defining String on Plus, the receiver's type parameter is bounded by interface Stringer, allowing String to be recursively invoked. Crucially, FGG permits the bounds on the type parameter in a receiver to implement the bound on the type parameter in the corresponding structure declaration (receiver type parameters are covariant). This is in contrast to method signatures, which must exactly match the signature in the interface (signatures are nonvariant). Since Evaler and Stringer implement Any, the method declarations are allowed.
A last step shows how to tie it all together. We define an interface Expr which embeds interfaces Evaler and Stringer, and show how to build a value of type Expr which we can then both evaluate and convert to a string.
How close could we get without generics? If we know all operations in advance, then in place of the type parameter in Plus we can use interface Expr, defining all required operations; but that removes the constraint that we can add operations later. Alternatively, in place of the type parameter in Plus we can use interface Any, with type assertions to Evaler or Stinger before the recursive calls; that allows us to add operations later, but violates the requisite that all types be checked statically.
As mentioned in the preceding section, in order to define equality on lists without type assertions, we would need to bound the elements of the lists so that they support equality. This might be regarded as a form of type pollution, as it rules out forming lists of a type that does not support equality (for instance, lists of functions) even if those lists are never tested for equality. An alternative design that applies the techniques developed here to avoid pollution is described in Appendix A.3.

Monomorphisation by example
We translate FGG into FG via monomorphisation. As an example, consider the FGG code in Figures 3 and 4. We only include the code relevant to the main method, so omit composition and equality. The given code monomorphises to the FG program shown in Figure 7.
Each parametric type and method in FGG is translated to a family of types and methods in FG, one for each possible instantiation of the type parameters. FGG type List(a) is instantiated at types int and bool, so it translates to the two FG types List<int> and List<bool>. For convenience, we assume that angle brackets and commas "<,>" may appear in FG identifiers, although that is not allowed in Go. In our prototype, we use Unicode letters that resemble angle brackets and a dash: Canadian Syllabics Pa (U+1438), Po (U+1433), and Final Short Horizontal Stroke (U+1428).
Monomorphisation tracks for each method the possible types of its receiver and type parameters. In this particular program, we need two instances of Map over lists of integers, one that yields a list of integers and one that yields a list of booleans, and none for Map over lists of booleans.
Each interface also contains an instance of a dummy version of Apply or Map, here called, e.g., Map<2>, where the number in brackets stands for a hash computed from the method signature. A dummy method is provided for every FGG method; these dummy methods are needed to ensure a correct implementation relation between structures and interfaces is maintained at runtime. For instance, if f is bound to a function such as incr{1} then the type assertion f.(List<bool>) should fail; but without the dummy it would succeed.
Monomorphisation yields specialised type declarations for structures and interfaces, and specialised method declarations, plus the required dummy methods. The source FGG and its translation to FG are both well-typed, and both evaluate to corresponding terms: we will show the translation preserves typing and is a bisimulation.
Not all typable FGG source can be monomorphised. Figure 8 shows a program that exhibits polymorphic recursion, where a method called at one type recursively calls itself at a different type. Here, calling method Nest on a receiver of type Box(a) leads to a recursive call on a receiver of type Box(Box(a)). Monomorphisation is impossible because we cannot determine in advance to what depth the types will nest. We will present a theorem stating that if source code does not exhibit problematic polymorphic recursion then it can be monomorphised.
3 FEATHERWEIGHT GO 3.1 FG syntax Figure 9 presents FG syntax. We let f range over field names, m range over method names, x range over variable names, t S , u S range over structure names, and t I , u I range over interface names. We let t, u range over type names, which are either structure or interface type names. We let d and e range over expressions, which have five forms: variable x, method call e.m(e), structure literal t S {e}, selection e.f , and type assertion e.(t). By convention, e stands for the sequence e 1 , . . . , e n . We consider e and e to be distinct metavariables.
A method signature M has the form (x t) t. Here x stands for x 1 , . . . , x n and t stands for t 1 , . . . , t n , and hence x t stands for x 1 t 1 , . . . , x n t n . We use similar conventions extensively.
A method specification S is a method name followed by a method signature. A type literal T is either a structure struct {f t} or an interface interface {S}. A declaration D is either a type declaration type t T or a method declaration func (x t S ) mM {return e}. In our examples, interface declarations may contain interface embeddings, i.e., a reference to another interface; for our formalism, we assume these are always expanded out to the corresponding method specifications.
A program P consists of a sequence of declarations D and a top-level expression e, written in the stylised form shown in the figure to make it legal Go. We sometimes abbreviate it as D ⊲ e. Figure 10 presents several auxiliary definitions. All definitions assume a given program with a fixed sequence of declarations D.

Auxiliary functions
Function fields(t S ) looks up the structure declaration for t S and returns a sequence (f t) of field names and their types. Write t S .m to refer to the method declaration with receiver type t S and name m. Function body(t S .m) returns (x : t S , x : t).e, where x : t S is the receiver parameter and its type, x : t the argument parameters and their types, and e the body from the declaration of a method with receiver of type t S and name m. In the phrase func (x t S ) m(x t) t, each of t S , t , and t is considered a distinct metavariable, and similarly for x and x. Function type( ) is explained in Section 3.4. Function unique(S) returns true if for every method specification mM in S the method name m uniquely determines the method signature M.
Function tdecls(D) returns a sequence with the name of every type declared in D. Function mdecls(D) returns a sequence with a pair t S .m for every method declared in D. Function distinct, not defined in the figure, takes a sequence and returns true if no item in the sequence is duplicated; order of items in the sequence is irrelevant, but it cannot take a set because items in a set are distinct by definition. Sequences may implicitly coerce to sets, but not vice-versa. When comparing method signatures, the names of formal variables are ignored; signatures are considered equal if they contain the same types in the same sequence.
Function methods(t) returns the set of all method specifications belonging to type t. If t is a structure type the method specifications are those from the method declarations with a receiver of the given type. It t is an interface type, the method specifications are those given in the interface. Figure 11 presents the FG typing rules. Let Γ range over environments, which are sequences of variables paired with type names, x : t. We write ∅ for the empty environment.

FG Typing
Judgement t <: u holds if type t implements type u. A structure type t S is only implemented by itself, while type t implements interface type t I if the methods defined on t are a superset of those defined on t I . It follows from the definition that <: is reflexive and transitive.
We write ok to indicate a construct is well-formed. Judgement t ok holds if type t is declared. Judgement S ok holds if method specification S is well formed: all formal variables x in it are distinct, and all the types t, t in it are declared. Judgement T ok holds if type literal T is well formed: for a structure, all field names must be distinct and all types declared; for an interface, all its method specifications must be well formed. Judgement D ok holds if declaration D is well formed: for a type declaration, its type literal must be well formed; for a method declaration, its receiver and formal variables must be distinct, all types must be declared, the method body must be well typed in the appropriate environment, and the expression type must implement the declared return type.
Well-formed method specifications and type literals Judgement Γ ⊢ e : t holds if in environment Γ expression e has type t. The rules for variables, method calls, structure literals, and field selection are straightforward. There are three rules for type assertions. A type assertion e.(t) always returns a value of type t (if it doesn't panic). Let e have type u. In Go source, u must always be an interface type. If t is also an interface type the assertion is always allowed (since e could always conceivably evaluate to a structure that implements t), but if t is a structure type the assertion is allowed only if t implements u (since otherwise e could not possibly contain a structure of type t). It would be stupid to write a type assertion if u has a structure type, because then the assertion could be checked at compile time, making it pointless. Nonetheless, during reduction a variable of interface type will be replaced by a value of structure

Value
: type, so without such stupid assertions an expression would become ill-typed during reduction. Stupid type assertions are similar to stupid casts as found in Featherweight Java. Judgement P ok holds if program P is well formed: all its type declarations are distinct, all its method declarations are distinct (each pair of a receiver type with a method name is distinct), all its declarations are well formed, and its body is well typed in the empty environment. Figure 12 presents the FG reduction rules. A value is a structure literal t S { } where each field is itself filled with a value. The auxiliary function type( ) returns t S when = t S { }. Evaluation contexts E are defined in the usual way. Judgement d −→ e holds if expression d steps to expression e. There are four rules, for field selection, method call, type assertion, and closure under evaluation contexts. All are straightforward.

FG properties
We have the usual results relating typing and reduction.
The substitution lemma is straightforward. It is sufficient to consider empty environments for the substituted terms, since FG has no binding constructs (such as lambda) in expressions.

L
3.2 (S ). If ∅ ⊢ : t and x : u ⊢ e : u and t <: u then ∅ ⊢ e[x := ] : t for some type t with t <: u.
The following are straightforward adaptions of the usual results. We say expression e panics if there exist evaluation context E, value , and type t such that e = E[ .(t)] and type( ) <: t.

FEATHERWEIGHT GENERIC GO
4.1 FGG Syntax Figure 13 presents FGG syntax, with the differences from FG syntax highlighted. We let α range over type parameters. and let τ , σ range over types. A type is either a type parameter α or a named type t(τ ). We also let τ S , σ S range over structure types of the form t S (τ ); τ I , σ I range over interface types of the form t I (τ ); and, τ , σ range over types that are either type parameters or interfaces τ I . Expressions and declarations are updated to replace type names by types, and method calls are updated to include type parameters: a structure declarations is now struct {f τ } and a method call is now e.m(τ )(e), a structure literal is now τ S {e}, and a type assertion is now e.(τ ).
We let Φ, Ψ range over type formals, which have the form type α τ I , pairing type parameters with their bounds, which are interface types. The bounds in type formals are mutually recursive, i.e., each interface in τ I may refer to any parameter in α. Type declarations type t(Φ) T , and signatures (Ψ)(x τ ) τ , and method declarations func (x t S (Φ)) mM {return e} now include type formals.
We let ϕ,ψ range over type actuals, which are sequences of types. Figure 14 presents several auxiliary definitions. As before, Γ ranges over environments, which are now sequences that pair variables with types, x : τ . In addition, ∆ ranges over type environments, which are sequences that pair type parameters with bounds, α : τ I . Type formals Φ, Ψ may implicitly coerce to type environments. We write η = (Φ := ϕ) for the substitution of formals Φ by actuals ϕ, and η = (Φ := ∆ ϕ) for the partial function that also checks that ϕ respects the bounds imposed by Φ. If a partial function that is undefined appears in the hypothesis of a rule, then the rule does not hold. We writeΦ for the type parameters of Φ.

Auxiliary functions
Functions fields(τ S ) and body(τ S .m(ψ )) are updated to replace type names by types, and for the latter to include method type arguments. The definitions are adjusted to include type formals which are instantiated appropriately. Functions type, unique, tdecls, and mdecls are updated to replace type names by types and include type formals. Function bounds ∆ (τ ) takes a type parameter to its bound, and leaves its argument unchanged otherwise.
Function methods ∆ (τ ) is updated to accept a type environment and to replace type names by types. The definition is adjusted to include type formals which are instantiated appropriately. If methods is applied to a type parameter, that parameter behaves the same as its bounding interface, so methods ∆ (τ ) = methods ∆ (bounds ∆ (τ )) for all τ . Figure 15 presents the FGG typing rules. Judgement ∆ ⊢ τ <:σ now depends on a type environment and relates types rather than type names. The definition is adjusted so that a type parameter implements its bound. It still follows from the definition that <: is reflexive and transitive. Judgement Φ<: Ψ compares the corresponding bounds of two type formals under an empty type environment. Judgement ∆ ⊢ τ ok holds if a type is well formed: all type parameters in it must be declared in ∆ and all named types must be instantiated with types that satisfy the bounds of the corresponding type parameters. Judgement ∆ ⊢ ϕ ok holds if under environment ∆ all types in ϕ are well formed.

FGG Typing
Judgement Φ ⊢ Ψ ok holds if under type environment Φ the type formal Ψ is well formed: all type parameters bound by Φ and Ψ are distinct, and all the bounds in Ψ are well formed in the type environment that results from combining Φ and Ψ. Note this permits mutually recursive bounds in a type formal. Judgement Φ; Ψ ok ∆ holds if a method declaration with receiver formals Φ and method formals Ψ is well formed, yielding type environment ∆: it requires that Φ is well formed under the empty environment, Ψ is well formed under Φ, and ∆ is the concatenation of Φ and Ψ. Hence, the type formals of the receiver are in scope when declaring the type formals of the method, but not vice versa, and both are in scope for declaring the types of the arguments and result.
Well-formed type and actuals Well-formed type formals and nested formals   Judgement Φ ⊢ S ok holds if under type environment Φ method specification S is well formed: it requires Φ, Ψ ok ∆ where Ψ is the type formals of the method specification, and the rest is similar to before but now under type environment ∆. Judgement Φ ⊢ T ok holds if under type formals Φ type literal T is well formed, and again is a straightforward adjustment of its earlier definition.

Well-formed method specifications and type literals
Judgement D ok holds if declaration D is well formed. The definitions are similar to previous definition. For a type declaration, its type formals must be well formed under the empty type environment, and its type literal must be well formed under the environment given by the type formals. For a method declaration, we require Φ; Ψ ok ∆, where Φ are the type formals of the receiver and Ψ are the type formals of the method. The receiver type must be declared with formals Φ ′ , where Φ <: Φ ′ . An alternative, simpler design would require Φ and Φ ′ to be identical; but that would rule out the solution to the expression problem given in Section 2.3. The rest is a straightforward adjustment of its earlier definition. Judgement ∆; Γ ⊢ e : τ holds if under type environment ∆ and environment Γ expression e has type τ . The adjustments are straightforward. Method calls are adjusted so that the type of the arguments and result are instantiated by the method type arguments. Type assertions are adjusted to take into account that type names are replaced by types. In method calls and type assertions, type parameters are treated as equivalent to the parameters' bound. Figure 16 presents the FG typing rules.

FGG Reduction
The adjustment to values, the auxiliary function type, and to evaluation contexts are simple, replacing type names by types and adding type arguments as appropriate. Judgement d −→ e holds if expression d steps to expression e. Again, the adjustments are all simple.

FGG properties
The results of the previous section adapt straightforwardly.
The substitution lemma is adapted to take into account that in a method declaration the type parameters of the receiver are substituted before the type parameters of the method. 4.2 (S ). Let η = (α := τ ) be a substitution.
The remaining results are easy to adjust.  4.4 (P ). If ∅; ∅ ⊢ d : σ then either d is a value, d −→ e for some e, or d panics.

MONOMORPHISATION
The monomorphisation process consists of two phases. In the first phase, a set of types and method instantiations are collected from an FGG program. In the second phase, an FGG program is translated to its FG equivalent following the instance set computed in the first phase.

Collecting type and method instances
Let ω, Ω range over instance sets, which contain elements of type τ or pairs of a type with a method and its type parameters, τ .m(ψ ). In Figure 17 we define a judgement P ◮ Ω which computes the set of instances of types and methods required to correctly monomorphise an FGG program. Judgement ∆; Γ ⊢ e ◮ ω holds if ω is the instance set for expression e, given environments ∆ and Γ. In the rules for variables, structure literals, field selections and type assertions, we simply collect the occurrences of type instances and proceed inductively. The rule for method calls additionally records the instantiation of the method τ .m(ψ ) where τ is the type of its receiver. In the rules for structure literals and method calls, we assume that sequences of instance sets, e.g., ω, coerce to a set consisting of the union of the elements of the sequence.
The instance set of a program P is the limit of function G applied to the instance set of its body. G ∆ (ω) is defined via four auxiliary functions that compute the type and method instances required by the elements of ω. It returns all type and method instantiations that are required to monomorphise declarations (F-closure, M-closure) and to preserve the <: relation (I-closure, S-closure).
F-closure finds all the type instances that occur in the declarations of structures, while M-closure finds all the type instances that occur in the declarations of method instances.
I-closure finds all the method signature instances that are required to preserve the <: relation over interfaces. S-closure finds all the type and method sets required by method calls, interprocedurally. For each method instance τ .m(ψ ) in ω it finds all instance sets of all implementations of method m, following the <: relation. Intuitively, I-closure and S-closure are used to guarantee that if τ <: σ , then the monomorphised version of τ also implements the monomorphised version of σ .

Monomorphisation judgement
We now define a judgement ⊢ P → P † where P is a program in FGG, and P † is a corresponding monomorphised program in FG. This judgement is in turn defined by judgements for each of the syntactic categories in FGG. Some of the judgements are also parameterised by instance sets (ranged over by Ω), substitutions that map type parameters to ground types (ranged over by η), or method instance sets (ranged over by µ). Figure 18 formalises how we recursively apply a consistent renaming to generate FG code. To monomorphise types, type formals, method names, and method formals, given a substitution η, we assume a map from closed types to identifiers. For instance, if f is a type with two parameters, and g and h are types with no parameters, then closed type f(g(), h()) might correspond to the identifier "f<g<>,h<>>" assuming "<,>" are allowed as letters in identifiers. We write t † = τ to compute the identifier t † that corresponds to closed type τ . Similarly, we write m † = m(ψ ) to compute the identifier m † that corresponds to closed method instantiation m(ψ ).
To monomorphise an expression given a substitution η, we recursively monomorphise all the types and expressions contained within this expression. We proceed similarly to monomorphise method signatures in Rule .
Rule is used to generate a dummy method signature that represents uniquely the alphaequivalence class of its FGG counterpart. The signature specifies no parameters and the return type Top. It is necessary to generate such methods to ensure that if a type does not implement another, then this is also the case in the monomorphised program. We assume that hash(mM 1 ) = hash(mM 2 ) for all M 1 = M 2 , using the same notion of equality as in unique and <:.
To monomorphise a structure given a substitution, we recursively monomorphise all the types contained within its field declarations. To monomorphise an interface, we recursively monomorphise each of its signatures and flatten the result in a single sequence of declarations. Figure 19 formalises how declarations are generated from Ω. Here we let N range over (x τ ) τ .
To monomorphise an interface specification we pass two environments. One is a substitution from type parameters to ground types η and the other is a set of method instances µ, i.e., a set of entries of type m(ψ ). For each entry in µ, we compute a new substitution θ which extends η and is used to generate a monomorphised instance of the corresponding signature. In addition, we generate dummy signature S † that uniquely identifies the FGG signature. Each parameterised method may produce zero or more monomorphised instances, plus a dummy method signature.
To monomorphise the declaration of a type t given an instance set, for each instance of t, we generate a substitution η and a method instance set µ. Then we recursively produce a monomorphised declaration for each generated pair of η and µ. Note that each type declaration may produce zero or more monomorphised declarations.
To monomorphise a method declaration given an instance set, we compute a substitution θ for each method instance in Ω. Then we produce a monomorphised version of a method for each of its instantiations. Note that each method declaration may produce zero or more monomorphised declarations. In addition, for each type instance and each of its methods, we generate a dummy method that returns an instance of Top.
To monomorphise a program P, we compute its instance set Ω then monomorphise its declaration and body given with respect to Ω. We additionally add the declaration of the empty structure Top.

Ruling out non-monomorphisable programs
It is not possible to monomorphise all FGG programs since programs that contain polymorphic recursive methods may produce infinitely many type instances. To address this issue, we propose a predicate P nomono which conservatively identifies programs that can produce infinitely many type instances. Programs for which this predicate does not hold are guaranteed to be monomorphisable.
The predicate is formally defined in Figure 20, notably reusing our instance generation procedures. P nomono holds if D nomono for at least one of its method declarations. D nomono holds if it is possible to find an element in its instance set, inductively constructed using function S-closure, such that the occurs check is satisfied. The occurs check holds when a type variable appears under a type constructor in a type instance or method call (in the same position it occupies in the type or method formal). We write fv(τ ) for the set of type parameters occurring in τ .

Monomorphisation properties
We can decide whether a program is monomorphisable.
T 5.1 (D ). If P ok then it is decidable whether or not P nomono holds.
T 5.2 (M ). If P ok and P nomono doesn't hold then P ◮ Ω with Ω finite.
Monomorphisation preserves typing and preserves and reflects reductions (see Figure 21).

IMPLEMENTATION
We have made available a prototype implementation, which contains FG and FGG type checkers and interpreters, and a monomorphiser from FGG to FG (including the nomono check). We wrote the implementation in Go to facilitate interactions with the Go designers and community. Our interface includes some extensions to our tiny syntax for FG and FGG, such as direct support for interface embedding, some primitive data types, and minimal I/O. Versions of all the presented examples have been tested using the implementation.
We took advantage of the implementation to perform extensive testing. FG evaluation results are compared to those using the official Go compiler, and the FG and FGG interpreters support dynamic checking of preservation and progress. To test monomorphisation, we added the test of bisimulation depicted in Figure 21: given a well-typed FGG program we generate its FG monomorphisation; we step the FGG and FG terms and confirm that the new FGG term monomorphises to the new FG term; and repeat until termination.
Besides handcrafted examples and stress tests, we used NEAT [Claessen et al. 2015;Duregård 2016] to lazily enumerate all well-typed programs (up to some size relative to the total number of occurrences of method and type symbols) from a subset of FGG (similar to S C [Runciman et al. 2008]). The subset consists of programs which have: (1) at least one method and one field; (2) at most one empty interface; and (3) at most two empty structs. And where: (1) each method has at most two arguments; (2) each struct has at most two fields; (3) each interface has at most two members and two parents; and (4) each method or type constructor has at most two type parameters. Moreover, we disallow mutually recursive type definitions. These measures are taken to truncate the space of possible programs. We generate all FGG programs in our subset up to size 20, and confirm they pass the bisimulation test described above.

RELATED WORK
This paper is the first to present a core formalism for the Go language. Our presentation is styled after that of Featherweight Java by Igarashi et al. [2001]. Like them, we focus on a tiny, functional subset of the language; we define versions with and without generics; and we consider translation from one to the other. We also mark as "stupid" casts/type assertions that are disallowed in source but are required for reduction to preserve types.
Our work resembles the development of generics for Java by Bracha et al. [1998] and for .NET by [Kennedy and Syme 2001] in that we build on a well-established base language. Prior work on generics adopts one, or a combination, of three main approaches, erasure, run-time representation of types as values, and monomorphisation.
[1998] present a translation from Java with generics to Java without generics that erases all information about type parameters. The translation relies on bridge methods, which in turn rely on method overloading, which is not supported in Go. Igarashi et al. [1999] formalised the translation for the FJ subset of Java (avoiding bridge methods) and proved it preserves typing and reductions. Downsides of erasure are that casts to generic types must be restricted and creation of generic arrays becomes tricky (see [Naftalin and Wadler 2006]). Moreover, erased code is often less efficient than monomorphised code. An upside is that erasure is linear in the size of the source, whereas monomorphisation can lead to an explosion in code size.
Run-time representation. In contrast to Java erasure, Kennedy and Syme [2001] developed an extension of the .NET Common Language Runtime (CLR) and C # with direct support for generics. They generate a mixture of specialised and shared code: the former is compiled separately for each primitive type and is similar to monomorphisation; the latter is compiled once for every object type and is similar to erasure. JIT compilation is exploited to perform specialisation dynamically, avoiding potential code bloat. Code sharing is implemented by storing run-time type-reps [Crary et al. 1998] for type parameters.
The overhead of runtime assembly of type-reps can be optimised by pre-computing and caching maps from open types to their reps when a generic type or method is instantiated [Kennedy and Syme 2001;Viroli and Natali 2000]. In future work, we may also look to techniques of optimising the coexistence of uniform (boxed) and non-uniform representations in polymorphic code [Leroy 1992] for dealing with the analogous mixture of struct and interface values in generic Go code.
Monomorphisation. Although monomorphisation has been employed for languages such as C ++ , Standard ML and Rust [Turon 2015], we found a relative lack of peer-reviewed literature on this topic. This section discusses works related to monomorphisation that do not state or prove any correctness results.
Stroustrup [2013, Chapter 26] describes template instantiation in C ++ . It is widely used, and infamous for code bloat.
Benton et al. [1998] describes a whole-program compiler from SML'97 to Java bytecode, where polymorphism is fully monomorphised. Monomorphisation is alway possible, since Standard ML rules out polymorphic recursion (unlike FGG). Fluet [2015] sketches a similar approach used in the SML optimising compiler MLton.
Tolmach and Oliva [1998, Section 6] develop a typed translation from an ML-like language to Ada, based on monomorphisation and presented in detail. Unlike us, they do not address subtyping (structural or otherwise) and they presume the absence of polymorphic recursion.
Jones [1995] describes the use of specialisation to efficiently compile type classes for Haskell, which bears some resemblance to monomorphisation.
Formalisation. We now consider works that formalise some aspect of monomorphisation. Yu et al. [2004] formalise the mixed specialisation and sharing mechanisms of the .NET JIT compiler [Kennedy and Syme 2001]. The work describes a type and semantics preserving translation to a polymorphic .NET Intermediate Language (IL), where polymorphic behaviours are driven by type-reps [Crary et al. 1998], codifying run-time type data that can be used in e.g. dynamic casts. Their approach only generates code where type variables are instantiated with basic data types, using a uniform (i.e. boxed) representation for all other types. This sidesteps the key challenges of monomorphising code with polymorphic recursion and parameterised methods. Notably, Kennedy and Syme [2001] state that "some polymorphism simply cannot be specialized statically (polymorphic recursion, first-class polymorphism)". In contrast, we present an algorithm that can determine whether monomorphisation is possible in the presence of polymorphic recursion.
Siek and Taha [2006] formalise the C ++ template instantiation mechanism. They model partial specialization, template parameterisation and instantiation, and prove type soundness of template expansion. Unlike us, they do not state or prove bisimulation or preservation of reductions. Since C ++ templates are Turing-complete, their soundness results are modulo termination, whereas our algorithms are guaranteed to terminate.
Tanaka et al. [2018, Section 2] report on a monomorphisation algorithm for Coq (Gallina) used in generation of low-level C code. Unlike us, they do not test for polymorphic recursion.
Monomorphisation and logic. In a related area, Blanchette et al. [2016]; Bobot and Paskevich [2011] study monomorphisation for polymorphic first-order logic formulas, targeting the untyped or multi-sorted logics found in automated theorem provers.

CONCLUSION
This is the beginning of the story, not the end. In future work, we plan to look at other methods of implementation beside monomorphisation, and in particular to consider an implementation based on passing runtime representations of types, similar to that used for .NET generics [Kennedy and Syme 2001]. A mixed approach that uses monomorphisation sometimes and passing runtime representations sometimes might be best, again similar to that used for .NET generics.
Featherweight Go is restricted to a tiny subset of Go. We plan a model of other important features such as assignments, arrays, slices, and packages, which we will dub Bantamweight Go; and a model of Go's innovative concurrency mechanism based on "goroutines" and message passing, which we will dub Cruiserweight Go.  Figure 22 shows how to implement booleans in FG. We begin by declaring two general-purpose interfaces. Interface Any has no methods, and so is implemented by any type. Interface Eq has one method with signature Equal(that Eq) Bool, an equality test that accepts an argument which is itself of type Eq and returns a boolean.
Interface Bool has three methods. Method Not() Bool computes the logical negation of its receiver. Method Equal(that Eq) Bool checks whether its receiver is equal to its argument. Method Cond(br Branches) Any executes one of two branches depending on whether the receiver is true or false. It refers to interface Branches, which has two methods with signatures IfTT() Any and IfFF() Any, one to be invoked for a true conditional and one to be invoked for a false conditional.
Go also supports interface embedding. Mentioning one interface in another stands for all the methods declared in the first. For example, the Bool interface in the figure is equivalent to: where the method specification for Equal has been replaced by the interface Eq. We use interface embedding in examples, but our formalism for FG assumes each interface embedding is expanded out to the corresponding method specifications.
We then define two structure types, TT and FF, each with no fields, and methods are defined with receivers of both types for each of the three methods Not, Equal, and Cond. Since they have methods whose signatures match those in interface Bool, we say that structure types TT and FF both implement the interface Bool.
Method Not returns false on receiver true, and true on receiver false. For instance, TT{}.Not() returns FF{}.
Method Equal returns its argument on true and the negation of its argument on false. The type assertion that.(Bool) returns the argument that if it implements the interface Bool and panics otherwise, where panic is Go jargon for indicating a runtime error has occurred. For instance, b.Equal(b) returns true if b is a boolean, while b.Equal(x) panics if b is a boolean but x is not.
Finally, method Cond invokes either IfTT() or IfFF() on its argument, depending on whether the receiver is true or false. For instance, assume x has type Eq and xs has type Cons, and that Equal and Contains are both methods that return booleans. The type assertion .(Bool) is required since otherwise the type of the expression would be Any, whereas Bool is expected. As one would expect, method Contains is called only when the condition is true.

A.2 Booleans in FGG
Booleans are adapted to generics in Figure 23. Interface Any is unchanged. The interface for equality is now written Eq(type a Eq(a)), indicating that it accepts a type parameter. A type parameter is always followed by an interface that it must implement, which is called its bound. Often the bound is Any, but in this case, the bound on a is itself Eq(a). For instance, we will see that Bool implements Eq(Bool). But Any does not implement Eq(Any), so the latter is not a valid type. The situation where a type parameter appears in its own bound is known as F-bounded polymorphism [Canning et al. 1989], and a similar idiom is common in Java with generics [Bracha et al. 1998;Naftalin and Wadler 2006].
In interface Bool, the signature for negation is unchanged. The signature for equality is now Equal(that Bool) Bool, where the argument type has now been refined from Eq to Bool. The signature for conditionals is now Cond(type a Any)(br Branches(a)) a where method Cond now accepts a type parameter, with bound Any. Its argument type has been refined from type Branches to type Branches(a), and its result has been refined from type Any to type a. Using interface embedding, we could equivalently write the interface as type Bool interface { Not() Bool Eq(Bool) Cond(type a Any)(br Branches(a)) a } which includes all members of the Eq(Bool) interface in the Bool interface.
The interface for branches now also takes a type parameter, Branch(type a Any), and the signatures of its methods are now IfTT() a and IfFF() a, where the result types have been refined from Any to a.
The two structure types, TT and FF are just as before, as is the method for logical negation. The method for equality are as before, save that the argument type has changed from Eq to Bool. The type assertions previously required to convert the argument to a boolean are no longer needed. Indeed, typing is now strong enough to assure a panic never occurs when evaluating equality.
Finally, the method for conditionals is as before, save for the refinement to its signature. Whereas in the previous example we wrote return x.Equal(xs.head).Cond (containsBr{x,xs} (a), c Eq(c))) Equal(ys c) bool { ys, ok := ys. (Nil(a,c)) return ok } func (xs Cons(type a Eq(a), c Eq(c))) Equal(ys c) bool { ys, ok := ys. (Cons(a,c)) return ok && xs.head.Equal(ys.head) && xs.tail.Equal(ys.tail) } // tie it all together type List(type a Eq (a) Method Cond now takes a type parameter Bool specifying its result type, so the type assertion .(Bool) can be removed.
We will always give type parameters in full, although in practice it is planned that these can be omitted if infered; describing type inference in full is a matter for future work. In Go, each name has only one binding in a scope, and hence in a constructs like receiver.Method(Type) (argument) no ambiguity arises if the (Type) parameter is dropped, because it is easy to determine whether a code fragment denotes a type or a value.
As before, for convenience in our examples we will assume booleans, integers, and strings as primitives in what follows. Our previous versions adapt as follows.
interface Eq(type a Eq(a)) { Equal (that a) bool } func (this bool) Equal(that bool) bool { return this == that } func (this int) Equal(that int) int { return this == that } Now the two definitions of equality may give the correct type to their argument, and no type assertions are required. Again, typing is now strong enough to assure a panic never occurs when evaluating equality. We have bool implements Eq(bool) and int implements Eq(int).

A.3 Lists in the style of The Expression Problem
In Section 2.3, we remarked that defining equality on lists pollutes the type, as it rules out forming lists of a type that does not support equality. We now present an alternative design that permits a list with elements of any type when Map is the only operation applied to the list, but requires elements to support equality when Equal is applied.
Our alternative solution for lists appears in Figure 24. Structures Nil and Cons now take not one but two type parameters, both bounded by interface Any. As before, parameter a is the type of the elements of the list (the head field of Cons), while the new parameter c is the type of the lists themselves (the tail field of Cons). The type parameters only appear in the definition of Cons, but we also add them to Nil because we may need to refer to them in the signatures of operations. (As it happens, c doesn't appear in the signatures here, but it would be needed if we wanted to define, for instance, a method to append two lists.) To avoid pollution, for each operation, Map and Equal we define a corresponding interface to specify that operation, Mapper and Eq.
Method Map now takes not one but two type parameters, both bounded by interface Any. As before, parameter b is the type of the elements of the result list, while the new parameter d is the type of the result list itself. When defining Map on Cons, the receiver's first parameter a is bounded by Any and its second type parameter c is bounded by Mapper(a), allowing Map to be recursively invoked on the tail.
When defining Equal on Cons, the receiver's first parameter a is bounded by Eq(a), allowing list elements to be tested for equality, and its second type parameter c is bounded by Eq(c), allowing Equal to be recursively invoked on the tail.
The bodies of the methods for equality use a second form of type assertion which returns both a value of the asserted type (xs, rebound) and a boolean saying whether the assertion succeeded (ok). Unlike the other form of type assertions, these can never panic, and so are not an issue with regard to static type checking. They are not included in our formalisations of FG and FGG, but would be easy to add.
As in the expression problem, for both Map and Equal it is crucial that bounds on the type receiver are covariant. Since the bounds on the parameters in Nil and Cons are Any, it is fine for the receivers to use tighter bounds, such as Mapper or Eq.
A last step shows how to tie it all together. We define an interface List(a) which embeds interfaces Mapper(a) and Eq(List(a)). At this point, the pollution occurs, and we bound type parameter a by interface Eq(a), since we must be able to test list elements for equality.
Not all applications will require this level of flexibility, or desire the associated complexity. But it is good that this design pattern is supported, and it is easy to see it may be valuable in some situations.

B FG TYPE SOUNDNESS This section develops FG type soundness in the form of Type Preservation by evaluation (Appendix B.1 and Progress (Appendix B.2).
The various substitution properties are often stated more generally in this appendix for convenience (i.e., those in the main matter are special cases of the results developed here). We make use of a reduction relation that replaces the contextual rule with the equivalent set of rules that identify each possible reduction explicitly, implementing a left-to-right call-by-value semantics. Uses of these congruence rules are labelled with the prefix . The development of progress makes use of an inductively defined epanic predicate, which holds iff expression e causes a runtime panic (i.e., contains an invalid type assertion). This predicate is equivalent to the definition of panics from the main matter.
by inversion on typing ∅ ⊢ e f : t a by inversion on typing t a <: t f by inversion on typing fields(t S ) = f t f by inversion on typing ∅ ⊢ e f i : t a i and t a i <: t f i by inversion on typing m(x t p ) t r ∈ methods(t S ) by inversion on typing ∅ ⊢ e a : t a by inversion on typing t a <: t p by inversion on typing x : t S , x : t p ⊢ e 0 : t 1 with t 1 <: t r by inversion on method typing ⊢ e 0 [x 0 := t S {e}][x := e a ] : t 2 , for some t 2 <: t 1 by Lemma B.5 t 2 <: t r by transitivity

inversion on typing
Case: Rule e = e 0 .m(e a ), e ′ = e ′ 0 .m(e a ), t = t r e 0 −→ e ′ 0 by inversion on −→ ∅ ⊢ e 0 : t 0 by inversion on typing m(x t p ) t r ∈ methods(t 0 ) by inversion on typing ∅ ⊢ e a : t a by inversion on typing t a <: t p by inversion on typing ∅ ⊢ e 0 : t 1 , for some t 1 <: t 0 by i.h. m(x t p ) t r ∈ methods(t 1 ) by Lemma B.3 ∅ ⊢ e ′ 0 .m(e a ) : t r by t r <: t r by reflexivity Case: Rule e = e 0 .m(e a ), e ′ = e 0 .m(e ′ a ), t = t r e a i −→ e ′ a i by inversion on −→ ∅ ⊢ e 0 : t 0 by inversion on typing m(x t p ) t r ∈ methods(t 0 ) by inversion on typing ∅ ⊢ e a : t a by inversion on typing t a <: t p by inversion on typing ∅ ⊢ e ′ a i : t 1 , for some t 1 <: t a i by i.h. t 1 <: t p i by transitivity ∅ ⊢ e 0 .m(e ′ a ) : t r by t r <: t r by reflexivity by inversion on typing Subcase: Γ ⊢ e 0 : t I by inversion on typing Γ ⊢ e ′ 0 : t 0 , for some t 0 <: t I by i.h. Subsubcase: t 0 is an interface type and t ′ is a struct type t 0 = t I and t ′ <: t I by value restriction Γ ⊢ e ′ 0 .(t ′ ) : t ′ by S Subsubcase: t 0 is an interface type and t ′ is an interface type

B.2 Progress
The inductive definition of e panic is given below: . If e is a value and ∅ ⊢ e : t then t = t S , for some t S and e = t S { }, for some .

P
. Straightforward induction on typing.
T B.8 (P ). If ∅ ⊢ e : t then either e is a value, e panic, or e −→ e ′ .

P
. By induction on typing. We show two illustrative but standard cases and then all cases pertaining to type assertions. Case: by inversion e is a value, e panic or e −→ e ′ by i.h. Subcase: e is a value The various substitution properties are often stated more generally in this appendix for convenience (i.e., those in the main matter are special cases of the results developed here). We make use of a reduction relation that replaces the contextual rule with the equivalent set of rules that identify each possible reduction explicitly, implementing a left-to-right call-by-value semantics. Uses of these congruence rules are labelled with the prefix . The development of progress makes use of an inductively defined e panic predicate, which holds iff expression e causes a runtime panic (i.e., contains an invalid type assertion). This predicate is equivalent to the definition of panics from the main matter.

C.1 Type Preservation
Below we write Φ, α : τ I under the assumption that distinct(Φ, α) and treat typing contexts and ∆ and type formals Φ, Ψ interchangeably, as in the rules of Section 4.

P
. Straightforward induction on the definition of <:.

P
. By induction on the derivation of ∆ 0 , α : τ I , ∆ 1 ; Γ ⊢ e : τ . Case:  by Lemma C.9 The proof of type preservation below relies on explicit congruence rules for the reduction semantics.

C.2 Progress
We extend the definition of e panic straightforwardly from FG to FGG. L C.13 (FGG C F ). If e is a value and ∅; ∅ ⊢ e : t then t = τ S , for some τ S and e = τ S { }, for some .

P
. Straightforward induction on typing.

P
. The proof follows the same lines of Theorem B.8.

P
. By straightforward induction on the rules from Figure 17.
Hereafter, we let ρ range over elements of Ω and ω, i.e., ρ is of the form τ or τ .m(ψ ). Also, we assume that all formal type parameters are pairwise distinct, without loss of generality.
Give η = (α := τ ) and η ′ = (α := σ ), we write [η] ⋗[η ′ ], iff the number of solved variables in η ′ is strictly greater than the number of solved variables in η. Variable α is solved in (α := τ ) if α ∈ α and α fv(τ ). We say that η is solved if all its variables are solved, otherwise it is unsolved. L C.17. Given P = D ⊲ d, if P ok holds and P nomono does not hold, then for each dec- .m(Ψ)}) for all n ≥ 1. Using Lemma C.16, we know that every element in these sets (where k is n or n + 1) is of the form ρ[η 1 · · · η k ] such that 1 ≤ i ≤ k, [η 1 · · · η i ] is good. There are finitely many instance ρ since they consists of a type name with finitely many type parameters, or a pair of type name with finitely many parameters and a method name, with finitely many type parameters. The number of distinct ρ is bounded by the number of declarations (methods and types) and the number of method signatures in interfaces.
Because each η i is extracted from a syntactical occurrence of a method call or type instantiation, there are also finitely many substitutions η i . The number of distinct substitutions η i is bounded by the size of the syntax of P.
By Lemma C.16, the sequences of substitutions grow on the left. We show that there is a well-founded ordering on these sequences, when they are not permutations. Note that they are only finitely many substitutions that are permutations. First, every sequence of substitutions [η 1 · · · η i · · · η n ] with η i solved, can replaced by [η 1 · · · η i ].
Next, we show that for (assuming we have shortened the sequences with solved substitutions as above).
Clearly the number of solved variables in [η ·η ′ ] is at least the number of solved variables in [η ′ ], indeed each α i occurring in τ is replaced by σ i . There must be α i such that it fv(σ )∩α = ∅ otherwise there would be a cycle which would lead to a bad substitution. Applying all substitutions in η ′ then replacing α i will solve it in [η · η ′ ] hence the number of solved variable is strictly increasing.
Hence, there is well-founded ordering over the elements generated by the limit of G, hence there exists a finite fixpoint.

T
C.18 (D ). If P ok then it is decidable whether or not P nomono holds.

P
. We construct a dovetailing algorithm that decides whether or not P nomono holds as follows. Given P = D ⊲d, we simultaneously check whether D i nomono holds for all i iteratively (starting with n = 1). The algorithm terminates either (i) when n is found such that G n , a fixpoint has been found, for each method declaration, or (ii) when there is a method such that there is n with (t S (ϕ).m(ψ )) ∈ G n ∆ (ω ∪ {t S (Φ)}) s.t. Φ ≺ ϕ or Ψ ≺ ψ (i.e., the occurs check fails).
This algorithm terminates if (i) all declaration checks reach a fixpoint or (ii) if at least one declaration fails the occurs check. By Lemma C.17 we know that either (i) or (ii) will eventually be satisfied, hence the algorithm always terminates.

T
C.19 (M ). If P ok and P nomono doesn't hold then P ◮ Ω with Ω finite.

P
. Direct consequence from Lemma C.17, considering the main function as a special case of a method declaration (with no type parameter).
P . By straightforward induction on the rules from Figure 17.

P
. Straightforward by the definitions for computation of instance sets and G.
. By induction definitions for computation of instance sets, G, F-closure and M-closure.

P
. By induction definitions for computation of instance sets, G, F-closure and M-closure.
If the derivation holds by rule <: S , then τ = σ = τ S . Since τ S [θ ] ∈ Ω and θ ⊢ τ S → t † we have that t † ok and conclude by the FG implements <: S rule.
We now proceed by a case analysis on the set of methods .m(ψ ) ∈ Ω}. If this set is empty, then in the monomorphisation of P (P † ), the type declaration for u † contains only the methods generated by the second premise of rule . Since τ [θ ] ∈ Ω, either τ is a struct type, and then we know that all its methods have a corresponding "dummy" analogue in P † and since methods ∆ (τ ) ⊇ methods ∆ (τ I ) then it must be the case that methods(t † ) ⊇ methods(u † ) and we conclude by the FG implements <: I rule. If τ is an interface type, the type declaration for t † contains at least the methods generated by the second premise of rule , and since methods ∆ (τ ) ⊇ methods ∆ (τ I ) it follows that methods(t † ) ⊇ methods(u † ) and we conclude by the FG implements <: I rule.
If the set M is not empty, then the declaration for u † contains the dummy version of all methods of τ I [θ ] and the monomorphisations of those in M (by rules , , and ). If τ is an interface type, since τ [θ ] ∈ Ω, M ⊆ Ω and ∅ ⊢ τ [θ ] <:τ I [θ ] by (Lemma C.5) then by I-closure each τ I [θ ].m(ψ ) ∈ Ω has a corresponding τ I [θ ] ′ .m(ψ ) ∈ Ω and so the type declaration for t † contains both the methods generated by the second premise of rule and all those corresponding to the monomorphisations of the methods of τ I [θ ] in M, and thus methods(t † ) ⊇ methods(u † ) and we conclude by the FG implements <: I rule. Finally, if τ is a struct type, we know that all its methods have a corresponding "dummy" analogue in P † for t † . Moreover, Since ∅ ⊢ τ [θ ] <: τ I [θ ] by (Lemma C.5), τ [θ ] ∈ Ω and M ⊂ Ω, by S-closure each τ I [θ ].m(ψ ) ∈ Ω has a corresponding τ [θ ].m(ψ ) ∈ Ω and so, since methods ∆ (τ ) ⊇ methods ∆ (τ I ) we have that by rule , methods(t † ) ⊇ methods(u † ) and we conclude by the FG implements <: I rule.

P
. Straightforward by definition of monomorphisation.
. By inversion on monomorphisation we have that P ◮ Ω, Ω ⊢ D → D, If T † is of the form struct{f t † }, by inversion we have that η ⊢ τ → t † . Since t(ϕ) ∈ Ω, by F-closure we have that τ [η] ∈ Ω. We show that can thus establish that type t † T † ok by showing distinct(f ) (since type t(Φ) T ∈ D and P ok) and by showing that t † ok (since τ [η] ∈ Ω, η ⊢ τ → t † and Ω ⊢ D → D).

P
. By induction on the derivation of ∅; x : τ ⊢ e : σ with case analysis on the last rule and a further case analysis on monomorphisation and instance generation. In the sequel we write Γ † for the FG typing context x : t † and Γ for the corresponding FGG typing context.
Since func (x t † S ) m † N † {return e † } ∈ D † then by inversion we know that the method definition arises from the first premise of or the second. If the latter, then m † N † = S † for some S † and e † = Top{}, with func (x t S (Φ)) m(Ψ)N {return e} ∈ D, t S (ϕ) ∈ Ω, η ⊢ t S (Φ) → t † S and η ⊢ m(Ψ)N → S † , with η = (Φ:=ϕ). We thus have that S † = m * () Top by inversion on η ⊢ m(Ψ)N → S † . Since t S (ϕ) ∈ Ω then t † S is declared in D † and well-formedness follows immediately.
We must show that t † S ok, t † ok, u † ok, distinct(x, x) and x : t † S , x : t † ⊢ e † : t with t <: u † . Since P ok and func (x t S (Φ)) m(Ψ)N {return e} ∈ D then we have that distinct(x, x). Since t S (ϕ).m(ψ ) ∈ Ω then by Lemma D.1, t S (ϕ) ∈ Ω, and so by Lemma D.8 it follows that t S ok. Similarly, by M-closure we know that τ [θ ] ∈ Ω and σ [θ ] ∈ Ω and thus by Lemma D.8 we have that t † ok and u † ok.
T D.11 (M ). If P ok and ⊢ P → P † then P † ok.

P
. Since P = D ⊲ d we have that P † = D † ⊲ d † , with P ◮ Ω, for some Ω. Since P ok we know that distinct(tdecls(D)) and distinct(mdecls(D)). By Lemmas D.10 and D.8 it follows that D † ok. We note that that distinct(tdecls(D † )) and distinct(mdecls(D † )) follows straightforwardly from the definitions of monomorphisation for names. Since ∅; ∅ ⊢ d : τ , for some τ , then by Lemma D.9 we have that ∅; ∅ ⊢ d † : t, with ⊢ τ → t, and so P † ok.
If the derivation holds from rule <: I then we have that t † 2 = t I , for some t I , and methods(t † 1 ) ⊇ methods(t I ). By the definition of monomorphisation, we know that τ 2 = τ I , for some τ I . Since τ 1 [η] ∈ Ω and τ 2 [η] ∈ Ω, and methods(t I ) contains at least as many (potentially dummy) elements as methods ∆ (τ I ), which are also in methods(t † 1 ). Since τ 2 [η] ∈ Ω then rules , and are such that all dummy methods of t I arise from all methods of τ 2 . If τ 1 is an interface type, by a similar reasoning we have that all dummy methods of t 1 , which contain all those of t 2 , arise from methods of τ 1 , and thus methods ∆ (τ 1 ) ⊇ methods ∆ (τ 2 ), and so ∆ ⊢ τ 1 <: τ 2 , by FGG implements rule <: I . If τ 1 is a struct type, then by rule , since τ 1 [η] ∈ Ω, we know that all dummy method implementations of t 1 (which include all methods declared for t 2 ) map from all the method declarations of τ 1 and so methods ∆ (τ 1 ) ⊇ methods ∆ (τ 2 ), and so ∆ ⊢ τ 1 <: τ 2 , by FGG implements rule <: I .
We now show that monomorphisation preserves and reflects reductions.
T E.5 (M ). Assume P = D ⊲ d, such that P ok and ⊢ P → D † ⊲ d † .
Then: (a) if d −→ e then there exists e † such that d † −→ e † and ∅ ⊢ e → e † ; (b) if d † −→ e ′ then there exists e such that d −→ e, ∅ ⊢ e → e † and e ′ = e † .

P
. Proof of (a): By induction on the derivation of d −→ e with a case analysis on the last reduction rule used.