What does HackerNews think of dialyxir?

Mix tasks to simplify use of Dialyzer in Elixir projects.

Language: Elixir

#4 in Elixir
For those of you who are interested by Elixir but find the lack of static typing an issue here are somethings to be aware of:

1. Static Typing is planned and currently the top priority of the team

https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...

2. There is a type checking tool

https://github.com/jeremyjh/dialyxir

3. You can go a long way with pattern matching and guides in the meantime and have alot more guarantees that a typical dynamic typed language.

You might also be interested in https://github.com/jeremyjh/dialyxir

I use both dialyxir and Credo in my projects

> Are many of the other languages you've used strongly typed? That's the thing that gives me pause - I feel like I rely on the compiler a lot in languages where it can do a lot for me, and that I'd be really frustrated managing a large project without it.

As someone who has been writing Elixir professionally for 4-ish years, and who is otherwise about as big of a proponent of static types as is possible, this is simultaneously my biggest critique of Elixir, and also a critique that has ended up being more theoretical than not. I wish that it were statically typed, but in practice that hasn't been slowing me down.

Part of the reason for that is that while Elixir is dynamically typed, I've found that it's possible to pretend it is a statically typed language if you squint just right. By that, I mean making judicious use of typespecs [0], dialyzer [1], Norm [2], and just generally constraining the way you write code to mirror the sorts of code that you'd write in a language that offers algebraic data-types, like Haskell. I've been meaning to put together a blog post on what I mean by this, because I often hear people talking about how unusable Dialyzer is, so I feel like my team is a rare example of a large production app that requires that Dialyzer typechecks on every build. This makes large-scale refactoring of our app almost (but not quite) as easy as it would be in Haskell.

The macro system in Elixir also means that it's possible to write libraries like typeclass [3], that offer compile-time guarantees (using compile-time property tests!) that your implementations correctly implement a given interface. I think that as the language evolves, we'll be seeing a lot more examples of macros that move runtime logic into the compilation step, to offer compile-time guarantees and safety. For example, a few weeks ago, I prototyped an experimental library in a few hours that added support for compile-time OCaml style parameterized-modules. [4]

Obviously, all of these techniques don't get you quite as far as proper static typing would (though the Whatsapp team is working on static types for Erlang! [5]), but the rest of the language and the ecosystem is just so well thought out, that I've been okay with that!

[0] https://hexdocs.pm/elixir/typespecs.html

[1] https://github.com/jeremyjh/dialyxir

[2] https://github.com/keathley/norm/

[3] https://github.com/witchcrafters/type_class

[4] https://github.com/QuinnWilton/daat/

[5] https://www.facebook.com/careers/jobs/229713254864749/

Erlang's type checker Dialyzer has an Elixir wrapper called Dialyxir (https://github.com/jeremyjh/dialyxir). As someone coming from C++, Dialyzer leaves a lot to be desired—I still miss C++ type checking—but it's better than nothing.

The Norm library (https://github.com/keathley/norm) is an attempt at higher-level, more expressive type checking which I think shows a lot of promise, but I've not adopted it in a real project yet.

Have you looked at Dialyxir? [1] It makes Elixir feel like a structurally typed language. I use it at work, and it catches a lot of inconsistencies at runtime.

[1]: https://github.com/jeremyjh/dialyxir

I wrote a tool[0] that converts Erlang style Dialyzer messages to enough of Elixir to where the Elixir formatter can pretty print it. This isn't an intractable problem, but the source tool does really bizarre things so the output so it wound up being really annoying to deal with the quirks. Still not quite done, but it's in a workable state to where messages can be dealt with individually when the errors are poor.

[0] https://github.com/asummers/erlex [1] https://github.com/jeremyjh/dialyxir

> Elixir is overall a syntax that works well for me, at least as well as Rust’s. The Elixir team have made great strides in providing good compiler error messages, and are actively improving the distribution/ packaging story. Hex and mix are fantastic, and on par with what I’ve use in cargo.

I'm working on making the dialyzer error messages better, too, in Dialyxir[0] and Erlex[1] =).

[0] https://github.com/jeremyjh/dialyxir [1] https://github.com/asummers/erlex

Not nearly as difficult, but I recently did a large project on converting Erlang Dialyzer output into Elixir friendly output in the Dialyxir[0] project, which involved a lot of lexing and parsing and pretty printing, though I was fortunately able to take advantage of the Elixir code formatter for a lot of the heavy lifting for output. My grammar rules, while better than they've been, are still pretty bad, but they seem to work well enough in practice for most programs that I've seen.

The tl;dr for that project is that it runs dialyzer, finds the relevant Warning module for each warning, which will pretty print parts of the error output into a larger explanation, which involves taking the output, lexing it, parsing it, then pretty printing the IR back into Elixir, then running through the formatter.

[0] https://github.com/jeremyjh/dialyxir

You're right. I've used it once as a part of an exercise in the "Programming Elixir" book and never again.

It should maybe come bundled with mix, as some other tools, that way it'll be more approachable.

Also there's a wrapper for it, which helps in the process.[0]

[0] - https://github.com/jeremyjh/dialyxir

Agreed on the typing, however.

Have you guys looked into Dialyzer?

Dialyzer is a static analysis tool for Erlang and other languages that compile to BEAM bytecode for the Erlang VM. It can analyze the BEAM files and provide warnings about problems in your code including type mismatches and other issues that are commonly detected by static language compilers. The analysis can be improved by inclusion of type hints (called specs) but it can be useful even without those. For more information I highly recommend the Success Typings paper that describes the theory behind the tool.

That's from the Dialyxir (for using Dialyzer w/Elixir) github page: https://github.com/jeremyjh/dialyxir

More: http://learnyousomeerlang.com/dialyzer

(Perhaps this should be read first: http://learnyousomeerlang.com/types-or-lack-thereof )

And this is the Success Types paper behind it (mentioned in the excerpt above):

https://www.it.uu.se/research/group/hipe/papers/succ_types.p...