4 ms·

How do I learn to write a type checker? Got any suggested readings?

krat0sprakhar 7y ago
I have a simple implementation of the Hindley Milner Type Inference algorithm in OCaml that should be easy to grok: https://github.com/prakhar1989/type-inference https://github.com/prakhar1989/type-inference
PeCaN 7y ago
Type checkers are actually surprisingly easy to write. I recommend learning about unification (in the logic sense), maybe just by playing around with Prolog. After you understand that I think type checking is rather easy to figure out (it's literally just unification).
- chubot 7y ago
  I think it depends on whether you have type inference or not. If you have type inference, then it's like unification. If you have explicit type annotations, it's even simpler than that. https://eli.thegreenplace.net/2018/unification/ https://eli.thegreenplace.net/2018/unification/ https://eli.thegreenplace.net/2018/type-inference/ https://eli.thegreenplace.net/2018/type-inference/
  - seanmcdirmid 7y ago
    And if you want nominal sub typing, F-bounded generics, and some inference, things get really fun.
    - rurban 7y ago
      Nominal subtyping is trivial and unsafe. The fun starts with structural subtyping.
      - seanmcdirmid 7y ago
        Nominal sub typing is hard from trivial and calling it unsafe is non-sensical. Structural subtyping yields poor error messages and does not support encapsulation very well, especially if you also want separate compilation.
barrkel 7y ago
Imperative languages without type inference (for variables and functions, that is) work from the bottom up. Symbols (variables, functions) have declared types, constants have known types. Operators have overloads, and depending on the arguments a particular overload is chosen which best matches, and its return type is the type of the operator expression. Type conversions may need to occur along the way to make the arguments to operators or functions fit. The hairiest thing is usually overload resolution (both operator and function, if implemented). Determining the set of applicable overloads may depend in the types of the arguments, scoping rules, or generic instantiation if it's in the language, and determining the best overload depends on weighing up coercions, subtyping and polymorphism. Simple rules may lead to rejection of overload selection as ambiguous in situations where programmers don't want to define more overloads.

I have a simple implementation of the Hindley Milner Type Inference algorithm in OCaml that should be easy to grok: https://github.com/prakhar1989/type-inference https://github.com/prakhar1989/type-inference

PeCaN 7y ago

Type checkers are actually surprisingly easy to write. I recommend learning about unification (in the logic sense), maybe just by playing around with Prolog. After you understand that I think type checking is rather easy to figure out (it's literally just unification).

chubot 7y ago
I think it depends on whether you have type inference or not. If you have type inference, then it's like unification. If you have explicit type annotations, it's even simpler than that. https://eli.thegreenplace.net/2018/unification/ https://eli.thegreenplace.net/2018/unification/ https://eli.thegreenplace.net/2018/type-inference/ https://eli.thegreenplace.net/2018/type-inference/
- seanmcdirmid 7y ago
  And if you want nominal sub typing, F-bounded generics, and some inference, things get really fun.
  - rurban 7y ago
    Nominal subtyping is trivial and unsafe. The fun starts with structural subtyping.
    - seanmcdirmid 7y ago
      Nominal sub typing is hard from trivial and calling it unsafe is non-sensical. Structural subtyping yields poor error messages and does not support encapsulation very well, especially if you also want separate compilation.

barrkel 7y ago

Imperative languages without type inference (for variables and functions, that is) work from the bottom up. Symbols (variables, functions) have declared types, constants have known types. Operators have overloads, and depending on the arguments a particular overload is chosen which best matches, and its return type is the type of the operator expression. Type conversions may need to occur along the way to make the arguments to operators or functions fit. The hairiest thing is usually overload resolution (both operator and function, if implemented). Determining the set of applicable overloads may depend in the types of the arguments, scoping rules, or generic instantiation if it's in the language, and determining the best overload depends on weighing up coercions, subtyping and polymorphism. Simple rules may lead to rejection of overload selection as ambiguous in situations where programmers don't want to define more overloads.