Type inference gives programmers the benefit of static, compile-time type checking without the cost of manually specifying types, and has long been a standard feature of functional programming languages. However, it has proven difficult to integrate type inference with subtyping, since the unification engine at the core of classical type inference accepts only equations, not subtyping constraints.
This thesis presents a type system combining ML-style parametric polymorphism and subtyping, with type inference, principal types, and decidable type subsumption. Type inference is based on biunification, an analogue of unification that works with subtyping constraints.
- Composable Builds for OCaml with Jbuilder
- MirageOS Hack Updates
- Databox Launch Event: 24th March, Cambridge
- Formalizing the OCaml multicore memory model
- MirageOS Hack Event 2017 in Marrakech
- Irmin 1.0 Released!
- Scaling Software Modularization with Topkg
- MirageOS 3.0.0 Released!
- Making PPXs portable with ocaml-migrate-parsetree
- Feedback on cmdliner doc language changes