• Background and Purpose: In recent years, there's been interest in tools for detecting bugs to improve product quality and programmer productivity. Traditional static type systems require much manual annotation. Modern programming languages use type inference to provide benefits with fewer or no manual annotations. The most popular form is based on the Hindley-Milner system, but it has limitations. Stephen Dolan introduced Algebraic Subtyping in his 2016 PhD thesis, but it's academic and lacks practical implementation guidance.
• Subtype Inference: Most current type inference systems use Hindley-Milner, which is based on unification and leads to inflexible and unintuitive systems with many language-specific hacks. Subtyping, on the other hand, ensures values have compatible types and follows the program's data flow without spurious type errors, making type inference more powerful and intuitive. It also enables new programming styles and removes the constraint of maintaining a convenient manual type syntax. For example, Rust uses structurally inferred traits for static analysis.
• Obstacles: There are two main obstacles to fulfilling the vision of a completely type annotation-free codebase. Performance is a concern as cubic biunification has worst-case cubic time complexity compared to Hindley-Milner's linear time complexity. However, in practice, worst-case time complexity is not a major issue for popular programming languages. Modularity is also an issue as large codebases may use manual type annotations for various reasons, but a type inference system without manual annotations still offers benefits.
• Cubiml Tutorial: Cubiml is a simple ML-like language implemented in Rust that compiles to Javascript and is used to demonstrate cubic biunification. It uses OCaml-like syntax. It has booleans and conditionals (where if is an expression), records and fields (accessed with .name syntax), functions (take one argument and are called by suffixing an argument), let bindings (create local variables), recursive let bindings (allow self-reference), mutual recursion (multiple functions referring to each other), and case types and matching (for making decisions based on runtime data in a type-safe manner).
• Conclusion: This concludes the overview of cubiml's syntax. In the next post, the compiler's front-end will be implemented, which is responsible for parsing the input and translating syntax-specific details into calls to the type checker.