Description of ismonom algorithms?

[mdempsky]

Hello, I'm trying to understand the algorithms used in https://github.com/rhu1/fgg/blob/main/internal/fgg/fgg_ismonom.go.

My first instinct for detecting non-monomorphisable code was to implement a "data" flow analysis algorithm for tracking which type parameters are used as type arguments for instantiating other generics, and then looking for cycles. It seems like this might be similar to the "old CFG-based test" included at the bottom of the above file. Is there a reason why that test was deprecated in favor of the transitive closure algorithm?

Concretely, the algorithm I had in mind was:

1. Create a weighted directed graph with vertices representing type parameters and edges representing uses in instantiation.
2. For each instantiation within a generic type/method declaration, add an edge from the instantiated type parameter to the used type parameter. An edge with zero weight is used if the type parameter is directly used (e.g., F[T]) and with positive weight if the type parameter is used within a composite type (e.g., F[*T] or F[[]T]).
3. Check the resulting graph for positive-weight cycles.

I think this algorithm can be applied to each package. We don't allow anything like C++'s template template parameters, so I don't think non-monomorphisable cycles can appear across packages.

Thanks.

[julien-lange]

Hi Matthew,

From the start of this work, this implementation has reflected the theory from Featherweight Go as much as possible. At some point, we formalised a graph-based algorithm for the nomono check but this ended up being impractical to prove correctness results. I suppose @rhu1 implemented that attempt (he can confirm).

What you suggest sounds fine to me. I suppose you would apply this algorithm from each declaration (types and functions), right?

That is basically what Fig. 23 in the paper does (modulo added complication because we support type params in methods). But essentially, Fig 23 computes the the call graph starting from any declaration, tracking type variables were declared (e.g, T), then it raises an error if a cycle includes a type variable that occurs under a type constructor (e.g., Box[T]).

Happy to talk more if you need help understanding that bit of the paper -- I know the greek letters don't help!

J.

[rhu1]

Hi @mdempsky A main reason for our change was to keep this prototype implementation "close" in terms of presentation to the definitions in the paper. (This is also a reason why this code is quite primitive in many ways, e.g., the naming of types and variables.) So, it was not due to any fundamental problem etc. with a graph-based approach. As Julien said, we'd be happy to talk more about the prototype implementation and/or paper. Your idea makes sense to me. However, I was wondering a bit about the package issue you mentioned. Non-monomorphisable code can arise when generic types are "further nested" inside type constructors in recursive code (and so could end up being nested to an unbounded depth). I was wondering if it's possible for such cases to occur between mutually referring types/methods across different packages? For reference, a small example (within a single package) is in Fig. 10 of our paper (linked by Julien above).

[mdempsky]

Thanks very much for the responses and background context on the algorithms you used.

I was wondering if it's possible for such cases to occur between mutually referring types/methods across different packages?

In Go, the package dependency graph has to be acyclic and methods must also be declared in the same package as their receiver type. So unless I'm misunderstanding your question, no, it's not possible to have mutually referential declarations across packages.