I'm new in type systems and type inference. My goal is to implement static type system and type inference algorithm for OOP language without types (the close example is JS without dynamic features like reflection and introspection).
My first idea was to implement static type system and type checking algorithm, and then implement type inference for this system. I've checked several articles about type inference (Object-oriented type inference, Type inference for static compilation of JavaScript, Type Inference of SELF) and they all skip the type checking part, so I'm a little confused about my idea.
The main question is: how is type inference related to type checking? Do we need to do a type check after type inference? How is this implemented in existing languages with type inference (fully and partial)?
I haven’t actually implemented a static type system, but here’s how I would currently make a distinction between type inference and type checking:
Type inference assigns a set of types for parts of the program without explicit types. This process could fail if the type of part of the program is ambiguous and/or contradictory in a way that the compiler/interpreter cannot deal with.
We can use a slightly more generic term “Type Assignment” to include both types assigned via inference and through explicit annotations.
Type checking confirms that the pieces of the program fit together properly, regarding types. This can happen after all the type assignment for the given pieces are done. For example, If a given function has a given type assigned, in many languages it is still syntactically possible to call it with values with incorrect types.
Note that it would be possible to write an implementation where type inference and type checking are mixed together, but it isn’t necessary to do that. For example, given a program with a function foo calling a function bar, foo and bar could have their types assigned and the callsite type checked before moving on to the rest of the program.