High level library goals

[baldwindavid]

I'm trying to understand this at a very high level. My current understanding is that upon compilation this will be able to uncover issues by inferring types "when it reasonably can" with compiler warnings. When it cannot, standard Elixir typespecs can be used to give the library more information to work with. Correct?

That would be plenty, but I'm wondering if there are plans for further ways to specify more complex types that typespecs cannot handle. Basically, will it handle any extended syntax that traditional typespecs might not? I'm not even sure that it should, but one thing that has been handy with the TypeCheck runtime checker is that it supports any custom Elixir (for better or worse).

[ityonemo]

Thanks for the question! Apologies for the wall of text, but I decided that this was an opportunity for me to organize my thoughts as well.

Please be aware that currently the system currently only does type inferencing, and not type checking, I haven't figured out how the system should deal with if an impossibility occurs, or how to detect or surface warnings, that's an issue of how the mechanics of the inferencing system can be extended to support the checking case (I do want that to happen, I just wanted to see some nice intermediate results first).

Selectrix will (or, actually, already does) provide hooks for compile-time typechecking. There are two phases in typechecking. The first is making sure that the functions are internally consistent, and dropping warnings and errors for questionable steps. The second is verifying that your dialyzer types are correct. To do this it will need to reach into the machine code and run type checking. I'm currently refactoring this so that opcode analysis will be modular. So if you want to handle an opcode differently, you can add a module to the top of the stack and it will special case it, before the rest of the opcode handlers get a chance to see it.

The next system that Selectrix will provide is "give me the type of function X" - you can supply a list of modules that have a typing behaviour. I'm hoping this is not a leaky abstraction. And Selectrix will rifle through the modules and try to figure out what the type is. Top layer would probably be an ETS cache, followed by user overrides, then, below that some sort of PLT-like lookup (those would live in selectrix), below that checking typespecs (currently provided by mavis), and finally the last layer would be actually running inference on the module (mavis_inference).

Note that the compile-time typechecking requires the "give me the type" service, because as soon as I hit a "run a foreign call" opcode, I'll need to do a lookup. So it would be nice to be able to inject the dependency on that and close the loop.

Finally, at the base of all of this is Mavis, which provides basic rules for types. It's currently not modular, but I want it to be slightly more modular. I have some ideas on how to do this that are kind of half-baked, but I want to actively be using Mavis in the primary use case for a bit before I dive into it.

Note that Selectrix will not have a hard dependency on Mavis. I don't know what's coming forward with Facebook's erlang typing adventure. In theory, nothing that Selectrix does should be dependent on what logic or datastructures you use to handle your types, so long as you implement a set of type theory primitives, so separating those concerns so that if we need to do a hard reboot on the underlying logic is important to me.

So, let's say you want "smarter enum logic" that checks that the lambda you're passing will interact favorably with the Enumerable that you're sending. That could be implemented with different strategies. Maybe you could implement it at the lowest level by writing an opcode processing module that pattern matches on foreign calls to the Enum module and triggers special logic, then throw that into the stack of opcode modules as an override to the generic opcode processor. Another possibility is if I allow some sort of "lambda" system in the typechecker you could drop it between the "PLT-lookup" and the "checking typespecs" phases.

A few other examples that I care about:

• I'd like a system by which you can declare that a module carries behaviour information, for example module([:gen_server | MyBehaviour]) and if your variable is tagged with this type, it gets checked when you try to do my_module.call(pid, :do_the_call), and gets the OK.
• I'd like a system that automatically analyzes all of the places in your module where you run :gen_server.call/2, :gen_server.cast/2, and makes sure you have handlers for those messages. Maybe even more ambitiously, I could track Task.async/1, as well. This should be opt-in because it requires you to stick to bundling your module API calls with your module (I think that there are some who use a pattern where module API calls are in a different module).

To answer one of your questions: Will handle any extended syntax that traditional typespecs might not? Aside from a few special cases where the builtins are not powerful enough (I really want a String.t(<size_of_binary>) type, and module(<union_of_behaviours>) type), I don't plan on using extended syntax. Instead I think the right way forward is to be slightly inexplicit and require overrides to detect the standard syntax and take action based on that. Again, though, if FB's typing system changes things, or triggers an EEP where the logic of typing in the BEAM gets fiddled with, I hope that the modular system will be able to cope.

[baldwindavid]

Thanks for the response. I appreciate the explanation outlining the separation of concerns between selectrix and mavis (and potential FB erlang changes, custom primitives, etc.).

I've noted similar in a few places which you've commented on, but my dream vision of elixir would be to write elixir without typespecs with compile-time type checking. All standard elixir typespec syntax would be supported (including referencing remote types) and would provide the typechecker more guidance. These seem to be right in line with the goals of Selectrix/Mavis.

Having the option of turning on this same typechecking for runtime (and per environment) would also be nice. While this is more in TypeCheck's wheelhouse/goals, it seems like your library could be used as a basis for the same sort of thing especially if it ends up supporting ALL of the existing typespec syntax, remote types, etc.

That last part seems like something where Mavis and TypeCheck could potentially work together. I could be misunderstanding, but it seems like both libraries need some underlying type inference / checking infrastructure that could potentially be the same library. I would love to see those worlds merge such that you guys aren't working on the same thing / duplicating effort separately if that is the case.

[ityonemo]

I absolutely see TypeCheck as occupying orthogonal niches. In my mind we aren't competing, and I think it wouldn't be hard to turn on TypeCheck for data ingressing and egressing functions (for example in :test, or maybe even in "safety-critical paths" in prod) with hooks against Mavis to pull the specs out from the module (or supply custom specs).

I could be misunderstanding, but it seems like both libraries need some underlying type inference / checking infrastructure that could potentially be the same library.

My thoughts exactly =D