Using Dialyzer in Elixir

Below is the general presentation from the December 2016 Houston Elixir Meetup on strings and binaries.

DialyzerDemo

Typing in Erlang

Erlang (and by Elixir) is a dynamically typed language. As a dynamic language, some type errors cannot by cought until runtime. Some parts of the language inherently make type errors harder to get than other dynamic languages: compilation, pattern matching, guard clauses, and the approach to errors go a long way. However, it does not grant the absolute type safety that you might get from ML-family languages or even languages that are just statically typed.

What is dialyzer?

The Dialyzer, a DIscrepancy AnalYZer for ERlang programs. Dialyzer is a static analysis tool used for checking types and other discrepancies such as dead or unreachable code.

Dialyzer examines .erl or .beam files (not .ex or .exs) – more on this in a minute.

Success typing

Success typing takea a very optomistic treatment of your code. Dialyzer will only emit errors when it can guarantee there is a problem (no false positives). While problematic code can still pass through the analysis, if dialyzer says there is a problem, there definitely is a problem.

As Dialyzer examines your code, it develops constraints on your functions. Dialyzer will assume your functions are being used properly until it can prove that the function will always be wrong.

Example: Boolean and function

The and function in a static language might look something like this:

and :: Bool -> Bool -> Bool
and x y | x == True && y == True = True
        | otherwise = False

In this static language, the compiler would throw and error at you if you used the function with anything other than a boolean value for both arguments.

An Elixir variant may look like this:

defmodule BooleanFuns do
   def and(true, true) do
    true
  end
  
  def and(false, _) do
    false
  end
  
  def and(_, false) do
    false
  end 
end

This code would be too uncertain for a static language to compile, but is A-OK in Elixir. Dialyzer is fine with it, too!

Constraint generation occurs with functions that it knows can only be of a certain type. For example, using the + is enough information for dialyzer to require this function receive only numbers. Guard clauses like is_atom or is_list will also develop more constraints for your functions.

Once the constraints are generated, it is time to solve them, just like a puzzle. The solution to the puzzle is the success typing of the function. Conversely, if no solution is found, the constraints are unsatisfiable and you have a type violation on your hands.

Using dialyzer

Dialyzer comes with current distributions of Erlang. If you have Elixir, you already have dialyzer.

Dialyzer uses a Persistent Lookup Table (PLT) to keep track of all of your constraints. As it analyzes your code, it includes more information onto the table.

The PLT can be built with the following command: dialyzer plt Keep in mind that the PLT takes a while to build, but only needs to be performed once.

Dialyzer can only work on .erl and .beam code, so we have to compile our code in order to use the dialyzer on Elixir code.

Using dialyxir

Remembering to compile each time we want to use dialyzer is a chore. Luckily, the dialyxir library includes handy mix tasks to compile and do other favors for us when we use dialyzer. After including dialyxir as a dependency in mix.exs, pulling the dependency, and building the PLT, you can run dialyzer through mix:

mix dialyzer

Alternatively, you can install dialyxir globally on your machine.

git clone https://github.com/jeremyjh/dialyxir
cd dialyxir
MIX_ENV=prod mix do compile, archive.build, archive.install

I recommend doing this, so you can use it on any project without adding it to the development dependencies.

Tip

Remember, you can always check types in iex with the i function:

iex(2)> i "elixir"
Term
  "elixir"
Data type
  BitString
Byte size
  6
Description
  This is a string: a UTF-8 encoded binary. It's printed surrounded by
  "double quotes" because all UTF-8 encoded codepoints in it are printable.
Raw representation
  <<101, 108, 105, 120, 105, 114>>
Reference modules
  String, :binary
iex(3)> i 'elixir'
Term
  'elixir'
Data type
  List
Description
  This is a list of integers that is printed as a sequence of characters
  delimited by single quotes because all the integers in it represent valid
  ASCII characters. Conventionally, such lists of integers are referred to as
  "charlists" (more precisely, a charlist is a list of Unicode codepoints,
  and ASCII is a subset of Unicode).
Raw representation
  [101, 108, 105, 120, 105, 114]
Reference modules
  List

Using @specs

Dialyzer doesn’t require typespecs to run and catch errors. However, the @specs act as hints for the program and can help it with developing better constraints. The @spec flag will tell dialyzer to include this information in the PLT.

Sources:

Dialyzer documentation

Dialyxir on Hex.pm

Learn You Some Erlang: Fred Hebert

Little Elixir & OTP Guidebook: Benjamin Tan

Success Typing Paper: Tobias Lindahl & Konstantinos Sagonas

Geoff Smith

Software developer with fine arts background

Tweet Share