Elixir Type Safety

I’ve been having a small block in continuing my series on Elixir application design. So this week I’ve written about another topic which has been sitting on my Learning Elixir TODO list for some time: type checking. This topic has been on my mind lately because I have been looking at the language PureScript which is similar to Haskell and centered around its type system. I’d like to see how Elixir’s type specs compare.

In this post I’ll go back and run Dialyzer on the Game of Life implementation that I used in my Optmizing Elixir series. I’ll also work with Elixir’s type annotations to make the types in the source more explicit.

Installing Dialyxir

I’ve opted to use Dialyxir to simplify use of Dialyzer in my project. I followed the directions from the README.

$ git clone https://github.com/jeremyjh/dialyxir.git
$ cd dialyxir/
$ mix archive.build
$ mix archive.install
Are you sure you want to install archive dialyxir-0.2.7.ez? [Yn]
* creating /Users/jkain/.mix/archives/dialyxir-0.2.7.ez
$ mix dialyzer.plt
Starting PLT Core Build ... this will take awhile...

Building the PLT took about 5-6 minutes on my system. This step builds the Persistent Lookup Table which contains type information for the standard library. This way Dialyzer doesn’t have to analyze the standard library every time I run it.

Running Dialyzer

Next I went back to my Game of Life source and ran Dialyzer:

$ mix dialyzer
Starting Dialyzer
dialyzer --no_check_plt --plt /Users/jkain/.dialyxir_core_17_1.0.4.plt -Wunmatched_returns -Werror_handling -Wrace_conditions -Wunderspecs /Users/jkain/Documents/Projects/elixir/life/_build/dev/lib/life/ebin
  Proceeding with analysis...
lifebench.ex:58: Function usage/0 only terminates with explicit exception
lifebench_cmp.ex:105: Function usage/0 only terminates with explicit exception
Unknown functions:
  'Elixir.ExProf':analyze/0
  'Elixir.ExProf':start/1
  'Elixir.ExProf':stop/0
  'Elixir.Statistics':mean/1
  eflame:apply/2
  fprof:analyse/1
  fprof:apply/2
  fprof:profile/0
 done in 0m0.84s
done (warnings were emitted)

@jeremyjh wasn’t kidding, Dialyxir really makes this process easy.

Interpreting Dialyzer Results

The next step is to read over the Dialyzer output and understand what it means. I’ll start with

lifebench.ex:58: Function usage/0 only terminates with explicit exception

My function doesn’t terminate? Oh, right it doesn’t really:

defp usage do
  Kernel.exit("Usage: mix lifebench <results file>")
end

This usage function is part of the lifebench mix task. My next thought was “how does dialyzer know?” and the answer must be in the type of Kernel.exit/1. Looking up the documentation for Kernel.exit/1 I found in its specs:

exit(term) :: no_return

So I add something similar to lifebench.usage/0 like this:

@spec usage :: no_return
defp usage do
  Kernel.exit("Usage: mix lifebench <results file>")
end

and with this change Dialyzer is happy with Lifebench.usage/0.

By the way, after making the change I have to recompile and then run dialyzer. I can do this in one mix invocation like this:

$ mix do compile, dialyzer

Now, LifebenchCmp.usage/0 still has the same problem:

lifebench_cmp.ex:105: Function usage/0 only terminates with explicit exception

and the same solution works here too.

@spec usage :: no_return
defp usage do
  Kernel.exit("Usage: mix lifebench.cmp <results file 1> <results file 2>")
end

External Modules

The remaining errors

Unknown functions:
  'Elixir.ExProf':analyze/0
  'Elixir.ExProf':start/1
  'Elixir.ExProf':stop/0
  'Elixir.Statistics':mean/1
  eflame:apply/2
  fprof:analyse/1
  fprof:apply/2
  fprof:profile/0
 done in 0m0.80s

Come from external modules. I certainly don’t want to see these warnings all the time so I should either include these in the analysis or supress them.

I had limited success adding modules for dialyzer in mix.exs

def project do
  [app: :life,
   version: "0.0.1",
   elixir: "~> 1.0.0",
   deps: deps,
   dialyzer: [
    paths: [
      "_build/dev/lib/eflame/ebin",
      # "_build/dev/lib/exprintf/ebin/"  # too many warnings in exprintf
      "_build/dev/lib/exprof/ebin/",
      "_build/dev/lib/life/ebin",
      "_build/dev/lib/statistics/ebin",
    ]
   ]
  ]
end

This reduces the Dialyzer errors down to:

dialyzer --no_check_plt --plt /Users/jkain/.dialyxir_core_17_1.0.4.plt -Wunmatched_returns -Werror_handling -Wrace_conditions -Wunderspecs _build/dev/lib/eflame/ebin _build/dev/lib/exprof/ebin/ _build/dev/lib/life/ebin _build/dev/lib/statistics/ebin
  Compiling some key modules to native code... done in 0m16.04s
  Proceeding with analysis...
Unknown functions:
  'Elixir.ExPrintf':printf/2
  eprof:analyze/2
  eprof:log/1
  eprof:start/0
  eprof:start_profiling/1
  eprof:stop_profiling/0
  fprof:analyse/1
  fprof:apply/2
  fprof:profile/0
 done in 0m0.83s
done (passed successfully)

eprof and fprof are part of the erlang standard library so I would have expected them in my PLT but they were not included. ExPrintf has too many warnings of its own so I left it out.

Next Steps

The next step for me would be to go back into the Game of Life source and start adding type specs to make sure I really understand the funcitons I have. As I go I would have dialyzer at my side to make sure I’m building something type-consistent.

I think I will continue with this in next week’s post.

Joseph Kain