Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez [1].
With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster.
As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2].
With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster.
As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2].
[1]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
[2]: https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"