2
$\begingroup$

I understand how a type inference algorithm infers types within a single file by building on top of already inferred types and identified constraints (e.g. in the Hindley-Milner type system).

I am wondering about how this process works/is implemented for languages where some bindings are imported from other files. I wasn't able to find any useful information elsewhere, so I figured I'd just test my luck here.

The trivial approach would obviously be to leave the imported binding type-less (e.g. substitute a type variable) and continue adding constraints. Then, when the actual definition of the binding is encountered in the other file, it is checked that the constraints and actual type can be unified. This approach has the major drawback that it basically discards all type information regarding a binding that may be present where it is defined.

Building on that first approach one could start by identifying an optimal order of analyzing files. In the case where there are no circular dependencies, this additional step would solve the problem. But in a lot of cases there are circular dependencies.

In TypeScript for example (afaik), circular dependencies are allowed without any loss of type information.

How is this problem usually handled in type inference algorithms? Are there any resources/papers that describe this problem?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

The first option is to simply process all the imports and see what is in them. This is not what you are asking, because it is equivalent to having everything in a single file, more or less. And it can be prety expensive to process all the dependencies.

What you are looking for is the notion of interface, also known as signature. To simplify things, an interface lists all the constants that are implemented in a given unit (file, module) together with their types. Thus, given that some file imports file X, all we need is an interface for X. Such an interface may be written by the programmer, or generated automatically and stored somewhere by a compiler, there are many ways to accomplish this.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Exactly this: in SML for example, structures have signatures (which can be defined separately, inline, or inferred) just like functions (vals are a bit different). Thus when you include the structure (such as via the compilation manager CM) you get both the structure and the signature for type-checking. $\endgroup$
    – D. Ben Knoble
    Apr 1, 2020 at 13:25
  • $\begingroup$ Right, I didn't want to mention too much theory, but definitely the place to look for a good treatment of structures and signatures is ML, be it Standard ML, OCaml, or some other variant of it. $\endgroup$
    – Andrej Bauer
    Apr 1, 2020 at 13:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.