ityonemo
Mavis - Typing Library for elixir
Introducing Mavis, a comprehensive Typing Library for Elixir:
Mavis fully utilizes Elixir’s Protocol system to create a fluent and composable type analysis library for erlang and Elixir’s types. The type analysis logic is hand-crafted to fit the pragmatic choices that were made when the BEAM was designed (and extended, e.g. with the map type), and does not attempt to square the BEAM’s types to a preexisting type-theoretical framework. Because of the operations that it supports, I expect it to be able to be more powerful than Dialyzer or Gradualyzer.
Hex:
https://hexdocs.pm/mavis/Type.html
Github:
This is the first stage in my “Selectrix” project which is a shot at bringing compile-time type analysis to Elixir as an optional add-in library.
I’d love it if the community could play around with the library to get a sense of what it can do (and hopefully also find bugs!)
Most Liked
ityonemo
update video: https://www.youtube.com/watch?v=2ooSWOCBTPQ
ityonemo
video update https://www.youtube.com/watch?v=m3nYFEyNJr0
ityonemo
Updated Mavis to 0.0.5, with support for two new types (not yet? supported by dialyzer) that I’ve discovered in the BEAM. Made a couple of videos explaining these types:
top-arity functions:
min-arity tuples:
ityonemo
Updated to 0.0.6, with support for pinned types in tuples, refactored way of specifying types that match typespecs E.G. (Type.integer(), Type.nonempty_maybe_improper_list()) and Type.normalize/1 which will take Mavis’ opinionated types and downconvert them to Elixir/Erlang standard types.
Qqwy
The primary goals of both libraries are different and do not fully align:
Mavis’ goal is to be the foundation of a compile-time static type analysis engine.
TypeCheck’s goal is to be a fast and flexible run-time type checking tool focusing on readable error messages and re-using type specifications for type-checking, proptest-generating and documentation.
When both mature it is possible that some kind of bridge between them is created, but I do not think that it is useful for one to depend on the other at this time.







