[TYPES] A question about the literature on monomorphisation

[Philip Wadler]

Dear Types,

We have a question about the literature on monomorphisation.  We will
give an example in terms generics for Java, but similar features occur
in many other languages (C++ templates, C#, Rust, and so on) and we
are interested in all of these.

Java generics are implemented by erasure, but let's consider what is
required for implementation by monomorphisation.  In Java, each of
classes, interfaces, and methods may take generic parameters.
Monomorphisation replaces each generic class, interface, or method by
one instance for each actual generic parameter that occurs in the
program.  An interface that is generic may itself contain generic
methods.  In that case, monomorphisation needs to generate one
instance of the interface for each type at which it is instantiated,
and then one instance of the method within the interface for each type
at which *it* is instantiated.

For example, consider the following Java interface:

    interface List<A> {
        public String toString()
        public List<B> map<B>(f Function(A,B))
    }

and this code:

    List<Integer> ints
    List<Boolean> bools
    Function<Integer,Integer> square
    Function<Integer,Boolean> positive
    String string1 = ints.toString()
    List<Integer> ints2 = ints.map(square)
    List<Boolean> bools2 = int.map(positive)
    String string2 = bools.ToString()

If there are no other invocations of toString() or map(), the List
interface would have two instances, the first requiring two instances
of the map method and the second requiring none:

    interface ListInteger {
        public String toString()
        public ListInteger mapInteger(f FunctionIntegerInteger)
        public ListBoolean mapBoolean(f FunctionIntegerBoolean)
    }
    interface ListBoolean {
        public String toString()
    }

The bookkeeping required to formalise monomorphisation of instances
and methods is not too difficult, but not trivial---it took us several
tries to formalise it for a different language.

The question is, where has this been described in the literature?
Below is a list of the references we have found on monomorphisation,
but none of them seems to cover the specific problem of
monomorphisation of generic methods within generic interfaces, as
described above, even though that combination occurs in several
languages.  Have we missed any relevant literature?

Thank you for your help.

Raymond Hu
Wen Kokke
Julien Lange
Bernardo Toninho
Philip Wadler
Nobuko Yoshida


References:

From ML to Ada: Strongly-Typed Language Interoperability via Source
Translation.  Andrew P. Tolmach and Dino Oliva, JFP 1998.

Design and Implementation of Generics for the .NET Common Language
Runtime. Andrew Kennedy and Don Syme, PLDI 2001.

Formalization of generics for the .NET common language
runtime. Dachuan Yu, Andrew Kennedy, and Don Syme, POPL 2004.

A Semantic Analysis of C++ Templates. Jeremy Siek and Walid Taha,
ECOOP 2006.

Whole-program compilation in MLton. Stephen Weeks. ML 2006.
(Slides of invited talk.)

Encoding Monomorphic and Polymorphic Types. Jasmin Christian
Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone,
Logical Methods in Computer Science 2016.

Safe Low-level Code Generation in Coq Using Monomorphization and
Monadification. Akira Tanaka, Reynald Affeldt, and Jacques
Garrigue. JIP 2018.

Monomorphisation for Rust (commented code)
https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/monomorphize/collector/index.html

Monomorphisation for Mlton (commented code)
https://rustc-dev-guide.rust-lang.org/backend/monomorph.html

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20200326/12f55f90/attachment.ksh>