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.
@Qqwy Since you are doing some typing stuff extensively I’d love your input on the API interface, or some of the more interesting choices that I’ve made (e.g. with Maps https://hexdocs.pm/mavis/Type.Map.html#content)
Woo…you’ve been putting in some work!
Random question: Is there a reason why isa? is not is_a?? It seems like you’ve used snake case mostly throughout so that one popped out at me. Perhaps there is precedent for that in other languages and I am just not used to seeing it or it is reserved in some way.
because is_ typically indicates “guard” and I don’t like confusing people. Looks like it had the opposite effect. I struggled a lot with that one, maybe I should just steal the javascript keyword.
it only does the type analysis, so not really =D. I gotta build that library. i don’t think there are too many use cases for this except for compile-time tools, since the type system is not typically used at runtime.
Thank you for directing me to your project! It looks very interesting. I am very happy that different points in the design space of typing are being explored by these various Elixir projects now .
With your project I can already see that you are pushing somewhat against the same boundaries as my run-time type checker project is, in that Erlang’s built-in typespecs have certain odd limitations (compare for instance [integer] (“list of 0 or more ints”), [integer, float] (does not compile), [foo: integer] (“a keyword list containing keyword :foo with an integer”), [foo: integer, bar: float] (“a keyword list with :foo containing an integer and :bar containing a float in any order but both need to be in there somewhere”).
I really like what you are doing with checks for unioning, intersecting and checking for subtypes of types. I think these operations can be very useful for practical purposes .
About Type.Map specifically:
What is the reason for the deviation:
?
Built-in Elixir maps used in typespecs do not do the same: map() assumes ‘any map’, but %{} assumes the empty map. I do agree that %{} meaning “empty” in types and values, but ‘any map’ in patterns might be confusing, but I do not fully understand how you are deviating here.
Other than that, I think you mostly nailed the interface for Type.Map.
I think the list wierdness is elixir’s syntatic sugar over the typespecs. It does make sense that [integer, float] does not compile; but [integer, …] has to be a special case, and [foo: integer, bar: integer] is just sugar for [{:foo, integer} | {:bar, integer}] because who’s got time in life to write all those symbols? They’re so far away from the home row! (j/k the elixir type syntax does cut down on line noise and i like it, if it does poke a bit at the OCD in me).
Point #1 - I do get that we want there to be a ‘required’ type of map element, for structs and the like, but I don’t know what this means: %{required(integer) => integer}. Another slight complication is that we can’t have nice things like %{required("my_field") => String.t} for json specs =(, the best we can do is %{required(String.t) => String.t}, but like the integer case, I don’t know what that means. I think something that maybe should be possible with mavis is to make that sort of thing possible via plugin, but I don’t want to push beyond the boundaries of the type system until at least Selectrix exists.
Maybe someone can explain to me what it means to have a required type that is an aggregate, non-singleton type, and, in particular, how I can do typechecking with those types?
Point taken on #2. Perhaps it shouldn’t be called a “deviation” in the docs. so much as a clarification.
@Qqwy - Not that you’re looking for another dependency, but would there be any cause for consideration to use Mavis for specific low-level checking in your TypeCheck library?
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.
I wouldn’t say that about mavis; I specifically broke it off of selectrix so that it could be use by other people who would like to perform set theory operations over erlang types. The isa? function, for example is created for this purpose even though I’m pretty sure selectrix will never use it.
I wonder if you could use this to encourage people to write typespecs in elixir_ls - if you specced a function and elixir_ls sees that the running value might be an elixir struct, then it can provide tab completion suggestions once you hit the . map dereferencing operator
not a dumb question! Thanks for the feedback. I think at least I should put up an example of using Type.fetch_spec / Type.fetch_type!, but to be honest, most people won’t be using this library unless they want to build compile-time tools that understand types. You could do runtime checking, with Type.isa?(spec, term). I don’t recommend that in prod, but maybe in test? Maybe with property testing?. My plan is to do a new release this afternoon, so I’ll add these examples and a description in the module landing page.
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:
.
.
