The Petr type system is based on a combination of the [[Hindley Milner Algorithm]] and literal subtypes. It focuses on ergonomic displays of errors, and bridging the gap between the current bleeding edge of static analysis and actual usability in real development environment. #