I’ll be honest, there is a lot about dialyzer output that confuses me.
Right now I’m confused by “The call … will never return since it differs in the 1st argument from the success typing arguments”
file.ex:23: The call ‘Elixir.Timber’:add_context(#{‘struct’:=‘Elixir.Timber.Contexts.UserContext’, ‘email’:=, ‘id’:=, ‘name’:=‘nil’}) will never return since it differs in the 1st argument from the success typing arguments: (maybe_improper_list())
My reading of that error is that dialyzer thinks that me calling Timber.add_context will fail because I’m sending in a struct and it is expecting input of maybe_improper_list.
Even though I know this works and Timber is an external dependancy, I wanted to understand why it wanted some type of list. I cracked into their code. Here is the code for add_context/1;
@doc """
Adds a context entry to the stack. See `Timber::Contexts::CustomContext` for examples.
"""
@spec add_context(map | Keyword.t | Context.context_element) :: :ok
def add_context(data) do
CurrentContext.load()
|> Context.add(data)
|> CurrentContext.save()
end
There is no explicit mention of maybe_improper_list, and as far as I know map covers the fact I’m passing in a struct.
Am I interpreting the output correctly? Any help would be much appreciated.
I can also add that sometimes dialyzer’s opinion of what should happen doesn’t always agree with reality. It tends to view all type mismatches as generating errors which they don’t always do.
Then I can’t really help you. I am not a big fan of dialyzer and don’t use it at all when I program elixir. I recall reading somewhere that dialyzer had problems with structs, but unfortunately I have no further details. Sorry I can’t help you more.
A map and a struct are different types. I assume in this case that Context.context_element is a maybe_improper_list(). Since dialyzer needs to give some error, I guess it picks the last provided type as the potential success type.
I had a look - there’s a ton of issues with the typespecs in this project. For your specific problem, Dialyzer says that the typespec for add/2 is wrong:
lib/timber/context.ex:48: Invalid type specification for function 'Elixir.Timber.Context':add/2. The success typing is (_,maybe_improper_list()) -> any()
Which is in turn because the spec for sub-functions are wrong. For instance:
The user context spec says id is a string, but to_api_map takes it as an integer. Dialyzer infers this is impossible.
Or take insert/3:
It accepts an atom as the second argument, violating its own typespec a few lines above which says it must be a context struct.
So, at the end of the day the problem is the typespecs are wrong, causing Dialyzer to think that the functions will not work if you pass them a context struct. So it infers the “success type” is a list, because it’s the only thing that would work correctly according to the provided specs.
I’ve hit similar issues in libraries before. It’s frustrating when package authors add typespecs for documentation purposes, but don’t run dialyzer in CI to check that the code and specs agree.
I wish dialyzer was faster and built in as part of the compile process (opt-out maybe, but really not even that).
And there is no reason it is so slow, even OCaml’s typing system is substantially faster in ways that puts dialyzer to utter shame, just a raw typing pass over a thousand files of source takes mere seconds, and that is with no cache files built yet, ‘with’ those then it only takes time of whichever files changed since the last run.
But see, that post above that shows the typing bugs in that library probably also shows that there are actual bugs too, this is why strong static typing is so useful…
I think one reason it runs slow is that it doesn’t trust you and must really check the system rather than a module. How can it know, really know, the types of functions in other modules which you call? The only way is to go out and check it.
I don’t really expect everyone to remember to run dialyzer in development, but for open source projects on github, it’s simple to add a dependency on dialyxir, run it on travis after the tests, cache the _build dir to avoid rebuilding the PLT from scratch between builds.
OCaml has almost no type checks in the source, like at all, even something like:
let doSomething a = Vwoop.doSomethingElse a
Which in Elixir is just:
def doSomething(a), do: Vwoop.doSomethingElse(a)
Is entirely not only well formed but completely typed.
What OCaml does is first it parses the files and gets the call information, building a dependency graph, which you can dump out in a variety of formats, but by default is just a simple list of dependent files based on another file via using the command ocamldep, so if the above source is in file bloop.ml (and you have a vwoop.ml file) and you ran ocamldep bloop.ml it would output:
bloop.cmo : vwoop.cmo
bloop.cmx : vwoop.cmx
A quick primer on the file extensions (think of ml and mli being like C’s c and h files, except mli are entirely optional and if missing it assumes the entire ml file is exported, you can even have the compiler dump out an mli file from an ml file then just prune whatever you don’t want visible): ml source files mli like source files except no definitions, it just shows names and what’s exported and such o output object file, like C generates o files, you can even link these o files into a C program or vice versa of GCC’s format. so an output shared library, like in C a an output static library, like in C cma bytecode library (when running ocaml in bytecode mode, think of these like python’s pyc files, bytecode is easier to debug than native code and only about 4-20x slower, which is a LOT faster than python, though native code is about on par with C speed) cmo files are cache files for the bytecode generation cmx files are cache files for the machine code generation (generated from the cmo files, and cmo are made from the source ml files)
So what the above output of ocamldep means is that both the bytecode and native code builds will absolutely require vwoop’s to exist first.
So what the compiler does is just run a dependency solver on the main file you are compiling first (like the entrance file in C, you can specify multiple too, like in C), and gets a list of files it depends on, then it recursively goes through those building the entire dependency tree.
Then it starts building, it takes the lowest level files first, the ones that depend on nothing or just depends on external’s (mostly the standard library) and builds the cmx/cmo (depending on if you are doing a machine code build or bytecode build) into it’s version of Elixir’s _build directory (traditionally named lib fun enough, that is a nice conflict with elixir, src is the traditional source directory name). It keeps the ‘interface’ of the file cached in memory as it compiles the later files (or loads the appropriate cmx/cmo to get the interface for it if it was compiled before), the sole purpose of which is to get the names and types.
So if vwoop.ml is:
let doSomethingElse a = a * 2
let id a = a
Then the interface of vwoop is (acquired via ocamlc -i vwoop.ml) is:
val doSomethingElse : int -> int
val id : 'a -> 'a
So then the bloop.ml file at compile time see that the Vwoop.doSomethingElse is typed as int -> int so it resolve Bloop’s doSomething’s argument a to that it has to be an int and that it returns an int as well, thus ocamlc -i bloop.ml outputs:
val doSomething : int -> int
Now, OCaml is not at all ‘just’ Hindley-Milner, though that is the basis of it’s resolution, always resolved by function definition. It is the defined ‘interface’ that a module must follow.
Now, you may not have the module you are calling, like Vwoop, but you would still have it’s mli interface file then (or the cmx/cmo cache files).
Now what if vwoop has the interface we defined above, but instead it had let doSomethingElse a = print_string a, thus the inferred type is actually string -> unit, it will fail to compile because it does not match the required interface. This is how you replace source files, the systems makes sure they follow the same interface. They can export more sure, but you cannot break the old version without doing a full version increment, which involves everything else to update as well.
Now, dialyzer has it a lot less easy of course still. Sure it can resolve that blah a = a + 4 means that a has to be a sumtype of an integer or a float, and it returns one of those as well, but larger things are not as fast, so it likes to have it’s own cache file as well (usually pre-baked with the standard library and more). However, that still does not explain the slowness.
Let’s take this, ocaml during the most complex compile, I.E. to machine code with full optimizations enabled, give it a massive project of hundreds of source files and thousands of types and maybe a few hundred dependencies each totaling to thousands of source files and maybe even millions of types, these are the programs that ocaml compiles the slowest, and even then it will parse, generate the dependency tree, type everything, run optimization passes that get it to near if not at or sometimes even better than C speed and output the final machine code all in mere seconds. The longest legit OCaml program (not something making a worst case even worse) I’ve heard of compiled in 40 seconds on much older hardware from a fresh compile (and later compiles that only recompile what changed takes <1s, always), puts to absolute and utter shame the elixir compiler (and most other compiles) and elixir is not even doing any strong typing steps or a massive amount of optimization passes, it is just ‘slow’, and dialyzer is even worse.
OCaml’s compiler does not trust you either. If you do something like let blah (a : int) : float = print_string a it will yell very loudly at you and refuse to compile because both a is typed as int but print_string only accept strings, and print_string a returns unit yet the function says it should return a float, it checks every-single-expression-in-the-program to make sure you did not do something wrong.
Right now there are only two ways to make the ocaml compiler slow as well (I’ll describe why I’m showing these soon), first being a polymorphic generically typed function definition that calls a polymorphic generically typed function definition multiple times that calls a polymorphic generically typed function definition multiple times and repeat this a few more times, and they all have to be defined in the same scope. This becomes an exponential growth in the number of types and you can hit billions in just a dozen calls. The second way is a similar thing but the higher typed Modules that generate modules from other module types, do the same type of recursive calls a dozen times and you get a similar problem. In reality it is almost impossible to hit these in real life and you have to actually try to go to these cases to hit them, and these are not cases that would happen in Elixir/Erlang either (which is why I’m showing them), thus there is still no excuse as to the slowness Elixir/Erlang.
Do note, that in the OCaml standard library the + function is typed as int -> int -> int by default, but you can of course redefine it in any scope, and in fact when implicit witnesses land there will be modules made that type it like (t = implicit module Addition) -> t -> t -> t or something similar (standard witness pattern, pretty universal through-out OCaml) which would then work on any type that has a module in scope that fulfills the Addition interface (so you’d have an IntAddition and a FloatAddition and whatever else you want). The current definition of + in the stdlib is a holdover from it’s SML origins, there are plenty of libraries that use the witness style for it already too.
So yes, OCaml will parse the source code, go over every-single-function in the module and sub modules and the source within them to get the type of each function and make sure that the body fulfills the type correctly as well, and optimize and compile and generate the machine code for whatever architecture, all in a tiny fraction of the time that Elixir compiles (even faster than Erlang, I’ve had many many (most?all?) old erlang projects that took substantially longer to compile than any OCaml project I’ve had), and yet it does it’s version of running dialyzer and more as well, even if the code is entirely untyped in the source. In addition thanks to the cache files in it’s build directory the repeated rebuilds only update and check what has changed and checks what references those changed files (and if the type on a name changed it will recompile those files as well to make sure they still match as well).
So in reference to your:
I think one reason it runs slow is that it doesn’t trust you and must really check the system rather than a module.
OCaml checks every tiny line of source from the entrance point through the entire standard library and dependencies every time you do a fresh compile and it still does it in seconds at most on average (almost all my projects compiles in <1s for full fresh builds).
And honestly, it probably is not even the fault of Dialyzer, I’ve not looked at it’s code so I could not say, but there is one part of the BEAM system that does indeed become much harder to type check than something like OCaml’s source, and that is that OCaml’s source only allows recursion within a module, modules that call each other need to have the recursive calls put into another module that is then called instead, but even that I don’t think is a computationally expensive problem and it only really is a problem for OCaml because of the language spec requires it, it could be solved by just keeping the recursive modules in memory and just resolving the generic types as far as possible.
The main difference between dialyzer and full HM typing though I’d say is that dialyzer more actually assumes that it does not know, where HM assumes you do know (or you fail out with a resolution failure error). And Dialyzers method is entirely fine for something like the beam/erlang/elixir where things like messages can be entirely unknown, but even then those are representable types, like in OCaml you can have a fully generic type, let’s call it 'a and yet you can still pass it to a typed function like in a switch by testing it’s type first, though this is a case where you do require a little magic but it is entirely doable and representable. However, OCaml has a full type called Polymorphic Variants, so a function can get typed with these by specifying what of them it (or it’s callee’s) uses and this style put into dializer via matching and guard testing (which is thankfully very limited in capability, thus making this pretty easy) would allow recursive definition of even message types (and you could in fact give a warning if the default/unknown case is not handled or marked as ignored specifically as well).
I have no doubt dialyzer could be made faster, but you might have to make it more ‘strong’ against user code, I.E. force the user to type the occasional thing that it cannot know for certain, go fully to an HM typing system. Such a new dialyzer may not be able to type, say, all dependencies if they leave some questionable code untyped, but that is what PR’s are for (or perhaps introduce the concept of type interface files for it as well, to let dependents be able to type their dependencies for such cases).
I can just keep this going, but I should stop… ^.^;
It seems strange to compare the performance of two completely different type systems with different requirements, constraints and different algorithms implementing the type system.
That is what my post was about, that they are different, and yet pointing out that they have so much overlap that it would not take much to have dialyzer act more like a strong typing typer instead of the positive typer that it is now (with some semantic changes about dialyzer in the process so it would not really be backwards compatible as it is now). And some remarks about the slow compilation of erlang/elixir (even though by all rights a dynamic language compilation should be so much faster than something machine code optimized like ocaml, even adding in a ton of OCaml’s macro’s/ppx, though yes they slow it down, not near as much as those still). ^.^;
Is it still dialyzer then? Dialyzer was built with some very specific requirements: no fundamental changes to the language, do not impose a type system and never have false positives [1].
Why is machine compiled language slower to compile? You point out why ocaml is fast to compile but you do not show why erlang/elixir is slow or why dialyzer is slow. If we don’t know why it’s slow then how can we improve it?
Not much in terms of user code, dialyzer would have to be rewritten no doubt. ^.^;
Exactly not, dialyzer is a band-aid due to the lack of actual types in the languages, we really need a better designed language instead.
Primarily because of the number of optimizations performed. It is not hard to compile to the metal, but performing the optimizations to make it efficient to perform to the metal (remember, OCaml averages 1-2x the speed of C) is traditionally very slow, even the ‘latest and greatest’ languages like Rust are dreadfully slow, go however is quite fast but it has a substantially limited type system in comparison to any of the others.
Unsure about erlang/elixir, it could just be BEAM limitations, not looked as of yet, and as stated in the post, I’ve not looked at dialyzer’s code at all, it’s been one of those things I’ve stayed away from thus far. ^.^;
There is a fundamental difference about dialyzer and HM type system. Dialyzer follows the “no false positives” approach (which means it will complain only if it can prove code is wrong), while HM type system follows the “no false negatives” approach (which means it will not complain only if it can prove code is correct). Both can’t be combined.
That was the entire (though condensed) point of my post, that dialyzer is way too weak and it should be far more strict, even if it requires adding in a lot more type information.
Dialyzer is not going to change how it fundamentally works. It would be interesting to see what a stricter type checker can do but there is no point in imaging that type checker would be dialyzer.
