How to make Dialyzer more strict?

tim2CF

If we have function with typespec that always returns value with incorrect type

@spec hello(integer()) :: map()
  def hello(int) do
    case int do
      1 -> :foo
      _ -> :wtf
    end
  end

then Dialyzer generates warning, good. It is as expected.

done in 0m1.08s
lib/hello.ex:16: Invalid type specification for function 'Elixir.Hello':hello/1. The success typing is (_) -> 'foo' | 'wtf'
done (warnings were emitted)

But if

  @spec hello(integer()) :: map()
  def hello(int) do
    case int do
      1 -> %{hello: "world"}
      _ -> :wtf
    end
  end

then

done in 0m1.07s
done (passed successfully)

Why it not generates any warnings when there is clause where wrong value is returned from function?
And if it is feature, not bug - how to make behaviour more strict?
It would be perfect if there will be flag to generate warnings when at least one possible clause has incorrect type.

51 comments

#dialyzer #algebraic_data_type #typespecs

7 11218 51

2020-01-13 13:34:45 UTC

Showing Posts 1 to 10

Show Best Posts
Show All (oldest first)
Show All (newest first)

mmport80

Dialyzer uses optimistic type checking.

So if it can find one route through the code which type checks, then it is happy.

Crazy, huh?

Function guards enforce input strictness, but AFAIK, there’s nothing straightforward that enforces output strictness.

IMO, cases / ifs which output different types is probably a code smell, perhaps someday the Elixir compiler can show a warning in future…

Dialyzer is a terrible tool, compared to what you find in ML languages.

Post #1

rvirding

Creator of Erlang

The reason for this is that dialyzer was added afterwards to a very dynamically typed language, then Erlang and now Elixir, with the requirement that it was not allowed to change the language. At all! So it does what it can. You will find that it doen’t just type a function but type checks a function and the calls made to it together to see if they agree.

Also in some ways dialyzer basically ignores a function spec when type checking so you don’t really need one to get the type checking. If you give one it will check that it is consistent with what it can work out about the function and it will use it when reporting type errors, which can be very useful. Actually same with type defs. Though both are extremely useful for documentation.

The compiler always ignores type specs except for some basic syntax checks.

Depressing no?

Post #2

stefanchrobot

Question is: can this be improved in the future? TypeScript is doing a similar thing for JavaScript. On the bright side, the coverage of different use cases is increasing while keeping the compilation time fast. The bad thing is that IMO the type system is kind of exploding with complexity.

Seems like Elixir could add opt-in strict type checking.

Post #3

gon782

Maybe Elixir could just be what it is and other languages on the BEAM can build a foundation much more suited to this kind of thing. I would rather have something designed from the get-go to be strict than trying to bolt it onto Elixir/Erlang.

What I mean is that I think you’ll see better results trying to design for something like this much earlier and languages like Alpaca are probably a better bet in this regard. If the people who really want a strongly, statically typed on the BEAM (myself included) simply tried to help with Alpaca, maybe we could end up with something that could even become our BEAM language of choice.

Post #4

stefanchrobot

I’d rather have this in Elixir 2.x. The downside of a new language is the fragmentation of the community. What’s the point of a new language if you can’t get hired to work in it? It’s still tough to find a job in Elixir.

Post #5

gon782

I work with both Erlang and Elixir, i.e. I work with the BEAM. Would I have issues trying to convince project leaders to let me use LFE? Yeah, but the value proposition of something like LFE isn’t as obvious as a statically typed language that could allow for far less cognitive load. The value of a language like that would be self-evident at some point and it’s a much easier comparison than external statically typed languages vs. Elixir as well.

Not to derail this too much, but I wouldn’t want to work with someone who seemed to have issues with the Erlang/Elixir divide, because all the important things in Elixir are the important things for the BEAM in general. The same would apply to any other language on the BEAM, really.

Post #6

LostKobrakai

Would elixir itself really be changed to bolt on type more strict type checking? I mean from my naive standpoint the constucts for using types are there, it’s just how dialyzer is using those, which makes people wish for a different solutions.

Post #7

gon782

Not for more strict type checking only, perhaps, but certainly for a better type system. If you want a decent language in terms of type system you should implement it in compiler passes and probably just output BEAM bytecode.

Probably my mistake, I assume in these kinds of conversations that we’re talking about going the whole way and supporting actual competent type systems, though in this case that’s probably false.

Post #8

hypno

I’m not an expert on types but we already have type declaration syntax that the community actively using in Elixir. The problem is how Dialyzer interprets them (too loose). Maybe a stupid question but can’t we just build source code level (Elixir AST) analyzer as a hex package (archive?) that reads source code like Code.string_to_quoted |> Macro.expand, and uses the type specs AST to match them against the source code AST?

We are very interested of stricter typing in our company and are willing to put a remarkable bounty on this project, if it is viable option ofcourse

Post #9

OvermindDL1

Yes, in fact it could even be done via a library, this is what my TypedElixir and MLElixir experiments do (in different ways).

(Wish I could get time to work on it some more, it’s so fun making such things!!)

Alpaca has promise, but it is more ‘pure’ in typing, like having OCaml compile to Javascript. It doesn’t have great integrations with Elixir and macro’s just don’t work at all, in addition it can’t use the types that the rest of the Beam more focuses on, as well as it doesn’t black box PID’s but instead tries to ‘type’ them (which seems inherently faulty on a BEAM language to me), etc… It is good as a more pure language, but not as something to interact with Elixir libraries.

Elixir is expressive enough (though the syntax definitely has some warts, like a couple random n-arity ‘functions’ as one example…) to do it as a library though. ^.^
Then you can mix-and-match as you want!

It actually would be possible to make an LFE library that can make and consume Elixir macro’s though, unlike Alpaca.

You could type LFE as well via a library for it.

Except Macro’s, Parse Transforms are indeed as powerful in erlang but just not as easy to use. Macro’s are where Elixir gets its power (a proper macro system in erlang would make choosing elixir over erlang far far harder with only the library ecosystem (because of elixir macros) being the deciding choice, I wish elixir was more erlang/beam compatible instead of making custom/new formats somehow…).

Precisely this. A good type system not only catches a lot of bugs (making entire classes of bugs just outright impossible), but it can also generate better code, make smaller and more expressive code constructs, and more!

As stated above, just strengthening it alone will make checks better, which is always good of course, but you don’t get the gain in code generation efficiency nor better code constructs. That is why both of my TypedElixir and MLElixir experiments tries to ‘use’ dialyzer specs as much as possible, but also expanded above and beyond those.

Oh I wish I had the time! It would be so fun to do!

Post #10

Load more posts (41 remaining)