149
Featherweight Go
ROBERT GRIESEMER, Google, USA
RAYMOND HU, University of Hertfordshire, UK
WEN KOKKE, University of Edinburgh, UK
JULIEN LANGE, Royal Holloway, University of London, UK
IAN LANCE TAYLOR, Google, USA
BERNARDO TONINHO, NOVA-LINCS, FCT-NOVA, Universidade Nova de Lisboa, Portugal
PHILIP WADLER, University of Edinburgh, UK
NOBUKO YOSHIDA, Imperial College London, UK
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.
CCS Concepts: • Theory of computation→ Program semantics; Type structures; • Software and its
engineering→ Polymorphism.
Additional Key Words and Phrases: Go, Generics, Monomorphisation
1 INTRODUCTION
Google introduced the Go programming language in 2009 [Griesemer et al. 2009; The Go Team
2020]. Today it sits at position 12 on the Tiobe Programming Language Index and position 10 on the
IEEE Spectrum Programming Language Ranking (Haskell sits at positions 41 and 29, respectively).
Recently, the Go team mooted a design to extend Go with generics [Taylor and Griesemer 2019],
and Rob Pike wrote Wadler to ask:
Would you be interested in helping us get polymorphism right (and/or figuring out
what “right” means) for some future version of Go?
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. Casts in Java correspond to type assertions in Go: casts in Java with generics are
Authors’ addresses: Robert Griesemer, Google, USA; Raymond Hu, University of Hertfordshire, School of Engineering and
Computer Science, Hatfield, UK, r.z.h.hu@herts.ac.uk; Wen Kokke, University of Edinburgh, Laboratory for Foundations of
Computer Science, Edinburgh, UK, wen.kokke@ed.ac.uk; Julien Lange, Royal Holloway, University of London, Department
of Computer Science, Egham, UK, julien.lange@rhul.ac.uk; Ian Lance Taylor, Google, USA; Bernardo Toninho, Departamento
de Informática, NOVA-LINCS, FCT-NOVA, Universidade Nova de Lisboa, Portugal, btoninho@fct.unl.pt; Philip Wadler,
University of Edinburgh, School of Informatics, Edinburgh, UK, wadler@inf.ed.ac.uk; Nobuko Yoshida, Imperial College
London, Computing, London, UK, n.yoshida@imperial.ac.uk.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and
the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2020 Copyright held by the owner/author(s).
2475-1421/2020/11-ART149
https://doi.org/10.1145/3428217
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:2 Griesemer et al.
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; 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 complete proofs are available in [Griesemer et al. 2020].
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 with generics. We had
to adjust our design: our first design for generics used nonvariant matching on bounds in receivers
of methods, but to solve The Expression Problem we had to relax this to covariant matching.
Monomorphisation. FGJ translates to FJ via erasure, whereas FGG translates to FG via monomor-
phisation. 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,
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:3
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 it is simple,
efficient, and the first design looked at by the Go team. Other designs offer other tradeoffs, e.g., the
restriction on a type assertion x.(a) could also be avoided by passing runtime representations of
types. This solution avoids exponential blowup and offers better support for separate compilation,
but at a cost in efficiency and complexity. We expect the final solution will involve a mix of both
monomorphisation and runtime representations of types, see Section 8 for more details.
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. (For example, Amin and Tate [2016] recently
showed that Java generics are unsound, but the bug is beyond the scope of
Featherweight Generic Java.)
We agree with these words. Since the reviewwas 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. The original proposal for generics in Go [Taylor and Griesemer 2019] was based on
contracts, which are syntactically convenient but lack a clear semantics. One result of our work is
that the new proposal [Taylor and Griesemer 2020] is based on interfaces, which are already well
defined in Go. After we submitted the draft of this paper, Griesemer wrote to Wadler:
I want to thank you and your team for all the type theory work on Go so far—it really
helped clarify our understanding to a massive degree. So thanks!
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 the future.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:4 Griesemer et al.
In this paper we adopt the syntax originally proposed by the Go team in July 2019 [Taylor and
Griesemer 2019]. In September 2020 [Taylor and Griesemer 2020], they proposed a revised syntax
where type parameters are declared within square brackets and the type keyword is omitted.
We prefer the new syntax, but retained the old since our artifact uses the old syntax and artifact
evaluation was already complete.
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.
Additional examples and details of all proofs are available in [Griesemer et al. 2020].
2 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. We show how to declare booleans in FG and FGG in [Griesemer et al. 2020].
2.1 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 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 Anywhere a boolean is expected, so the type assertion .(bool) is required.
Bound variable names are irrelevant when comparing method signatures, but method names and
type names must match exactly. For example, the following signatures are considered equivalent:
Apply(x Any) Any Apply(arg Any) Any
Equality in FG. Figure 2 shows equality in FG.
Interface Eq has one method with signature Equal(that Eq) bool. If a type implements this interface
we say it supports equality.
A type 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.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:5
type Any interface {}
type Function interface {
Apply(x Any) Any
}
type incr struct { n int }
func (this incr) Apply(x Any) Any {
return x.(int) + this.n
}
type pos struct {}
func (this pos) Apply(x Any) Any {
return x.(int) > 0
}
type compose struct {
f Function
g Function
}
func (this compose) Apply(x Any) Any {
return this.g.Apply(this.f.Apply(x))
}
func main() {
var f Function = compose{incr{-5},pos{}}
var _ bool = f.Apply(3).(bool) // false
}
Fig. 1. Functions in FG
type Eq interface {
Equal(that Eq) bool
}
type Int int
func (this Int) Equal(that Eq) bool {
return this == that.(Int)
}
type Pair struct {
left Eq
right Eq
}
func (this Pair) Equal(that Eq) bool {
return this.left.Equal(that.(Pair).left) &&
this.right.Equal(that.(Pair).right)
}
func main() {
var i, j Int = 1, 2
var p Pair = Pair{i, j}
var _ bool = p.Equal(p) // true
}
Fig. 2. Equality in FG
type List interface {
Map(f Function) List
}
type Nil struct {}
type Cons struct {
head Any
tail List
}
func (xs Nil) Map(f Function) List {
return Nil{}
}
func (xs Cons) Map(f Function) List {
return Cons{f.Apply(xs.head), xs.tail.Map(f)}
}
func main() {
var xs List = Cons{3, Cons{6, Nil{}}}
var ys List = xs.Map(incr{-5})
// Cons{-2, Cons{1, Nil{}}}
var _ List = ys.Map(pos{})
// Cons{false, Cons{true, Nil{}}}
}
Fig. 3. Lists in FG
A second type declaration introduces the structure Pair with two fields left and right which may
be of any type that supports equality, and the method declaration ensures that pairs themselves
support equality. Again, the argument has type Eq and the body uses a type assertion to convert it
to a Pair as required. The top level main method builds a pair of integers and compares it to itself
for equality, yielding true.
Since pairs are to support equality, their components are also required to support equality. In
general, if a structure is to satisfy some interface we may need to require that each field of that
structure satisfies the same interface—a property we refer to as type pollution. An alternative design
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:6 Griesemer et al.
would give fields the type Any, and to replace this.left by this.left.(Eq), and similarly for the
other component. The alternative design is more flexible—it permits fields of the pair to have any
type—but is less efficient (the type assertions must be checked at runtime) and less reliable (the
type assertions may fail). As we will see, FGG will let us avoid type pollution, providing flexibility,
efficiency, and reliability all at the same time.
Lists in FG. Figure 3 shows lists in FG.
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 laid 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 the 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
type Cons struct { head Any; tail List }
where the tail field of type List may itself contain a Cons, since Cons implements interface List.
2.2 FGG by Example
We now adapt the examples of the previous section to generics.
Functions in FGG. Figure 4 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. Here 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.
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 main method, type param-
eters are added and the type assertion at the end is no longer required.
Equality in FGG. Figure 5 shows equality 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 has signature Equal(that a) bool. 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].
Since we use a type parameter for the argument to Equal, in the method declaration for Int the
argument must now have type Int instead of type Eq. A type assertion in the method body is no
longer required, increasing efficiency and reliability.
The type declaration for Pair now take two type parameters, a and b, which are both bounded by
Any. The method declaration for equality on pairs also uses two type parameters, a and b, bounded
by Eq(a) and Eq(b) respectively, so the call to Equality on the components of the pair is permitted.
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
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:7
type Function(type a Any, b Any) interface {
Apply(x a) b
}
type incr struct { n int }
func (this incr) Apply(x int) int {
return x + this.n
}
type pos struct {}
func (this pos) Apply(x int) bool {
return x > 0
}
type compose(type a Any, b Any, c Any) struct {
f Function(a, b)
g Function(b, c)
}
func (this compose(type a Any, b Any, c Any))
Apply(x a) c {
return this.g.Apply(this.f.Apply(x))
}
func main() {
var f Function(int,bool) =
compose(int,int,bool){incr{-5},pos{}}
var _ bool = f.Apply(3) // false
}
Fig. 4. Functions in FGG
type Eq(type a Eq(a)) interface {
Equal(that a) bool
}
type Int int
func (this Int) Equal(that Int) bool {
return this == that
}
type Pair(type a Any, b Any) struct {
left a
right b
}
func (this Pair(type a Eq(a), b Eq(b)))
Equal(that Pair(a,b)) bool {
return this.left.Equal(that.left) &&
this.right.Equal(that.right)
}
func main() {
var i, j Int = 1, 2
var p Pair(Int, Int) = Pair(Int, Int){i, j}
var _ bool = p.Equal(p) // true
}
Fig. 5. Equality in FGG
type List(type a Any) interface {
Map(type b Any)(f Function(a, b)) List(b)
}
type Nil(type a Any) struct {}
type Cons(type a Any) struct {
head a
tail List(a)
}
func (xs Nil(type a Any))
Map(type b Any)(f Function(a,b)) List(b) {
return Nil(b){}
}
func (xs Cons(type a Any))
Map(type b Any)(f Function(a,b)) List(b) {
return Cons(b)
{f.Apply(xs.head), xs.tail.Map(b)(f)}
}
func main() {
var xs List(int) =
Cons(int){3, Cons(int){6, Nil(int){}}}
var ys List(int) = xs.Map(int)(incr{-5})
var _ List(bool) = ys.Map(bool)(pos{})
}
Fig. 6. Lists in FGG
type Edge(type e Edge(e,v),
v Vertex(e,v)) interface {
Source() v
Target() v
}
type Vertex(e Edge(e,v),
v Vertex(e,v)) interface {
Edges() List(e)
}
Fig. 7. Mutually recursive bounds
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:8 Griesemer et al.
covariant). This is in contrast to method signatures, which must exactly match the signature in the
interface (signatures are nonvariant). In this case, the bounds on a and b in the type declaration for
pairs are both Any, while the bounds on a and b in the receiver are Eq(a) and Eq(b). By covariance,
since Eq(a) and Eq(b) implement Any, the method declaration is allowed.
The Go team’s current design does not support covariant receiver typing. Instead, receivers are
nonvariant, just like method signatures. With that design, the bounds on a and b in the declaration
for pairs must exactly match those in the method receiver. Either the type and method declarations
must both use bounds Eq(a) and Eq(b) (in which case one cannot have pairs where the components
do not support equality, even if don’t need that pair to itself support equality, reintroducing type
pollution and reducing flexibility), or they must both use bounds Any (in which case the method
body will need to add type assertions to Eq(a) and Eq(b), reducing efficiency and reliability).
Lists in FGG. Figure 6 shows lists in FGG.
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 b Any)(f Function(a, b)) List(b) 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. This is a form of type pollution.
An alternative design that avoids pollution, based on our solution to The Expression Problem, can
be found in [Griesemer et al. 2020].
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 7 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.
2.3 The Expression Problem
Following Wadler [1998], we present The Expression Problem pared to a minimum. Our solution
appears in Figure 8. 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:
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:9
// Eval on Num
type Evaler interface {
Eval() int
}
type Num struct {
value int
}
func (e Num) Eval() int {
return e.value
}
// Eval on Plus
type Plus(type a Any) struct {
left a
right a
}
func (e Plus(type a Evaler)) Eval() int {
return e.left.Eval() + e.right.Eval()
}
// String on Num
type Stringer interface {
String() string
}
func (e Num) String() string {
return fmt.Sprintf("%d", e.value)
}
// String on Plus
func (e Plus(type a Stringer)) String() string {
return fmt.Sprintf("(%s+%s)",
e.left.String(), e.right.String())
}
// tie it all together
type Expr interface {
Evaler
Stringer
}
func main() {
var e Expr = Plus(Expr){Num{1}, Num{2}}
var _ Int = e.Eval() // 3
var _ string = e.String() // "(1+2)"
}
Fig. 8. Expression problem in FGG
(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. (The naming convention is typical of Go.) 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. Note this depends
crucially on FGG’s support for covariant receivers in method declarations. Since the bounds or
the receivers in the method declarations, Evaler and Stringer, implement the bounds in the type
declarations, Any, the method declarations are allowed.
A last step shows how to tie it all together. We define an interface Expr embedding Evaler and
Stringer, and show how to build an Expr value which we can 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
violates the requirement 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 Stringer before the
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:10 Griesemer et al.
type Top struct {}
type Function<int,int> interface {
Apply<0> Top
Apply(x int) int
}
type incr struct { n int }
func (this incr) Apply<0> Top {
return Top{}
}
func (this incr) Apply(x int) int {
return x + this.n
}
type Function<int,bool> interface {
Apply<1> Top
Apply(x int) bool
}
type pos struct {}
func (this pos) Apply<1> Top {
return Top{}
}
func (this pos) Apply(x int) bool {
return x > 0
}
type List<int> interface {
Map<2>() Top
Map<int>(f Function<int,int>) List<int>
Map<bool>(f Function<int,bool>) List<bool>
}
type Nil<int> struct {}
type Cons<int> struct {
head int
tail List<int>
}
func (xs Nil<int>) Map<2>() Top {
return Top{}
}
func (xs Cons<int>) Map<2>() Top {
return Top{}
}
func (xs Nil<int>)
Map<int>(f Function<int,int>) List<int> {
return Nil<int>{}
}
func (xs Cons<int>)
Map<int>(f Function<int,int>) List<int> {
return Cons<int>
{f.Apply(xs.head), xs.tail.Map<int>(f)}
}
func (xs Nil<int>)
Map<bool>(f Function<int,bool>) List<bool> {
return Nil<bool>{}
}
func (xs Cons<int>)
Map<bool>(f Function<int,bool>) List<bool> {
return Cons<bool>
{f.Apply(xs.head), xs.tail.Map<bool>(f)}
}
type List<bool> interface {
Map<3>() Top
}
type Nil<bool> struct {}
type Cons<bool> struct {
head bool
tail List<bool>
}
func (xs Nil<bool>) Map<3>() Top {
return Top{}
}
func (xs Cons<bool>) Map<3>() Top {
return Top{}
}
func main() {
var xs List<int> =
Cons<int>{3, Cons<int>{6, Nil<int>}}
var ys List<int> = xs.Map<int>(incr{-5})
var _ List<bool> = ys.Map<bool>(pos{})
}
Fig. 9. Monomorphisation: example of FG translation
type Box(type a Any) struct {
value a
}
func (this Box(type a Any)) Nest(n int) Any {
if (n == 0) { return this }
else { return Box(Box(a)){this}.Nest(n-1) }
}
Fig. 10. FGG code that cannot be monomorphised
recursive calls; that allows us to add operations later, but violates the requirement that all types be
checked statically.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:11
2.4 Monomorphisation by example
We translate FGG into FG viamonomorphisation. As an example, consider the FGG code in Figures 4
and 6. 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 9.
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 source 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 incr{1} then the type assertion f.(List<bool>) should fail;
but without the dummy, interface List<bool> would have no methods and hence any structure or
interface would implement it.
Monomorphisation yields specialised type declarations for structures and interfaces, and spe-
cialised method declarations, plus the required dummymethods. 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 10 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 11 presents FG syntax. We let 𝑓 range over field names,𝑚 range over method names, 𝑥
range over variable names, 𝑡𝑆 , 𝑢𝑆 range over structure names, and 𝑡𝐼 , 𝑢𝐼 range over interface names.
We let 𝑡,𝑢 range over type names, which are either structure or interface type names. We let 𝑑
and 𝑒 range over expressions, which have five forms: variable 𝑥 , method call 𝑒.𝑚(𝑒), structure literal
𝑡𝑆{𝑒}, selection 𝑒.𝑓 , and type assertion 𝑒.(𝑡). By convention, 𝑒 stands for the sequence 𝑒1, . . . , 𝑒𝑛 .
We consider 𝑒 and 𝑒 to be distinct metavariables.
A method signature𝑀 has the form (𝑥 𝑡) 𝑡 . Here 𝑥 stands for 𝑥1, . . . , 𝑥𝑛 and 𝑡 stands for 𝑡1, . . . , 𝑡𝑛 ,
and hence 𝑥 𝑡 stands for 𝑥1 𝑡1, . . . , 𝑥𝑛 𝑡𝑛 . We use similar conventions extensively.
A method specification 𝑆 is a method name followed by a method signature. A type literal
𝑇 is either a structure struct {𝑓 𝑡} or an interface interface {𝑆}. A declaration 𝐷 is either a
type declaration type 𝑡 𝑇 or a method declaration func (𝑥 𝑡𝑆 ) 𝑚𝑀 {return 𝑒}. In our examples,
interface declarationsmay 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.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:12 Griesemer et al.
Field name 𝑓
Method name 𝑚
Variable name 𝑥
Structure type name 𝑡𝑆 , 𝑢𝑆
Interface type name 𝑡𝐼 , 𝑢𝐼
Type name 𝑡,𝑢 ::= 𝑡𝑆 | 𝑡𝐼
Method signature 𝑀 ::= (𝑥 𝑡) 𝑡
Method specification 𝑆 ::=𝑚𝑀
Type Literal 𝑇 ::=
Structure struct {𝑓 𝑡}
Interface interface {𝑆}
Declaration 𝐷 ::=
Type declaration type 𝑡 𝑇
Method declaration func (𝑥 𝑡𝑆 ) 𝑚𝑀 {return 𝑒}
Program 𝑃 ::= package main; 𝐷 func main() {_ = 𝑒}
Expression 𝑑, 𝑒 ::=
Variable 𝑥
Method call 𝑒.𝑚(𝑒)
Structure literal 𝑡𝑆{𝑒}
Select 𝑒.𝑓
Type assertion 𝑒.(𝑡)
Fig. 11. FG syntax
A program 𝑃 consists of a sequence of declarations 𝐷 and a top-level expression 𝑒 , written in the
stylised form shown in the figure to make it legal Go. We sometimes abbreviate it as 𝐷 ▷ 𝑒 .
3.2 Auxiliary functions
Figure 12 presents several auxiliary definitions. All definitions assume a given program with a fixed
sequence of declarations 𝐷 .
Function fields(𝑡𝑆 ) looks up the structure declaration for 𝑡𝑆 and returns a sequence (𝑓 𝑡) of field
names and their types. Write 𝑡𝑆 .𝑚 to refer to the method declaration with receiver type 𝑡𝑆 and
name𝑚. Function body(𝑡𝑆 .𝑚) returns (𝑥 : 𝑡𝑆 , 𝑥 : 𝑡).𝑒 , where 𝑥 : 𝑡𝑆 is the receiver parameter and
its type, 𝑥 : 𝑡 the argument parameters and their types, and 𝑒 the body from the declaration of a
method with receiver of type 𝑡𝑆 and name𝑚. In the phrase func (𝑥 𝑡𝑆 )𝑚(𝑥 𝑡) 𝑡 , each of 𝑡𝑆 , 𝑡 , and 𝑡
is considered a distinct metavariable, and similarly for 𝑥 and 𝑥 .
Function type(𝑣) is explained in Section 3.4. Predicate unique(𝑆) holds if for every method
specification𝑚𝑀 in 𝑆 the method name𝑚 uniquely determines the method signature𝑀 .
Function tdecls(𝐷) returns a sequence with the name of every type declared in 𝐷 . Function
mdecls(𝐷) returns a sequence with a pair 𝑡𝑆 .𝑚 for every method declared in 𝐷 . Predicate distinct,
not defined in the figure, takes a sequence, and holds if no item in the sequence is duplicated. We
are careful to distinguish between sets and sequences. Predicate distinct must take a sequence
rather than 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 parameters
are ignored; signatures are considered equal if they contain the same types in the same sequence.
Function methods(𝑡) returns the set of all method specifications belonging to type 𝑡 . If 𝑡 is a
structure type the method specifications are those from the method declarations with a receiver of
the given type. It 𝑡 is an interface type, the method specifications are those given in the interface.
Figure 13 presents the FG typing rules. Let Γ range over environments, which are sequences of
variables paired with type names, 𝑥 : 𝑡 . We write ∅ for the empty environment.
Judgement 𝑡 <: 𝑢 holds if type 𝑡 implements type 𝑢. A structure type 𝑡𝑆 is only implemented by
itself, while type 𝑡 implements interface type 𝑡𝐼 if the methods defined on 𝑡 are a superset of those
defined on 𝑡𝐼 . It follows from the definition that <: is reflexive and transitive.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:13
(type 𝑡𝑆 struct{𝑓 𝑡}) ∈ 𝐷
fields(𝑡𝑆 ) = 𝑓 𝑡
(func (𝑥 𝑡𝑆 ) 𝑚(𝑥 𝑡) 𝑡 {return 𝑒}) ∈ 𝐷
body(𝑡𝑆 .𝑚) = (𝑥 : 𝑡𝑆 , 𝑥 : 𝑡).𝑒
type(𝑡𝑆{𝑣}) = 𝑡𝑆
𝑚𝑀1,𝑚𝑀2 ∈ 𝑆 implies𝑀1 = 𝑀2
unique(𝑆)
tdecls(𝐷) = [𝑡 | (type 𝑡 𝑇 ) ∈ 𝐷] mdecls(𝐷) = [𝑡𝑆 .𝑚 | (func (𝑥 𝑡𝑆 ) 𝑚𝑀 {return 𝑒}) ∈ 𝐷]
methods(𝑡𝑆 ) = {𝑚𝑀 | (func (𝑥 𝑡𝑆 ) 𝑚𝑀 {return 𝑒}) ∈ 𝐷}
type 𝑡𝐼 interface{𝑆} ∈ 𝐷
methods(𝑡𝐼 ) = 𝑆
Fig. 12. FG auxiliary functions
3.3 FG Typing
We write ok to indicate a construct is well-formed. Judgement 𝑡 ok holds if type 𝑡 is declared.
Judgement 𝑆 ok holds if method specification 𝑆 is well formed: all formal parameters 𝑥 in it are
distinct, and all the types 𝑡, 𝑡 in it are declared. Judgement𝑇 ok holds if type literal𝑇 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 𝐷 ok holds if declaration 𝐷 is well formed: for a
type declaration, its type literal must be well formed; for a method declaration, its receiver and
formal parameters 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.
Judgement Γ ⊢ 𝑒 : 𝑡 holds if in environment Γ expression 𝑒 has type 𝑡 . Rules for variable, method
call, structure literal, and field selection are straightforward. For instance, the four hypotheses for a
method call check the type of the receiver, check the types of the arguments, look up the signature
of the method, and confirm the types of the arguments implement the types of the parameters.
Type assertions are more interesting. A type assertion 𝑒.(𝑡) always returns a value of type 𝑡
(if it doesn’t panic). Let 𝑒 have type 𝑢. There are three cases. If 𝑢 and 𝑡 are both interface types
(t-assert𝐼 ) then the assertion is always allowed, since 𝑒 could always conceivably evaluate to a
structure that implements 𝑡 . If 𝑢 is an interface but 𝑡 is a structure (t-assert𝑆 ) then the assertion is
allowed only if 𝑡 implements 𝑢, since otherwise 𝑒 could not possibly contain a structure of type 𝑡 .
If 𝑢 is a structure type (t-stupid) then it is stupid to write the assertion in source code, since 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 type, so without such stupid type
assertions an expression would become ill-typed during reduction. We write a box around this rule
to indicate that it doesn’t apply to source terms, but may apply to terms that result from reducing
the source. Stupid type assertions are similar to stupid casts as found in Featherweight Java.
Judgement 𝑃 ok holds if program 𝑃 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.
3.4 FG Reduction
Figure 14 presents the FG reduction rules. A value 𝑣 is a structure literal 𝑡𝑆{𝑣} where each field
is itself filled with a value. The auxiliary function type(𝑣) returns 𝑡𝑆 when 𝑣 = 𝑡𝑆{𝑣}. Evaluation
contexts 𝐸 are defined in the usual way. Judgement 𝑑 −→ 𝑒 holds if expression 𝑑 steps to expression
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:14 Griesemer et al.
Implements, well-formed type 𝑡 <: 𝑢 𝑡 ok
<:𝑆
𝑡𝑆 <: 𝑡𝑆
<:𝐼
methods(𝑡) ⊇ methods(𝑡𝐼 )
𝑡 <: 𝑡𝐼
t-named
(type 𝑡 𝑇 ) ∈ 𝐷
𝑡 ok
Well-formed method specifications and type literals 𝑆 ok 𝑇 ok
t-specification
distinct (𝑥) 𝑡 ok 𝑡 ok
𝑚(𝑥 𝑡) 𝑡 ok
t-struct
distinct (𝑓 ) 𝑡 ok
struct {𝑓 𝑡} ok
t-interface
unique(𝑆) 𝑆 ok
interface {𝑆} ok
Well-formed declarations 𝐷 ok
t-type
𝑇 ok
type 𝑡 𝑇 ok
t-func
distinct (𝑥, 𝑥)
𝑡𝑆 ok 𝑡 ok 𝑢 ok 𝑥 : 𝑡𝑆 , 𝑥 : 𝑡 ⊢ 𝑒 : 𝑡 𝑡 <: 𝑢
func (𝑥 𝑡𝑆 ) 𝑚(𝑥 𝑡) 𝑢 {return 𝑒} ok
Expressions Γ ⊢ 𝑒 : 𝑡
t-var
(𝑥 : 𝑡) ∈ Γ
Γ ⊢ 𝑥 : 𝑡
t-call
Γ ⊢ 𝑒 : 𝑡 Γ ⊢ 𝑒 : 𝑡 (𝑚(𝑥 𝑢) 𝑢) ∈ methods(𝑡) 𝑡 <: 𝑢
Γ ⊢ 𝑒.𝑚(𝑒) : 𝑢
t-literal
𝑡𝑆 ok Γ ⊢ 𝑒 : 𝑡 (𝑓 𝑢) = fields(𝑡𝑆 ) 𝑡 <: 𝑢
Γ ⊢ 𝑡𝑆{𝑒} : 𝑡𝑆
t-field
Γ ⊢ 𝑒 : 𝑡𝑆 (𝑓 𝑢) = fields(𝑡𝑆 )
Γ ⊢ 𝑒.𝑓𝑖 : 𝑢𝑖
t-assert𝐼
𝑡𝐼 ok Γ ⊢ 𝑒 : 𝑢𝐼
Γ ⊢ 𝑒.(𝑡𝐼 ) : 𝑡𝐼
t-assert𝑆
𝑡𝑆 ok Γ ⊢ 𝑒 : 𝑢𝐼 𝑡𝑆 <: 𝑢𝐼
Γ ⊢ 𝑒.(𝑡𝑆 ) : 𝑡𝑆
t-stupid
𝑡 ok Γ ⊢ 𝑒 : 𝑢𝑆
Γ ⊢ 𝑒.(𝑡) : 𝑡
Programs 𝑃 ok
t-prog
distinct (tdecls(𝐷)) distinct (mdecls(𝐷)) 𝐷 ok ∅ ⊢ 𝑒 : 𝑡
package main; 𝐷 func main() {_ = 𝑒} ok
Fig. 13. FG typing
𝑒 . There are four rules, for field selection, method call, type assertion, and closure under evaluation
contexts. All are straightforward.
3.5 FG properties
We have the usual results relating typing and reduction.
Lemma 3.1 (Well formed). If Γ ⊢ 𝑒 : 𝑡 then 𝑡 ok.
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.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:15
Value 𝑣 ::= 𝑡𝑆{𝑣}
Evaluation context 𝐸 ::=
Hole □
Method call receiver 𝐸.𝑚(𝑒)
Method call arguments 𝑣 .𝑚(𝑣, 𝐸, 𝑒)
Structure 𝑡𝑆{𝑣, 𝐸, 𝑒}
Select 𝐸.𝑓
Type assertion 𝐸.(𝑡)
Reduction 𝑑 −→ 𝑒
r-field
(𝑓 𝑡) = fields(𝑡𝑆 )
𝑡𝑆{𝑣}.𝑓𝑖 −→ 𝑣𝑖
r-call
(𝑥 : 𝑡𝑆 , 𝑥 : 𝑡).𝑒 = body(type(𝑣).𝑚)
𝑣 .𝑚(𝑣) −→ 𝑒 [𝑥 := 𝑣, 𝑥 := 𝑣]
r-assert
type(𝑣) <: 𝑡
𝑣 .(𝑡) −→ 𝑣
r-context
𝑑 −→ 𝑒
𝐸 [𝑑] −→ 𝐸 [𝑒]
Fig. 14. FG reduction
Lemma 3.2 (Substitution). If ∅ ⊢ 𝑣 : 𝑡 and 𝑥 : 𝑢 ⊢ 𝑒 : 𝑢 and 𝑡 <: 𝑢 then ∅ ⊢ 𝑒 [𝑥 := 𝑣] : 𝑡 for some
type 𝑡 with 𝑡 <: 𝑢.
The following are straightforward adaptions of the usual results. We say expression 𝑒 panics if
there exist evaluation context 𝐸, value 𝑣 , and type 𝑡 such that 𝑒 = 𝐸 [𝑣 .(𝑡)] and type(𝑣) ≮: 𝑡 .
Theorem 3.3 (Preservation). If ∅ ⊢ 𝑑 : 𝑢 and 𝑑 −→ 𝑒 then ∅ ⊢ 𝑒 : 𝑡 for some 𝑡 with 𝑡 <: 𝑢.
Theorem 3.4 (Progress). If ∅ ⊢ 𝑑 : 𝑢 then either 𝑑 is a value, 𝑑 −→ 𝑒 for some 𝑒 , or 𝑑 panics.
4 FEATHERWEIGHT GENERIC GO
4.1 FGG Syntax
Figure 15 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 𝑡 (𝜏). We also let 𝜏𝑆 , 𝜎𝑆 range over structure types of the form 𝑡𝑆 (𝜏); 𝜏𝐼 , 𝜎𝐼 range over interface
types of the form 𝑡𝐼 (𝜏); and, 𝜏𝐽 , 𝜎𝐽 range over types that are either type parameters or interfaces 𝜏𝐼 .
Expressions and declarations are updated to replace type names by types, and method calls are
updated to include type parameters: a structure declaration is now struct {𝑓 𝜏} and a method call
is now 𝑒.𝑚(𝜏) (𝑒), a structure literal is now 𝜏𝑆{𝑒}, and a type assertion is now 𝑒.(𝜏).
We let Φ,Ψ range over type formals, which have the form type 𝛼 𝜏𝐼 , pairing type parameters
with their bounds, which are interface types. The bounds in type formals are mutually recursive, i.e.,
each interface in 𝜏𝐼 may refer to any parameter in 𝛼 . Type declarations type 𝑡 (Φ) 𝑇 , and signatures
(Ψ) (𝑥 𝜏) 𝜏 , and method declarations func (𝑥 𝑡𝑆 (Φ)) 𝑚𝑀 {return 𝑒} now include type formals.
We let 𝜙,𝜓 range over type actuals, which are sequences of types.
4.2 Auxiliary functions
Figure 16 presents several auxiliary definitions. As before, Γ ranges over environments, which are
now sequences that pair variables with types, 𝑥 : 𝜏 . In addition, Δ ranges over type environments,
which are sequences that pair type parameters with bounds, 𝛼 : 𝜏𝐼 . 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 corresponding premise does not hold. We
write Φˆ for the type parameters of Φ.
Functions fields(𝜏𝑆 ) and body(𝜏𝑆 .𝑚(𝜓 )) 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
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:16 Griesemer et al.
Field name 𝑓
Method name 𝑚
Variable name 𝑥
Structure type name 𝑡𝑆 , 𝑢𝑆
Interface type name 𝑡𝐼 , 𝑢𝐼
Type name 𝑡,𝑢 ::= 𝑡𝑆 | 𝑡𝐼
Type parameter 𝛼
Method signature 𝑀 ::= (Ψ) (𝑥 𝜏) 𝜏
Method specification 𝑆 ::=𝑚𝑀
Type Literal 𝑇 ::=
Structure struct {𝑓 𝜏}
Interface interface {𝑆}
Declaration 𝐷 ::=
Type declaration type 𝑡 (Φ) 𝑇
Method declaration func (𝑥 𝑡𝑆 (Φ)) 𝑚𝑀 {return 𝑒}
Program 𝑃 ::= package main; 𝐷 func main() {_ = 𝑒}
Type 𝜏, 𝜎 ::=
Type parameter 𝛼
Named type 𝑡 (𝜏)
Structure type 𝜏𝑆 , 𝜎𝑆 ::= 𝑡𝑆 (𝜏)
Interface type 𝜏𝐼 , 𝜎𝐼 ::= 𝑡𝐼 (𝜏)
Interface-like type 𝜏𝐽 , 𝜎𝐽 ::= 𝛼 | 𝜏𝐼
Type formal Φ, Ψ ::= type 𝛼 𝜏𝐼
Type actual 𝜙 ,𝜓 ::= 𝜏
Expression 𝑒 ::=
Variable 𝑥
Method call 𝑒.𝑚(𝜏) (𝑒)
Structure literal 𝜏𝑆{𝑒}
Select 𝑒.𝑓
Type assertion 𝑒.(𝜏)
Fig. 15. FGG syntax
which are instantiated appropriately. Functions type, tdecls, and mdecls and predicate unique are
updated to replace type names by types and to 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 𝜏 .
4.3 FGG Typing
Figure 17 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 type arguments that satisfy the bounds of the
corresponding type parameters. Judgement Δ ⊢ 𝜙 ok holds if under environment Δ all types in 𝜙
are well formed.
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.
Judgement Φ ⊢ 𝑆 ok holds if under type environment Φ method specification 𝑆 is well formed: it
requires Φ,Ψ ok Δ where Ψ is the type formals of the method specification, and the rest is similar
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:17
(type 𝛼 𝜏𝐼 ) = Φ 𝜂 = (𝛼 := 𝜏)
(Φ := 𝜏) = 𝜂
(type 𝛼 𝜏𝐼 ) = Φ 𝜂 = (Φ := 𝜙) Δ ⊢ (𝛼 <: 𝜏𝐼 ) [𝜂]
(Φ :=Δ 𝜙) = 𝜂
(type 𝑡𝑆 (Φ) struct {𝑓 𝜏}) ∈ 𝐷 𝜂 = (Φ := 𝜙)
fields(𝑡𝑆 (𝜙)) = (𝑓 𝜏) [𝜂]
(func (𝑥 𝑡𝑆 (Φ)) 𝑚(Ψ) (𝑥 𝜏) 𝜏 {return 𝑒}) ∈ 𝐷 𝜃 = (Φ,Ψ := 𝜙,𝜓 )
body(𝑡𝑆 (𝜙).𝑚(𝜓 )) = (𝑥 : 𝑡𝑆 (𝜙), 𝑥 : 𝜏).𝑒 [𝜃 ]
(type 𝛼 𝜏𝐼 ) = Φ
Φˆ = 𝛼
type(𝜏𝑆{𝑣}) = 𝜏𝑆
𝑚𝑀1,𝑚𝑀2 ∈ 𝑆 implies𝑀1 = 𝑀2
unique(𝑆)
tdecls(𝐷) = [𝑡 | (type 𝑡 (Φ) 𝑇 ) ∈ 𝐷]
mdecls(𝐷) = [𝑡𝑆 .𝑚 | (func (𝑥 𝑡𝑆 (Φ)) 𝑚𝑀 {return 𝑒}) ∈ 𝐷]
(𝛼 : 𝜏𝐼 ) ∈ Δ
boundsΔ (𝛼) = 𝜏𝐼
boundsΔ (𝜏𝑆 ) = 𝜏𝑆 boundsΔ (𝜏𝐼 ) = 𝜏𝐼
methodsΔ (𝑡𝑆 (𝜙)) = {(𝑚𝑀) [𝜂] | (func (𝑥 𝑡𝑆 (Φ)) 𝑚𝑀 {return 𝑒}) ∈ 𝐷, 𝜂 = (Φ :=Δ 𝜙)}
type 𝑡𝐼 (Φ) interface {𝑆} ∈ 𝐷 𝜂 = (Φ := 𝜙)
methodsΔ (𝑡𝐼 (𝜙)) = 𝑆 [𝜂]
(𝛼 : 𝜏𝐼 ) ∈ Δ
methodsΔ (𝛼) = methodsΔ (𝜏𝐼 )
Fig. 16. FGG auxiliary functions
to before but now under type environment Δ. Judgement Φ ⊢ 𝑇 ok holds if under type formals Φ
type literal 𝑇 is well formed, and again is a straightforward adjustment of its earlier definition.
Judgement 𝐷 ok holds if declaration 𝐷 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 Δ; Γ ⊢ 𝑒 : 𝜏 holds if under type environment Δ and environment Γ expression 𝑒 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.
4.4 FGG Reduction
Figure 18 presents the FGG reduction rules.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:18 Griesemer et al.
Implements Δ ⊢ 𝜏 <: 𝜎 Φ <: Ψ
<:-param
Δ ⊢ 𝛼 <: 𝛼
<:𝑆
Δ ⊢ 𝜏𝑆 <: 𝜏𝑆
<:𝐼
methodsΔ (𝜏) ⊇ methodsΔ (𝜏𝐼 )
Δ ⊢ 𝜏 <: 𝜏𝐼
<:-formals
∅ ⊢ 𝜏𝐼 <: 𝜎𝐼
(type 𝛼 𝜏𝐼 ) <: (type 𝛼 𝜎𝐼 )
Well-formed type and actuals Δ ⊢ 𝜏 ok Δ ⊢ 𝜙 ok
t-param
(𝛼 : 𝜏𝐼 ) ∈ Δ
Δ ⊢ 𝛼 ok
t-named
Δ ⊢ 𝜙 ok (type 𝑡 (Φ) 𝑇 ) ∈ 𝐷 𝜂 = (Φ :=Δ 𝜙)
Δ ⊢ 𝑡 (𝜙) ok
t-actual
𝜏 = 𝜙 Δ ⊢ 𝜏 ok
Δ ⊢ 𝜙 ok
Well-formed type formals and nested formals Φ ⊢ Ψ ok Φ; Ψ ok Δ
t-formal
(type 𝛼 𝜏𝐼 ) = Ψ distinct (Φˆ, 𝛼) Φ,Ψ ⊢ 𝜏𝐼 ok
Φ ⊢ Ψ ok
t-nested
∅ ⊢ Φ ok Φ ⊢ Ψ ok Δ = Φ,Ψ
Φ; Ψ ok Δ
Well-formed method specifications and type literals Φ ⊢ 𝑆 ok Φ ⊢ 𝑇 ok
t-specification
Φ; Ψ ok Δ
distinct (𝑥) Δ ⊢ 𝜏 ok Δ ⊢ 𝜏 ok
Φ ⊢𝑚(Ψ) (𝑥 𝜏) 𝜏 ok
t-struct
distinct (𝑓 ) Φ ⊢ 𝜏 ok
Φ ⊢ struct {𝑓 𝜏} ok
t-interface
unique(𝑆) Φ ⊢ 𝑆 ok
Φ ⊢ interface {𝑆}
Well-formed declarations 𝐷 ok
t-type
∅ ⊢ Φ ok Φ ⊢ 𝑇 ok
type 𝑡 (Φ) 𝑇 ok
t-func
distinct (𝑥, 𝑥) (type 𝑡𝑆 (Φ′) 𝑇 ) ∈ 𝐷 Φ <: Φ′ Φ; Ψ ok Δ
Δ ⊢ 𝜏 ok Δ ⊢ 𝜎 ok Δ; 𝑥 : 𝑡𝑆 (Φˆ), 𝑥 : 𝜏 ⊢ 𝑒 : 𝜏 Δ ⊢ 𝜏 <: 𝜎
func (𝑥 𝑡𝑆 (Φ)) 𝑚(Ψ) (𝑥 𝜏) 𝜎 {return 𝑒} ok
Expressions Δ; Γ ⊢ 𝑒 : 𝜏 <
t-var
(𝑥 : 𝜏) ∈ Γ
Δ; Γ ⊢ 𝑥 : 𝜏
t-call
(𝑚(Ψ) (𝑥 𝜎) 𝜎) ∈ methodsΔ (𝜏)
Δ; Γ ⊢ 𝑒 : 𝜏 Δ; Γ ⊢ 𝑒 : 𝜏 𝜂 = (Ψ :=Δ 𝜓 ) Δ ⊢ (𝜏 <: 𝜎) [𝜂]
Δ; Γ ⊢ 𝑒.𝑚(𝜓 ) (𝑒) : 𝜎 [𝜂]
t-literal
Δ ⊢ 𝜏𝑆 ok Δ; Γ ⊢ 𝑒 : 𝜏 (𝑓 𝜎) = fields(𝜏𝑆 ) Δ ⊢ 𝜏 <: 𝜎
Δ; Γ ⊢ 𝜏𝑆{𝑒} : 𝜏𝑆
t-field
Δ; Γ ⊢ 𝑒 : 𝜏𝑆 (𝑓 𝜏) = fields(𝜏𝑆 )
Δ; Γ ⊢ 𝑒.𝑓𝑖 : 𝜏𝑖
t-assert𝐼
Δ ⊢ 𝜏𝐽 ok Δ; Γ ⊢ 𝑒 : 𝜎𝐽
Δ; Γ ⊢ 𝑒.(𝜏𝐽 ) : 𝜏𝐽
t-assert𝑆
Δ ⊢ 𝜏𝑆 ok Δ; Γ ⊢ 𝑒 : 𝜎𝐽 𝜏𝑆 <: boundsΔ (𝜎𝐽 )
Δ; Γ ⊢ 𝑒.(𝜏𝑆 ) : 𝜏𝑆
t-stupid
Δ ⊢ 𝜏 ok Δ; Γ ⊢ 𝑒 : 𝜎𝑆
Δ; Γ ⊢ 𝑒.(𝜏) : 𝜏
Programs 𝑃 ok
t-prog
distinct (tdecls(𝐷)) distinct (mdecls(𝐷)) 𝐷 ok ∅; ∅ ⊢ 𝑒 : 𝜏
package main; 𝐷 func main() {_ = 𝑒} ok
Fig. 17. FGG typing
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:19
Value 𝑣 ::= 𝜏𝑆{𝑣}
Evaluation context 𝐸 ::=
Hole □
Method call receiver 𝐸.𝑚(𝜏) (𝑒)
Method call arguments 𝑣 .𝑚(𝜏) (𝑣, 𝐸, 𝑒)
Structure 𝜏𝑆{𝑣, 𝐸, 𝑒}
Select 𝐸.𝑓
Type assertion 𝐸.(𝜏)
Reduction 𝑑 −→ 𝑒
r-field
(𝑓 𝜏) = fields(𝜏𝑆 )
𝜏𝑆{𝑣}.𝑓𝑖 −→ 𝑣𝑖
r-call
(𝑥 : 𝜏𝑆 , 𝑥 : 𝜏).𝑒 = body(type(𝑣).𝑚(𝜓 ))
𝑣 .𝑚(𝜓 ) (𝑣) −→ 𝑒 [𝑥 := 𝑣, 𝑥 := 𝑣]
r-assert
∅ ⊢ type(𝑣) <: 𝜏
𝑣 .(𝜏) −→ 𝑣
r-context
𝑑 −→ 𝑒
𝐸 [𝑑] −→ 𝐸 [𝑒]
Fig. 18. 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 𝑑 −→ 𝑒 holds
if expression 𝑑 steps to expression 𝑒 . Again, the adjustments are all simple.
4.5 FGG properties
The results of the previous section adapt straightforwardly.
Lemma 4.1 (Well formed). If Δ; Γ ⊢ 𝑒 : 𝜏 then Δ ⊢ 𝜏 ok.
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.
Lemma 4.2 (Substitution). Let 𝜂 = (𝛼 := 𝜏) be a substitution.
• If ∅ ⊢ 𝛼 <: 𝜏𝐼 [𝜂] and 𝛼 : 𝜏𝐼 , Δ ⊢ 𝜏 ok then Δ[𝜂] ⊢ 𝜏 [𝜂] ok.
• If ∅ ⊢ 𝛼 <: 𝜏𝐼 [𝜂] and 𝛼 : 𝜏𝐼 , Δ; Γ ⊢ 𝑒 : 𝜏 then Δ[𝜂]; Γ [𝜂] ⊢ 𝑒 [𝜂] : 𝜏 [𝜂].
• If ∅; ∅ ⊢ 𝑣 : 𝜏 and ∅; 𝑥 : 𝜎 ⊢ 𝑒 : 𝜎 and ∅ ⊢ 𝜏 <: 𝜎 then ∅; ∅ ⊢ 𝑒 [𝑥 := 𝑣] : 𝜏 for some type 𝜏 with
∅ ⊢ 𝜏 <: 𝜎 .
The remaining results are easy to adjust.
Theorem 4.3 (Preservation). If ∅; ∅ ⊢ 𝑑 : 𝜎 and 𝑑 −→ 𝑒 then ∅; ∅ ⊢ 𝑒 : 𝜏 for some 𝜏 with
∅ ⊢ 𝜏 <: 𝜎 .
Expression 𝑑 panics if there exist evaluation context 𝐸, value 𝑣 , and type 𝜏 such that 𝑑 = 𝐸 [𝑣 .(𝜏)]
and ∅ ⊢ type(𝑣) ≮: 𝜏 .
Theorem 4.4 (Progress). If ∅; ∅ ⊢ 𝑑 : 𝜎 then either 𝑑 is a value, 𝑑 −→ 𝑒 for some 𝑒 , or 𝑑 panics.
5 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.
Throughout this section, we illustrate the monomorphisation process with the FGG program
in Figure 19 (left). This program contains a Dispatcher structure which processes abstract Events.
A Dispatcher processes events, and events are objects that can be processed. For the sake of space,
the program in Figure 19 includes only one implementation of Events, i.e., UIEvents, but other
implementations may be easily added following the same pattern.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:20 Griesemer et al.
type Any interface {}
type Int struct {}
type Event interface {
Process(type b Any)(y b) Int
}
type UIEvent struct {}
func (x UIEvent) Process(type b Any)(y b) Int {
return Int{}
}
type Dispatcher struct {}
func (x Dispatcher) Dispatch(y Event) Int {
return y.Process(Int)(Int{})
}
func main() {
_ = Dispatcher{}.Dispatch(UIEvent{})
}
type Top struct {}
type Int struct {}
type Event interface {
Process<Int>(y Int) Int
Process<1>() Top
}
type UIEvent struct {}
func (x UIEvent) Process<Int>(y Int) Int {
return Int{} }
func (x UIEvent) Process<1>() Top {
return Top{} }
type Dispatcher struct {}
func (x Dispatcher) Dispatch(y Event) Int {
return y.Process<Int>(Int{}) }
func (x Dispatcher) Dispatch<1>() Top {
return Top{} }
func main() {
_ = Dispatcher{}.Dispatch(UIEvent{})
}
Fig. 19. Dispatcher example: FGG source (left) and FG translation (right)
5.1 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 arguments, 𝜏 .𝑚(𝜓 ). In Figure 20 we define a judgement 𝑃 ▶ Ω which computes the set
of instances of types and methods required to correctly monomorphise an FGG program.
Judgement Δ; Γ ⊢ 𝑒 ▶ 𝜔 holds if 𝜔 is the instance set for expression 𝑒 , 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 𝜏 .𝑚(𝜓 ) 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 𝑃 is the limit of function 𝐺 applied to the instance set of its body.
𝐺Δ (𝜔) is defined via four auxiliary functions that compute the type and method instances required
by 𝜔 . 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, inter-procedurally.
For each method instance 𝜏 .𝑚(𝜓 ) in 𝜔 it finds all instance sets of all implementations of method
𝑚, 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 𝜎 .
Consider the example in Figure 19 (left). For the top-level method, we have
∅; ∅ ⊢ Dispatcher{}.Dispatch(UIEvent{}) ▶ {Dispatcher, Dispatcher.Dispatch()}
Posing 𝜔0 = {Dispatcher, Dispatcher.Dispatch()}, we compute the limit of 𝐺 applied to 𝜔0. We have
𝐺∅ (𝜔0) = 𝜔0 ∪ {Event, Int, Dispatcher.Dispatch(), Event, Event.Process(Int)} where Event and Int
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:21
Instance sets 𝜔,Ω
𝜔,Ω range over sets containing elements of the form 𝜏 or 𝜏 .𝑚(𝜓 ).
Expressions and programs Δ; Γ ⊢ 𝑒 ▶ 𝜔 𝑃 ▶ Ω
I-var
Δ; Γ ⊢ 𝑥 ▶ ∅
I-literal
Δ; Γ ⊢ 𝑒 ▶ 𝜔
Δ; Γ ⊢ 𝜏𝑆{𝑒} ▶ {𝜏𝑆 } ∪ 𝜔
I-field
Δ; Γ ⊢ 𝑒 ▶ 𝜔
Δ; Γ ⊢ 𝑒.𝑓𝑖 ▶ 𝜔
I-assert
Δ; Γ ⊢ 𝑒 ▶ 𝜔
Δ; Γ ⊢ 𝑒.(𝜏) ▶ {𝜏} ∪ 𝜔
I-call
Δ; Γ ⊢ 𝑒 : 𝜏 Δ; Γ ⊢ 𝑒 ▶ 𝜔 Δ; Γ ⊢ 𝑒 ▶ 𝜔
Δ; Γ ⊢ 𝑒.𝑚(𝜓 ) (𝑒) ▶ {𝜏, 𝜏 .𝑚(𝜓 )} ∪ 𝜔 ∪ 𝜔
I-prog
∅; ∅ ⊢ 𝑒 ▶ 𝜔 Ω = lim
𝑛→∞𝐺
𝑛
∅ (𝜔)
package main; 𝐷 func main() {_ = 𝑒} ▶ Ω
Auxiliary functions
𝐺Δ (𝜔) = 𝜔 ∪ F-closure(𝜔) ∪M-closureΔ (𝜔) ∪ I-closureΔ (𝜔) ∪ S-closureΔ (𝜔)
F-closure(𝜔) =
⋃{
𝜏
 𝜏𝑆 ∈ 𝜔, (𝑓 𝜏) = fields(𝜏𝑆 )}
M-closureΔ (𝜔) =
⋃{
𝜎 [𝜂] ∪ {𝜎 [𝜂]}
 𝜏 .𝑚(𝜓 ) ∈ 𝜔, (𝑚(Ψ) (𝑥 𝜎) 𝜎) ∈ methodsΔ (𝜏), 𝜂 = (Ψ :=𝜓 )}
I-closureΔ (𝜔) =
{
𝜏 ′𝐼 .𝑚(𝜓 )
 𝜏𝐼 .𝑚(𝜓 ) ∈ 𝜔, 𝜏 ′𝐼 ∈ 𝜔, Δ ⊢ 𝜏 ′𝐼 <: 𝜏𝐼 }
S-closureΔ (𝜔) =
⋃{
{𝜏𝑆 .𝑚(𝜓 )} ∪ Ω
 𝜏 .𝑚(𝜓 ) ∈ 𝜔, 𝜏𝑆 ∈ 𝜔, Δ ⊢ 𝜏𝑆 <: 𝜏, Δ; 𝑥 : 𝜏𝑆 , 𝑥 : 𝜎 ⊢ 𝑒 ▶ Ω(𝑥 : 𝜏𝑆 , 𝑥 : 𝜎).𝑒 = body(𝜏𝑆 .𝑚(𝜓 )) }
Fig. 20. Computing instance sets
are obtained from M-closure∅ (𝜔0), while Dispatcher.Dispatch(), Event, and Event.Process(Int) are
obtained from S-closure∅ (𝜔0).
The limit of function 𝐺 is reached after two iterations, i.e., lim𝑛→∞𝐺𝑛∅ (𝜔0) = 𝐺∅ (𝐺∅ (𝜔0)) =
𝐺∅ (𝜔0) ∪ {UIEvent.Process(Int)}. Note that UIEvent.Process(Int) is obtained via S-closure using the
fact that UIEvent <: Event holds.
5.2 Monomorphisation judgement
We now define a judgement ⊢ 𝑃 ↦→ 𝑃† where 𝑃 is a program in FGG, and 𝑃† 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 21 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 arguments,
and g and h are types with no arguments, then closed type f(g(), h()) might correspond to the
identifier “f<g<>,h<>>” assuming “<,>” are allowed as letters in identifiers. We write 𝑡† = ⟨𝜏⟩ to
compute the identifier 𝑡† that corresponds to closed type 𝜏 . Similarly, we write𝑚† = ⟨𝑚(𝜓 )⟩ to
compute the identifier𝑚† that corresponds to closed method instantiation𝑚(𝜓 ).
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:22 Griesemer et al.
Types and methods 𝜂 ⊢ 𝜏 ↦→ 𝑡† 𝜂 ⊢ 𝑡 (Φ) ↦→ 𝑡† 𝜂 ⊢𝑚(𝜓 ) ↦→𝑚† 𝜂 ⊢𝑚(Ψ) ↦→𝑚†
m-type
𝑡† = ⟨𝜏 [𝜂]⟩
𝜂 ⊢ 𝜏 ↦→ 𝑡†
m-tformal
𝑡† = ⟨𝑡 (𝛼 [𝜂])⟩
𝜂 ⊢ 𝑡 (type 𝛼 𝜏𝐼 ) ↦→ 𝑡†
m-method
𝑚† = ⟨𝑚(𝜓 [𝜂])⟩
𝜂 ⊢𝑚(𝜓 ) ↦→𝑚†
m-mformal
𝑚† = ⟨𝑚(𝛼 [𝜂])⟩
𝜂 ⊢𝑚(type 𝛼 𝜏𝐼 ) ↦→𝑚†
Expression 𝜂 ⊢ 𝑒 ↦→ 𝑒†
m-var
𝜂 ⊢ 𝑥 ↦→ 𝑥
m-value
𝜂 ⊢ 𝜏𝑆 ↦→ 𝑡†𝑆 𝜂 ⊢ 𝑒 ↦→ 𝑒†
𝜂 ⊢ 𝜏𝑆 {𝑒} ↦→ 𝑡†𝑆 {𝑒†}
m-select
𝜂 ⊢ 𝑒 ↦→ 𝑒†
𝜂 ⊢ 𝑒.𝑓 ↦→ 𝑒† .𝑓
m-call
𝜂 ⊢ 𝑒 ↦→ 𝑒† 𝜂 ⊢𝑚(𝜓 ) ↦→𝑚† 𝜂 ⊢ 𝑒 ↦→ 𝑒†
𝜂 ⊢ 𝑒.𝑚(𝜓 ) (𝑒) ↦→ 𝑒† .𝑚† (𝑒†)
m-assert
𝜂 ⊢ 𝑒 ↦→ 𝑒† 𝜂 ⊢ 𝜏 ↦→ 𝑡†
𝜂 ⊢ 𝑒.(𝜏) ↦→ 𝑒† .(𝑡†)
Method signature 𝜂 ⊢ 𝑀 ↦→ 𝑀† 𝜂 ⊢ 𝑆 ↦→ 𝑆†
m-sig
𝜂 ⊢ 𝜏 ↦→ 𝑡† 𝜂 ⊢ 𝜏 ↦→ 𝑢†
𝜂 ⊢ (𝑥 𝜏) 𝜏 ↦→ (𝑥 𝑡†) 𝑢†
m-id
hash(𝑚𝑀 [𝜂]) =𝑚∗
𝜂 ⊢𝑚𝑀 ↦→𝑚∗ () Top
Type literal 𝜂; 𝜇 ⊢ 𝑇 ↦→ 𝑇 †
m-struct
𝜂 ⊢ 𝜏 ↦→ 𝑡†
𝜂; 𝜇 ⊢ struct{𝑓 𝜏} ↦→ struct{𝑓 𝑡†}
m-interface
𝜂; 𝜇 ⊢ 𝑆 ↦→ S
𝜂; 𝜇 ⊢ interface{𝑆} ↦→ interface{
⋃
S}
Fig. 21. Monomorphisation of FGG into FG — name mapping
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 m-sig.
Rule m-id is used to generate a dummy method signature that represents uniquely the alpha-
equivalence 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
in an FGG program, then this is also the case in its monomorphised counterpart. We assume that
hash(𝑚𝑀1) = hash(𝑚𝑀2) for all𝑀1 = 𝑀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 monomor-
phise each of its signatures and flatten the result in a single sequence of declarations.
Figure 22 formalises how declarations are generated from Ω. Here we let 𝑁 range over (𝑥 𝜏) 𝜏 .
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𝑚(𝜓 ). 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 𝑆† that uniquely identifies the FGG signature. Each parameterised
method may produce zero or more monomorphised instances, plus a dummy method signature.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:23
Interface specification 𝜂; 𝜇 ⊢ 𝑆 ↦→ S
m-spec
S =
{
𝑚†𝑁 †
𝑚(𝜓 ) ∈ 𝜇, 𝜃 = (𝜂,Ψ :=𝜓 ), 𝜃 ⊢𝑚(Ψ) ↦→𝑚†, 𝜃 ⊢ 𝑁 ↦→ 𝑁 † } 𝜂 ⊢𝑚(Ψ)𝑁 ↦→ 𝑆†
𝜂; 𝜇 ⊢𝑚(Ψ)𝑁 ↦→ S ∪ {𝑆†}
Declaration Ω ⊢ 𝐷 ↦→ D
m-type
D =
{
type 𝑡† 𝑇 †
 𝑡 (𝜙) ∈ Ω, 𝜂 = (Φ := 𝜙), 𝜇 = {𝑚(𝜓 ) | 𝑡 (𝜙).𝑚(𝜓 ) ∈ Ω}, 𝜂; 𝜇 ⊢ 𝑇 ↦→ 𝑇 † }
Ω ⊢ type 𝑡 (Φ) 𝑇 ↦→ D
m-func
D =
{
func (𝑥 𝑡†𝑆 ) 𝑚†𝑁 † {return 𝑒†}
 𝑡𝑆 (𝜙).𝑚(𝜓 ) ∈ Ω, 𝜃 = (Φ := 𝜙,Ψ :=𝜓 ), 𝜃 ⊢ 𝑡𝑆 (Φ) ↦→ 𝑡†𝑆𝜃 ⊢𝑚(Ψ) ↦→𝑚†, 𝜃 ⊢ 𝑁 ↦→ 𝑁 †, 𝜃 ⊢ 𝑒 ↦→ 𝑒† }
D ′ =
{
func (𝑥 𝑡†𝑆 ) 𝑆† {return Top{}}
 𝑡𝑆 (𝜙) ∈ Ω, 𝜂 = (Φ := 𝜙), 𝜂 ⊢ 𝑡𝑆 (Φ) ↦→ 𝑡†𝑆 , 𝜂 ⊢𝑚(Ψ)𝑁 ↦→ 𝑆†}
Ω ⊢ func (𝑥 𝑡𝑆 (Φ)) 𝑚(Ψ)𝑁 {return 𝑒} ↦→ D ∪ D ′
Program ⊢ 𝑃 ↦→ 𝑃†
m-program
package main; 𝐷 func main() {_ = 𝑒} ▶ Ω
Ω ⊢ 𝐷 ↦→ D 𝐷† = {type Top struct {}} ∪
⋃
D ∅ ⊢ 𝑒 ↦→ 𝑒†
⊢ package main; 𝐷 func main() {_ = 𝑒} ↦→ package main; 𝐷† func main() {_ = 𝑒†}
Fig. 22. Monomorphisation of FGG into FG — instance generation, where 𝑁 ranges over (𝑥 𝜏) 𝜏
To monomorphise the declaration of a type 𝑡 given an instance set, for each instance of 𝑡 , we
generate a substitution 𝜂 and a method instance set 𝜇. Then we recursively produce a monomor-
phised 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 𝑃 , 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.
The FGG program in Figure 19 (left) is translated to the FG program on the righthand side of
the figure. The translation starts with rule m-program where Ω = {Int, Event, Event.Process(Int),
UIEvent, UIEvent.Process(Int), Dispatcher, Dispatcher.Dispatch()}. Rule m-type is used to generate the
instances of types Int, Event, UIEvent, and Dispatcher. Rule m-func is used to generate the methods
UIEvent.Process(Int) and Dispatcher.Dispatch(), as well as their dummy counterparts Process<1>()
and Dispatch<1>(). Rule m-spec is used to generate the method signatures of interface Event, i.e.,
Event.Process(Int) and its dummy counterpart Process<1>().
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:24 Griesemer et al.
Not monomorphisable 𝑃 nomono 𝐷 nomono
mn-program
𝐷𝑖 nomono
package main; 𝐷 func main() {_ = 𝑒} nomono
mn-func
Δ = Φ,Ψ exists 𝑛 ∈ N and (𝑡𝑆 (𝜙).𝑚(𝜓 )) ∈ 𝐺𝑛Δ ({𝑡𝑆 (Φˆ), 𝑡𝑆 (Φˆ).𝑚(Ψˆ)}) s.t. Φ ≺ 𝜙 or Ψ ≺ 𝜓
func (𝑥 𝑡𝑆 (Φ)) 𝑚(Ψ) (𝑦 𝜏) 𝜏 {return 𝑒} nomono
Occurs check Φ ≺ 𝜙 𝛼 ≺ 𝜏
𝜙 = 𝜏 𝛼𝑖 ≺ 𝜏𝑖
(type 𝛼 𝜏𝐼 ) ≺ 𝜙
𝜏 ≠ 𝛼 𝛼 ∈ fv(𝜏)
𝛼 ≺ 𝜏
Fig. 23. Monomorphisability check
5.3 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 𝑃 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.
Note that there exist programs which produce finitely many type instances but for which the
predicate does hold, e.g., programs containing a polymorphic recursive method that is never called.
The predicate is formally defined in Figure 23, notably reusing our instance generation procedures.
𝑃 nomono holds if 𝐷 nomono holds for at least one of its method declarations. 𝐷 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 𝜏 .
5.4 Monomorphisation properties
Not all programs are monomorphisable, however we can decide whether a program is monomor-
phisable with the 𝑃 nomono predicate.
Theorem 5.1 (Decidability). If 𝑃 ok then it is decidable whether or not 𝑃 nomono holds.
For all well-typed programs 𝑃 such that 𝑃 nomono does not hold, their instance sets are finite.
Theorem 5.2 (Monomorphisable). If 𝑃 ok and 𝑃 nomono doesn’t hold then 𝑃 ▶ Ω with Ω finite.
Monomorphisation preserves typing, i.e., the translation of a well-typed FGG program is a
well-typed FG program.
Theorem 5.3 (Sound). If 𝑃 ok and ⊢ 𝑃 ↦→ 𝑃† then 𝑃† ok.
The reduction behaviour of well-typed FGG programs is preserved and reflected by their
monomorphised counterpart (see Figure 24). Write ⊢ 𝑑 ↦→ 𝑑† to abbreviate ∅; ∅ ⊢ 𝑑 ↦→ 𝑑†.
Theorem 5.4 (Bisimulation). Let 𝑃 ok and ⊢ 𝑃 ↦→ 𝑃† with 𝑃 = 𝐷 ▷ 𝑑 and 𝑃† = 𝐷† ▷ 𝑑†. Then:
(a) if 𝑑 −→ 𝑒 then there exists 𝑒† such that 𝑑† −→ 𝑒† and ⊢ 𝑒 ↦→ 𝑒†;
(b) if 𝑑† −→ 𝑒† then there exists 𝑒 such that 𝑑 −→ 𝑒 and ⊢ 𝑒 ↦→ 𝑒†.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:25
𝑑
𝑑†
𝑒1
𝑒†1
...
...
𝑒𝑛
𝑒†𝑛
⊢ 𝑑 ↦→ 𝑑† ⊢ 𝑒1 ↦→ 𝑒†1 ⊢ 𝑒𝑛 ↦→ 𝑒†𝑛
Assume 𝑃 ok
and ⊢ 𝑃 ↦→ 𝑃†
with 𝑃 = 𝐷 ▷ 𝑑
and 𝑃† = 𝐷† ▷ 𝑑†
Fig. 24. Bisimulation
6 IMPLEMENTATION
We have made available a prototype implementation,1 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 24: 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 SmallCheck [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.
7 RELATEDWORK
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. We note that in
Featherweight Go, Featherweight Generic Go (and in the Go language), since method signatures
are nonvariant, there are no fundamental decidability issues related to F-bounded polymorphism
and variance [Pierce 1992], and so there is no need to consider more sophisticated techniques such
as those of Greenman et al. [2014] to ensure decidability of type checking.
In terms of formalisations of generics, prior work on generics adopts one, or a combination, of
three main approaches, erasure, runtime representation of types as values, and monomorphisation.
1https://github.com/rhu1/fgg/
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:26 Griesemer et al.
Erasure. Bracha et al. [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.
Runtime 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 runtime 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 will 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 com-
piler [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 runtime 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 (polymor-
phic recursion, first-class polymorphism)”. In contrast, we present an algorithm that can determine
whether monomorphisation is possible in the presence of polymorphic recursion.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:27
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 (see Theorem 5.1 and [Griesemer et al. 2020]).
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.
8 CONCLUSION
In this work we studied generics for a minimal subset of Go and their compilation via monomor-
phisation. We chose monomorphisation since it is a simple first way of concretely explaining the
semantics of generics using (simplified) Go and it avoids restrictions required by the erasure-based
approach used in FGJ (e.g. type assertions on type variables). Another key benefit of monomorphi-
sation is that of enabling 0-cost abstractions – programs that do not use generics incur no runtime
penalty and generic code is translated into code that is equivalent to hand coded instantiations.
The cost is that of requiring a whole program analysis and disallowing programs that would result
in infinite instantiations (Section 5.3). Clearly, 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 we plan to consider an implementation based on passing runtime representations of
types, similar to that used for .NET generics [Kennedy and Syme 2001]. The idea is to automatically
equip methods and structs with data that codifies type arguments used in generic code at runtime.
For instance, a Cons struct would carry at runtime an additional field that specifies the type of the
element contained in the cell, and a method that constructs a tree from a List would thread the
runtime type information of the list cells into the tree. This approach requires translating all structs
and methods of a program to account for runtime type passing and construction and thus the
resulting programs can incur some runtime penalty. A mixed approach that uses monomorphisation
sometimes and passing runtime representations sometimes might be best, again similar to that
used for .NET generics. We will study the trade-offs and performance impact of this spectrum of
approaches in future work.
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.
ACKNOWLEDGMENTS
We thank Nicholas Ng, Sam Lindley, and our referees for comments and suggestions. This work was
funded under EPSRC EP/K034413/1, EP/T006544/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1,
EP/N028201/1, EP/T006544/1, EP/T014709/1 and EP/V000462/1, NCSS/EPSRC VeTSS, NOVA LINCS
(UIDB/04516/2020) with the financial support of FCT- Fundação para a Ciência e a Tecnologia, and
EU MSCA-RISE BehAPI (ID:778233).
REFERENCES
Nada Amin and Ross Tate. 2016. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In
Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA). 838–848.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
149:28 Griesemer et al.
Nick Benton, Andrew Kennedy, and George Russell. 1998. Compiling Standard ML to Java Bytecodes. In Proceedings of the
third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September
27-29, 1998, Matthias Felleisen, Paul Hudak, and Christian Queinnec (Eds.). ACM, 129–140. https://doi.org/10.1145/
289423.289435
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. 2016. Encoding Monomorphic and
Polymorphic Types. Logical Methods in Computer Science 12, 4 (2016).
François Bobot and Andrey Paskevich. 2011. Expressing Polymorphic Types in a Many-Sorted Language. In FroCoS (Lecture
Notes in Computer Science, Vol. 6989). Springer, 87–102.
Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. 1998. Making the Future Safe for the Past: Adding
Genericity to the Java Programming Language. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented
Programming Systems, Languages & Applications (OOPSLA ’98), Vancouver, British Columbia, Canada, October 18-22, 1998.
ACM, 183–200. https://doi.org/10.1145/286936.286957
Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C Mitchell. 1989. F-bounded polymorphism for
object-oriented programming. In Functional Programming Languages and Computer Architecture (FPCA). 273–280.
Henry Cejtin, Suresh Jagannathan, and Stephen Weeks. 2000. Flow-directed closure conversion for typed languages. In
European Symposium on Programming (ESOP). Springer, 56–71.
Koen Claessen, Jonas Duregård, and Michał Pałka. 2015. Generating constrained random data with uniform distribution.
Journal of Functional Programming 25 (2015). https://doi.org/10.1017/s0956796815000143
William R Cook. 1990. Object-oriented programming versus abstract data types. In Workshop of the REX Project (LNCS,
Vol. 489). Springer, 151–178.
Karl Crary, Stephanie Weirich, and J. Gregory Morrisett. 1998. Intensional Polymorphism in Type-Erasure Semantics.
In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore,
Maryland, USA, September 27-29, 1998. ACM, 301–312. https://doi.org/10.1145/289423.289459
Sophia Drossopoulou and Susan Eisenbach. 1997. Java is type safe—probably. In European Conference on Object-Oriented
Programming. Springer, 389–418.
Jonas Duregård. 2016. Automating Black-Box Property Based Testing. Ph.D. Dissertation. Chalmers University of Technology.
Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. 1998. Classes and Mixins. In Principles of Programming
Languages (POPL). 171–183.
Matthew Fluet. 2015. MLton – Monomorphise. http://mlton.org/Monomorphise.
Ben Greenman, Fabian Muehlboeck, and Ross Tate. 2014. Getting F-bounded polymorphism into shape. In ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11,
2014. 89–99. https://doi.org/10.1145/2594291.2594308
Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko
Yoshida. 2020. Featherweight Go. CoRR abs/2005.11710 (2020). arXiv:2005.11710 https://arxiv.org/abs/2005.11710
Robert Griesemer, Rob Pike, Ken Thompson, Ian Taylor, Russ Cox, Jini Kim, and Adam Langley. 2009. Hey! Ho! Let’s Go!
https://opensource.googleblog.com/2009/11/hey-ho-lets-go.html
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 1999. Featherweight Java: A Minimal Core Calculus for Java and GJ.
In Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications
(OOPSLA ’99), Denver, Colorado, USA, November 1-5, 1999., Brent Hailpern, Linda M. Northrop, and A. Michael Berman
(Eds.). ACM, 132–146. https://doi.org/10.1145/320384.320395
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ.
ACM Trans. Program. Lang. Syst. 23, 3 (2001), 396–450. https://doi.org/10.1145/503502.503505
Mark P Jones. 1995. Dictionary-free overloading by partial evaluation. Lisp and Symbolic Computation 8, 3 (1995), 229–248.
Andrew Kennedy and Don Syme. 2001. Design and Implementation of Generics for the .NET Common Language Runtime. In
Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird,
Utah, USA, June 20-22, 2001. ACM, 1–12. https://doi.org/10.1145/378795.378797
Shriram Krishnamurthi, Matthias Felleisen, and Daniel P Friedman. 1998. Synthesizing object-oriented and functional
design to promote re-use. In European Conference on Object-Oriented Programming (ECOOP). Springer, 91–113.
Xavier Leroy. 1992. Unboxed Objects and Polymorphic Typing. In Conference Record of the Nineteenth Annual ACM SIGPLAN-
SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992. ACM
Press, 177–188. https://doi.org/10.1145/143165.143205
Maurice Naftalin and PhilipWadler. 2006. Java generics and collections. O’Reilly. http://www.oreilly.de/catalog/javagenerics/
index.html
Tobias Nipkow and David von Oheimb. 1998. Javalight is Type-safe—Definitely. In Principles of Programming Languages
(POPL). 161–170.
Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Conference Record of the Nineteenth Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22,
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.
Featherweight Go 149:29
1992. 305–315. https://doi.org/10.1145/143165.143228
John C Reynolds. 1994. User-defined types and procedural data structures as complementary approaches to data abstraction.
In New Directions in Algorithmic Languages. MIT Press, 13–23.
Colin Runciman, Matthew Naylor, and Fredrik Lindblad. 2008. Smallcheck and lazy smallcheck. In Proceedings of the first
ACM SIGPLAN symposium on Haskell - Haskell '08. ACM Press. https://doi.org/10.1145/1411286.1411292
Jeremy G. Siek and Walid Taha. 2006. A Semantic Analysis of C++ Templates. In European Conference on Object-Oriented
Programming (ECOOP) (LNCS, Vol. 4067). Springer, 304–327.
Bjarne Stroustrup. 2013. The C++ Programming Language, 4th Edition. Addison-Wesley.
Wouter Swierstra. 2008. Data types à la carte. Journal of Functional Programming 18, 4 (2008), 423–436.
Don Syme. 1999. Proving Java Type Soundness. In Formal Syntax and Semantics of Java. Springer-Verlag, 83–118.
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. 2018. Safe Low-level Code Generation in Coq UsingMonomorphization
and Monadification. JIP 26 (2018), 54–72.
Ian Lance Taylor and Robert Griesemer. 2019. Contracts — Draft Design. https://go.googlesource.com/proposal/+/master/
design/go2draft-contracts.md
Ian Lance Taylor and Robert Griesemer. 2020. Type Parameters — Draft Design. https://go.googlesource.com/proposal/+/
refs/heads/master/design/go2draft-type-parameters.md
The Go Team. 2020. The Go Programming Language Specification. https://golang.org/ref/spec
The Rust Team. 2017. The Rust programming language. http://rust-lang.org/
Andrew P. Tolmach and Dino Oliva. 1998. FromML to Ada: Strongly-Typed Language Interoperability via Source Translation.
Journal of Functional Programming 8, 4 (1998), 367–412.
Mads Torgersen. 2004. The expression problem revisited. In European Conference on Object-Oriented Programming (ECOOP).
Springer, 123–146.
Aaron Turon. 2015. Abstraction without overhead: traits in Rust. https://blog.rust-lang.org/2015/05/11/traits.html
Mirko Viroli and Antonio Natali. 2000. Parametric polymorphism in Java: an approach to translation based on reflective
features. In Proceedings of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages &
Applications (OOPSLA 2000), Minneapolis, Minnesota, USA, October 15-19, 2000. ACM, 146–165. https://doi.org/10.1145/
353171.353182
Philip Wadler. 1998. The expression problem. Posted on the Java Genericity mailing list. http://homepages.inf.ed.ac.uk/
wadler/papers/expression/expression.txt
Dachuan Yu, Andrew Kennedy, and Don Syme. 2004. Formalization of generics for the .NET common language runtime. In
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice,
Italy, January 14-16, 2004. ACM, 39–51. https://doi.org/10.1145/964001.964005
Matthias Zenger and Martin Odersky. 2004. Independently extensible solutions to the expression problem. Technical Report.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 149. Publication date: November 2020.