Mavis - Typing Library for elixir

@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 Type.Map — mavis v0.0.6)

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.

Maybe kind_of??

Excited to try this out! Do you have a sample project that is using Mavis that we could take a look at?

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.

That makes sense

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?