Pith. sign in

REVIEW 2 major objections 2 minor 22 references

Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)

T0 review · 2 major / 2 minor · reviewed 2026-06-26 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A type-directed compilation from Welterweight Go to LWG implements generics and structural subtyping using runtime conversions and adaptor methods while preserving separate compilation.

desk verdict WG and LWG give a core model for Go generics plus structural subtyping, compiled via runtime conversions and adaptors to keep separate compilation and avoid code generation. read the letter →

arxiv 2606.27138 v1 pith:HCO7H6QS submitted 2026-06-25 cs.PL

Raymond Hu , Julien Lange , Bernardo Toninho , Philip Wadler , Robert Griesemer , Keith Randall This is my paper · ORCID
classification cs.PL
keywords structuralsubtypinggenericsGoprogramminglanguagetype-directedcompilationruntimetypeconversionsadaptormethodsseparateboxing
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces WG as a core model of Go that includes underlying types, type unions, type sets, and generic methods. It also defines LWG to capture Go's runtime distinction between raw struct values and interface values carrying runtime type information. The central contribution is a type-directed compilation from WG to LWG that handles the interactions between structural subtyping and generics through runtime type conversions and adaptor methods. This approach meets Go's design goals of compatibility with separate compilation and no runtime code generation, differing from static monomorphisation strategies.

What carries the argument

The type-directed compilation from WG to LWG that employs runtime type conversions and adaptor methods to manage structural subtyping and generics.

What would settle it

A concrete program using generic methods on types with underlying types where the LWG execution does not match the WG semantics or requires generating new code at runtime.

Watch

Extended reading notes

Core claim

WG models key Go features including underlying types, type unions and type sets, and generic methods. LWG models the runtime mechanisms distinguishing raw structs from interfaces with RTTI. The type-directed compilation from WG to LWG uses runtime type conversions and adaptor methods to implement the features while ensuring separate compilation and no runtime code generation.

Load-bearing premise

WG correctly models the main Go features not covered before, and the compilation to LWG accurately captures the runtime difference between plain struct values and typed interface values while keeping the same meaning.

Editorial extensions

If this is right

  • The compilation strategy demonstrates that proposed Go features can be implemented without runtime code generation.
  • It shows compatibility with separate compilation for programs using generics and structural subtyping.
  • The use of runtime conversions and adaptors avoids the limitations of static monomorphisation in handling Go's runtime infrastructure.
  • Semantics are preserved between the high-level model and the runtime model.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the compilation preserves semantics, it could guide implementations of similar features in other languages with structural subtyping and generics.
  • Testable by checking if the compiled LWG code matches the behavior of actual Go programs with generic methods and type sets.
  • The approach might extend to other runtime distinctions in languages like interfaces versus concrete types.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 2 minor

Summary. The paper introduces WG, a core calculus modeling Go that incorporates structural subtyping, generics, underlying types, type unions/type sets, and generic methods (features excluded from prior formalizations). It defines LWG as a lower-level language capturing Go runtime distinctions between raw struct values and interface values carrying RTTI. A type-directed compilation from WG to LWG is presented that employs runtime type conversions and adaptor methods to realize the features while maintaining separate compilation and avoiding runtime code generation, in contrast to static monomorphisation approaches.

Significance. If the compilation strategy is shown to preserve the necessary properties, the work would supply a formal account of Go-specific challenges at the intersection of structural subtyping and generics, together with a practical compilation technique aligned with Go's implementation constraints. The explicit modeling of runtime boxing and RTTI distinctions, plus the emphasis on separate compilation, distinguishes the contribution from monomorphisation-based formalisms.

major comments (2)
  1. [Abstract / compilation sections] Abstract and compilation development: the central claim is that the type-directed compilation from WG to LWG correctly implements the features while preserving semantics and design goals, yet the manuscript supplies no theorems, lemmas, or proof sketches establishing type preservation, semantic equivalence, or that the runtime conversions and adaptor methods handle all interactions between structural subtyping, generics, and Go's runtime infrastructure.
  2. [WG and LWG definitions] The assumption that WG faithfully captures the excluded Go features (underlying types, type unions/sets, generic methods) and that the LWG model accurately reflects the runtime distinction between raw structs and RTTI-carrying interfaces is load-bearing for the compilation claim, but no validation (e.g., via examples, metatheory, or comparison to Go implementation) is provided to confirm this modeling choice.
minor comments (2)
  1. [WG syntax] Notation for type sets and unions could be clarified with a small example table showing how they interact with structural subtyping.
  2. [LWG runtime model] The distinction between 'raw struct values' and 'interface values' in LWG would benefit from an explicit side-by-side comparison figure.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. The two major points correctly identify areas where the manuscript is currently thin on formal justification and validation. We address each below and indicate how we will revise.

read point-by-point responses

  1. Referee: [Abstract / compilation sections] Abstract and compilation development: the central claim is that the type-directed compilation from WG to LWG correctly implements the features while preserving semantics and design goals, yet the manuscript supplies no theorems, lemmas, or proof sketches establishing type preservation, semantic equivalence, or that the runtime conversions and adaptor methods handle all interactions between structural subtyping, generics, and Go's runtime infrastructure.

    Authors: We agree that the manuscript presents the compilation rules and argues for their correctness via examples and informal reasoning but does not supply theorems, lemmas, or proof sketches for type preservation or semantic equivalence. This is a genuine gap. In the revised version we will add a dedicated metatheory section containing (i) a statement of type preservation for the compilation, (ii) a sketch of the key lemmas relating WG and LWG reductions, and (iii) a brief argument that the adaptor-method technique preserves the required structural-subtyping and generic-method interactions. We will also make explicit which properties are proved and which remain conjectural. revision: yes

  2. Referee: [WG and LWG definitions] The assumption that WG faithfully captures the excluded Go features (underlying types, type unions/sets, generic methods) and that the LWG model accurately reflects the runtime distinction between raw structs and RTTI-carrying interfaces is load-bearing for the compilation claim, but no validation (e.g., via examples, metatheory, or comparison to Go implementation) is provided to confirm this modeling choice.

    Authors: The modeling decisions are grounded in the Go language specification and the published implementation of the runtime and compiler, but the manuscript indeed provides only illustrative examples rather than systematic validation or direct comparison with the Go toolchain. We will expand the revised paper with (a) a table mapping each WG construct to the corresponding Go feature or proposal, (b) additional worked examples that exercise underlying types, type sets, and generic methods, and (c) a short discussion of how the LWG boxing rules align with the concrete representation choices described in the Go runtime source. Full mechanized correspondence with the production compiler is beyond the scope of this work, but the added material will make the modeling assumptions more transparent and checkable. revision: yes

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; definitional model and compilation strategy

full rationale

The paper defines WG as a core calculus capturing Go features (underlying types, type unions/sets, generic methods) and LWG as a lower-level model of runtime boxing/RTTI. It then defines a type-directed compilation from WG to LWG. This is a constructive, by-definition translation whose correctness is established relative to the authors' own semantics; it does not reduce any claimed result to a fitted parameter, a self-citation chain, or an input by construction. No predictions, uniqueness theorems, or ansatzes are invoked in a load-bearing way. The approach is offered as an alternative to monomorphisation while preserving separate compilation, which is an independent design goal external to the formalisation itself. This is the normal, non-circular outcome for a language-design and compilation paper.

Assumptions & free parameters 0 free parameters · 0 assumptions · 0 invented entities

Abstract provides no explicit free parameters, axioms, or invented entities; full text would be required to audit them.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)." pith.science (2026). https://pith.science/paper/HCO7H6QS

@misc{pith2026260627138,
  author       = {Pith},
  title        = {Pith review of: Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HCO7H6QS}},
  note         = {Machine review of arXiv:2606.27138}
}
read the original 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 unions 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.

Figures

Figures reproduced from arXiv: 2606.27138 by the authors.

Figure 1
Figure 1. (top) Code supported by Go and WG; (bottom) code supported by WG only. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Extending the example from Fig. 1 [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. WG syntax Assignability in Go relies on the notion of underlying type which in turn is a cornerstone of the language formalism. In the type union Ordered, the clause that includes string types is written ∼string. Go allows a new type with the same underlying memory representation as another to be defined as a nominally distinct type and to which, for instance, additional methods can be attached. By using the ∼ type … view at source ↗
Figures from the paper (24 more)
Figure 4
Figure 4. Figure 4: WG: auxiliary definitions Expressions include variables, method calls, structure literals, field selection, type assertions, type conversions, typed constants, and operations. We model only explicitly typed constants 𝑇 (𝑐) such as int(42) or float64(42.0), abstracting …
Figure 5
Figure 5. Figure 5: Implements and Assignability relations. U is defined s.t. 𝑇 ∈ U for all 𝑇 . The typesΔ (𝑇 ) function returns the type set of a type, and particularly the set of types explicitly listed in an interface, possibly flagged with ∼𝑇 notation. The type set of a non-interface …
Figure 6
Figure 6. Figure 6: Well-formed types and declarations essentially erases (recursively) our type annotations in method signatures and within types, e.g., 𝑇@𝑉 ⇂1 =𝑇 ⇂1. Aspect (2) involves checking that each element in the type set of 𝑇 is directly in the type set of 𝑈 or is otherwise cove…
Figure 7
Figure 7. Figure 7: WG typing instance, Rule t-call handles generic type parameter instantiation through substitution 𝜂, it also ensures that the instantiated type parameters satisfy their bounds. Observe how implementability (<:Δ) is used to check that type instances implements their bou…
Figure 8
Figure 8. Figure 8: WG reduction Converter{}.toPoint(Point{1,1}) and Converter{}.toPoint(Coord{1,1}) are all well-typed in WG (and Go). Similarly, Converter{}.toAnonymous(Point{1,1}) is well-typed. However, the invocation Converter{}.toAnonymous(Coord{1,1}) is ill-typed since Coord ≺: Poi…
Figure 9
Figure 9. Figure 9: LWG syntax We say expression 𝑒 panics if there exists an evaluation context 𝐸, value 𝑣 and type 𝑇 such that 𝑒 = 𝐸[𝑣.(𝑇 )] and type(𝑣) </: 𝑇 . Theorem 3.6 (Progress). If ∅; ∅ ⊢ 𝑒 : 𝑇 then either 𝑒 is a value, 𝑒 −→ 𝑒 ′ for some 𝑒 ′ , or 𝑒 panics. 4 Low-Level Welterweight…
Figure 10
Figure 10. Figure 10: LWG reduction The “Static-Change” operation performs a “conversion” between assignable non-interface types. This operation does not perform any actions related to boxing such as RTTI or method tables (in Go it supports reflection which we are not modelling here). The …
Figure 11
Figure 11. Figure 11: LWG: Typing for declarations and expressions [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]
Figure 12
Figure 12. Figure 12: LWG: additional typing rules The last three rules deal with static and dynamic form of operators. Rule t-op-static handles operators on concrete types that are resolved statically. In this case, the operator must be available on the underlying type of 𝑇 . Rule t-op-dy…
Figure 13
Figure 13. Figure 13: Auxiliary notations and compilation rules for types [PITH_FULL_IMAGE:figures/full_fig_p020_13.png]
Figure 14
Figure 14. Figure 14: In Δ; Γ ⊢ 𝑒 : 𝑈 ↦→Φ 𝑒 ′ , 𝑒 is a well-typed WG expression, 𝑒 ′ is an LWG expression that 𝑒 compiles into, and Φ is the target LWG type of 𝑒 ′ . This judgement determines which synthetic casts (make, change or static-change) are needed in the resulting expression. Inte…
Figure 14
Figure 14. Figure 14: Compilation rules: generate synthetic casts [PITH_FULL_IMAGE:figures/full_fig_p021_14.png]
Figure 15
Figure 15. Figure 15: Compilation rules: expressions (part 1) Rules op-static and op-dyn deal with operators. Recall that the WG type system enforces that the operands have all the same type, which is either a type whose underlying type is a base type, or a type variable whose bound suppor…
Figure 16
Figure 16. Figure 16: Compilation rules: expressions (part 2) unbox the return value, in order for it to match the signature of useProcessor which has a non￾generic return. The attentive reader might have already identified the problem with this naive approach: while IntProcessor implement…
Figure 17
Figure 17. Figure 17: Compilation rules: method declarations There is a lowering simulation between a WG program 𝐷 ▷ 𝑒 and an LWG program 𝐷′ ▷ 𝑒 ′ , if whenever 𝑒 −→ 𝑑 then 𝑒 ′ −→∗ 𝑑 ′ , and 𝑒 ′ and 𝑑 ′ are in a lowering simulation. Also, if 𝑒 is a value, then 𝑑 is an equivalent value; and…
Figure 18
Figure 18. Figure 18: WG: additional auxiliary definitions (3) If Δ ⊢ 𝛽 𝑇 ✓ then Δ, 𝛼 : 𝑆 ⊢ 𝛽 𝑇 ✓ (4) If Δ ⊢ 𝑚[𝛽 𝑇 ] (𝑥 𝑈 ) 𝑈 ✓ then Δ, 𝛼 : 𝑆 ⊢ 𝑚[𝛽 𝑇 ] (𝑥 𝑈 ) 𝑈 ✓ (5) If Δ; Γ ⊢ 𝑒 : 𝑇 then Δ, 𝛼 : 𝑆; Γ ⊢ 𝑒 : 𝑇 and Δ; Γ, 𝑥 : 𝑆 ⊢ 𝑒 : 𝑇 (6) If Δ ⊢ 𝑇 ✓ and Δ ⊢ 𝑈 ✓ and 𝑇 <:Δ 𝑈 implies 𝑇 <:Δ,𝛼:𝑆 𝑇…
Figure 19
Figure 19. Figure 19: WG: well-formedness ifaceΔ (𝑇 ) ¬tyvarΔ (𝑇 ) by inversion typesΔ (𝑇 ) ⊆ typesΔ (𝑈 ) methodsΔ(𝑇 ) ⊇ methodsΔ(𝑈 ) ifaceΔ (𝑈 ) ¬tyvarΔ (𝑈 ) by inversion typesΔ (𝑆) ⊆ typesΔ (𝑈 ) by transitivity of ⊆ methodsΔ(𝑆) ⊇ methodsΔ(𝑈 ) by transitivity of ⊇ 𝑆 <:Δ 𝑈 by <:𝐼 □ Lemma 9…
Figure 20
Figure 20. Figure 20: WG: additional typing rules for expressions [PITH_FULL_IMAGE:figures/full_fig_p031_20.png]
Figure 21
Figure 21. Figure 21: Correspondence between WG and LWG values. [PITH_FULL_IMAGE:figures/full_fig_p044_21.png]
Figure 22
Figure 22. Figure 22: Equivalence between LWG well-typed expressions modulo synthetic casts. We write 𝑑 ≏ 𝑑 ′ for ∅; ∅ ⊢ 𝑑 ≏ 𝑑 ′ and we write 𝑒.(𝑉 @𝑇 ) ◦ to indicate a type-assert added by the compiler. Proof. Mechanical by investigating the type derivation of Δ; 𝑥 : 𝑈 ⊢ 𝑒 :𝑇 with Theorem …
Figure 23
Figure 23. Figure 23: Key diagram for the proof of Lemma 9.40. [PITH_FULL_IMAGE:figures/full_fig_p048_23.png]
Figure 24
Figure 24. Figure 24: 𝑑 = 𝑑 ′ = ⌊𝑇 ⌋{𝑛}.𝑖.( ⌊𝑆𝑖⌋@⌊𝑆𝑖⌋) −→∗ ⌊𝑇 ⌋{𝑣 ′}.𝑖.( ⌊𝑆𝑖⌋@⌊𝑆𝑖⌋) −→ 𝑣 ′ 𝑖 .( ⌊𝑆𝑖⌋@⌊𝑆𝑖⌋) −→ ⌊𝑆𝑖⌋@⌊𝑆𝑖⌋( ⌊𝑈𝑖⌋, 𝜌′ , 𝑣′′ 𝑖 ) = 𝑑 ′′′ ≏ 𝑛𝑖 .( ⌊𝑈𝑖⌋ →𝜌 ⌊𝑆𝑖@𝑆𝑖⌋) = 𝑑 ′′ since the first step (−→∗ ) follows from Lemma 9.39 (via rule context), the second step (−→) follows from rule…
Figure 24
Figure 24. Figure 24: Key diagram for the proof of Lemma 9.42. [PITH_FULL_IMAGE:figures/full_fig_p052_24.png]
Figure 9
Figure 9. Figure 9: gives an overview of our proof strategy. We start from [PITH_FULL_IMAGE:figures/full_fig_p053_9.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 16 canonical work pages

  1. [1]

    InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D

    Type soundness proofs with definitional interpreters. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 666–679. doi:10.1145/3009837.3009866 Nada Amin and Ross Tate

    work page doi:10.1145/3009837.3009866 2017

  2. [2]

    InProceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA ’98), Vancouver, British Columbia, Canada, October 18-22,

    Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. InProceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA ’98), Vancouver, British Columbia, Canada, October 18-22,

    1998

  3. [3]

    doi:10.1145/286936.286957 Karl Crary, Stephanie Weirich, and J

    ACM, 183–200. doi:10.1145/286936.286957 Karl Crary, Stephanie Weirich, and J. Gregory Morrisett

    work page doi:10.1145/286936.286957

  4. [4]

    InProceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998.ACM, 301–312

    Intensional Polymorphism in Type-Erasure Semantics. InProceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998.ACM, 301–312. doi:10.1145/289423.289459 dominikh

    work page doi:10.1145/289423.289459 1998

  5. [5]

    ACM Program

    Generic Go to Go: dictionary-passing, monomorphisation, and hybrid.Proc. ACM Program. Lang.6, OOPSLA2 (2022), 1207–1235. doi:10.1145/3563331 Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida

    work page doi:10.1145/3563331 2022

  6. [6]

    ACM Program

    Featherweight go.Proc. ACM Program. Lang.4, OOPSLA (2020), 149:1–149:29. doi:10.1145/3428217 Robert Griesemer and Ian Lance Taylor

    work page doi:10.1145/3428217 2020

  7. [7]

    InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20,

    Java generics are turing complete. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20,

    2017

  8. [8]

    doi:10.1145/3009837 Robert Harper and J

    ACM, 73–85. doi:10.1145/3009837 Robert Harper and J. Gregory Morrisett

    work page doi:10.1145/3009837

Show all 22 references
  1. [9]

    doi:10.1145/199448.199475 Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, and Keith Randall

    ACM Press, 130–141. doi:10.1145/199448.199475 Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, and Keith Randall

    doi

  2. [10]

    Welterweight Go: Boxing, Structural Subtyping and Generics (Artifact). Zenodo. doi:10.5281/zenodo.17741038 Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler

    doi

  3. [11]

    ACM Trans

    Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst.23, 3 (2001), 396–450. doi:10.1145/503502.503505 Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer

    2001 doi

  4. [12]

    ACM Program

    RustBelt: securing the foundations of the rust programming language.Proc. ACM Program. Lang.2, POPL (2018), 66:1–66:34. doi:10.1145/3158154 Andrew Kennedy and Don Syme

    2018 doi

  5. [13]

    In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22,

    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

  6. [14]

    doi:10.1145/378795.378797 Xavier Leroy

    ACM, 1–12. doi:10.1145/378795.378797 Xavier Leroy

    doi

  7. [15]

    doi:10.1145/143165.143205 Mario Macías

    ACM Press, 177–188. doi:10.1145/143165.143205 Mario Macías

    doi

  8. [16]

    InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Stephen M

    KJS: a complete formal semantics of JavaScript. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Stephen M. Blackburn (Eds.). ACM, 346–356. doi:10.1145/2737924.2737991 Keith Randall

    2015 doi

  9. [17]

    A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go.J. Funct. Program.33 (2023). doi:10.1017/S0956796823000047 Ian Lance Taylor and Robert Griesemer

    2023 doi

  10. [18]

    https://blog.rust-lang.org/2015/05/11/traits.html Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, and Keith Randall Mirko Viroli and Antonio Natali

    Abstraction without overhead: traits in Rust. https://blog.rust-lang.org/2015/05/11/traits.html Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, and Keith Randall Mirko Viroli and Antonio Natali

    2015

  11. [19]

    Parametric polymorphism in Java: an approach to translation based on reflective features. InProceedings of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 2000), Minneapolis, Minnesota, USA, October 15-19, 2000.ACM, 146–...

    2000 doi

  12. [20]

    In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16,

    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

  13. [21]

    doi:10.1145/964001.964005 7 Examples 7.1 Desugared version of Fig

    ACM, 39–51. doi:10.1145/964001.964005 7 Examples 7.1 Desugared version of Fig. 1 packagemain typeMyNuminterface{ MyInt | MyFloat } typeMyIntint func(x MyInt) String()string{returnstrconv.Itoa(int(x)) } typeMyFloatfloat64 func(x MyFloat) String()string{returnstrconv.FormatFloat...

    doi

  14. [22]

    methods(𝑆)=methods(𝑇 ′)andtypes(𝑆)=types(𝑇 ′)therefore 𝑇< : 𝑆and so𝑇≺:𝑆

    WG: additional typing rules for expressions Follows by transitivity of<: No other possible derivation of≺: Case:𝑇< : 𝑇and¬iface(𝑇) Immediate since𝑇=𝑇 ′ Case:𝑇< : 𝑇 ′ fromiface(𝑇 ′),types(𝑇) ⊆types(𝑇 ′),methods(𝑇) ⊇methods(𝑇 ′),¬tyvar(𝑇 ′) Subcase:𝑇 ′ ≺:𝑆from𝑇< : 𝑆 Follows by t...

    2020

Pith tools

Reviewed June 26, 2026 · model on record in the stance chip above.