Welterweight Go: Boxing, Structural Subtyping, and Generics
Open Access
- 8 January 2026
- journal article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 10 (POPL) , 2295-2322
Abstract
Go’s unique combination of structural subtyping between generics and types with non-uniform runtime representations presents significant challenges for formalising the language. We introduce WG (Welterweight Go), a core model of Go that captures key features excluded by prior work, including underlying types, type constraints and type sets, and proposed new features, such as generic methods. We also develop LWG, a lower-level language that models Go’s runtime mechanisms, notably the distinction between raw struct values and interface values that carry runtime type information (RTTI). We give a type-directed compilation from WG to LWG that demonstrates how the proposed features can be implemented while observing important design and implementation goals for Go: compatibility with separate compilation, and no runtime code generation. Unlike existing approaches based on static monomorphisation, our compilation strategy uses runtime type conversions and adaptor methods to handle the complex interactions between structural subtyping, generics, and Go’s runtime infrastructure.Keywords
All Related Versions
Funding Information
- Fundação para a Ciência e a Tecnologia, I.P. (UID/50021/2025)
- Fundação para a Ciência e a Tecnologia, I.P. (UID/PRR/50021/2025)
This publication has 16 references indexed in Scilit:
- A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic GoJournal of Functional Programming, 2023
- RustBelt: securing the foundations of the Rust programming languageProceedings of the ACM on Programming Languages, 2017
- Type soundness proofs with definitional interpreters2017
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages2017
- Java and scala's type systems are unsound: the existential crisis of null pointers2016
- KJS: a complete formal semantics of JavaScript2015
- Making the future safe for the past1998
- Intensional polymorphism in type-erasure semantics1998
- Compiling polymorphism using intensional type analysis1995
- Unboxed objects and polymorphic typing1992