Elixir Type Specs

Last week I wrote a post about setting up Dialyxir and analyzing type safety in Elixir. This week I continue the effort and add type specs to an existing Elixi source base - my Game of Life in Elixr.

Elixir @spec

I started by adding an @spec to the function count_live_neighbors/3 as it seemed straighforward:

@spec count_live_neighbors(Integer, Integer, any) :: Integer
defp count_live_neighbors(x, y, board) do
  list_of_neighbors(x, y, board)
  |> Enum.map(&state_as_int/1)
  |> Enum.sum
end

I didn’t get the spec right but Dialyzer’s error message was helpful:

life.ex:45: Invalid type specification for function 'Elixir.Life':count_live_neighbors/3. The success typing is (_,_,_) -> number()

I rewrote the spec as:

@spec count_live_neighbors(Integer, Integer, any) :: number

Thinking about this more, I could have also looked up the return type of Enum.sum:

@spec sum(t) :: number
sum(collection)

But, what if I wanted the result to be Integer? The number of live neighbors is an integer whereas number represents integer or float (see http://elixir-lang.org/docs/v1.0/elixir/Kernel.Typespec.html). How can I coerce the result after Sum? The best I’ve been able to do is:

@spec count_live_neighbors(Integer, Integer, any) :: integer()
defp count_live_neighbors(x, y, board) do
  list_of_neighbors(x, y, board)
  |> Enum.map(&state_as_int/1)
  |> Enum.sum
  |> round
end

A type for my board

Next I wanted to create a type for the game Board which should be defined in module Board. I started with

@type board :: map

and put it to use in module Life

@spec board_to_string(Board.board) :: String.t
def board_to_string(board), do: Board.to_string(board)

But later while reading over core Elixir types I realized that a more idiomatic name for the board type would be Board.t which is defined like this:

defmodule Life.Board do
  @type t :: map
  # ...
end

and then refered to as just t within the Board module and as Board.t outside. For a while I experimented with refering the the type as Board.t inside the module. This seems a little clearer to me but doesn’t match the patter used in the Elixir standard library. But, be aware that some of the error messages from Dizalyer may show Board.t.

In Elixr, for module Foo the main type for Foo should be named Foo.t

Next I looked at the function Board.apply_rules/3

Builtin types

defp apply_rules({x, y}, value, board) do
  case {value, count_live_neighbors(x, y, board)} do
    {v, c} when (v == @live) and (c < 2)            -> @dead
    {v, c} when (v == @live) and (c == 2 or c == 3) -> @live
    {v, c} when (v == @live) and (c > 3)            -> @dead
    {v, c} when (v == @dead) and (c == 3)           -> @live
    {v, _}                                          -> v
  end
end

I’m was not sure what the type of value should be. It is supposed to be a printable character. So, is it Integer? I was hoping to enter sometihng invalid and have Dialyzer tell me the success typing. But it seems to accept anything here. I tried:

@spec apply_rules({Integer, Integer}, Integer, Board.board) :: Integer

And it seems to work. But, looking through the documentation for Kernel.Typespec I see there is a buitin type char(). I changed the code to use the following spec:

@spec apply_rules({Integer, Integer}, char(), Board.t) :: Integer

Digging into Dialyzer broken contracts

The most difficult specs to write revolved aroun my Board constructors:

defmodule Life.Board do

  @type board :: map

  @spec new_from_file(Path.t) :: board
  def new_from_file(seedfile) do
    {:ok, seed} = File.read(seedfile)
    new_from_string(seed)
  end

  @spec new_from_string(String.t) :: board
  def new_from_string(string) do
    Map.new |> insert(0, 0, String.to_char_list(string))
  end

  @spec insert(t, Integer, Integer, char_list) :: t
  defp insert(map, _x, _y, []), do: map
  defp insert(map, _x,  y, [10 | list]), do: insert(map, 0, y + 1, list)
  defp insert(map,  x,  y, [char | list]) do
    new_map = Map.put(map, {x, y}, char)
    insert(new_map, x + 1, y, list)
  end

Adding the type specs to new_from_file and new_from_string worked but insert broke the contracts.

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...
board.ex:6: Function new_from_file/1 has no local return
board.ex:12: Function new_from_string/1 has no local return
board.ex:13: The call 'Elixir.Life.Board':insert(#{},0,0,string()) breaks the contract ('Elixir.Board':t(),'Elixir.Integer','Elixir.Integer',elixir:char_list()) -> 'Elixir.Board':t()
board.ex:16: Invalid type specification for function 'Elixir.Life.Board':insert/4. The success typing is (#{},non_neg_integer(),non_neg_integer(),string()) -> #{}
board.ex:18: The call 'Elixir.Life.Board':insert(map@1::#{},0,pos_integer(),list@1::string()) breaks the contract ('Elixir.Board':t(),'Elixir.Integer','Elixir.Integer',elixir:char_list()) -> 'Elixir.Board':t()
board.ex:21: The call 'Elixir.Life.Board':insert(new_map@1::#{},pos_integer(),y@1::non_neg_integer(),list@1::string()) breaks the contract ('Elixir.Board':t(),'Elixir.Integer','Elixir.Integer',elixir:char_list()) -> 'Elixir.Board':t()
cli.ex:6: Function main/0 has no local return
cli.ex:6: Function main/1 has no local return
life.ex:7: Function run_game/2 has no local return
life.ex:7: Function run_game/1 has no local return
life.ex:14: Function seed_board/1 has no local return
life.ex:15: Function do_seed_board/1 has no local return
life.ex:18: Function empty_board/0 has no local return
life.ex:20: Function iterations/1 will never be called
life.ex:21: Function 'animated?'/1 will never be called
life.ex:23: Function run_loop/3 will never be called
life.ex:32: Function tick/1 will never be called
life.ex:33: The created fun has no local return
life.ex:36: Function apply_rules/3 will never be called
life.ex:47: Function count_live_neighbors/3 will never be called
life.ex:54: Function list_of_neighbors/3 will never be called
life.ex:61: Function output/2 will never be called
life.ex:61: Function output/3 will never be called
profile.ex:22: The created fun has no local return
profile.ex:24: Function run_test/0 has no local return
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
Unknown types:
  'Elixir.Board':t/0
 done in 0m0.88s
done (warnings were emitted)

The first thought I had is that this error

board.ex:13: The call 'Elixir.Life.Board':insert(#{},0,0,string()) breaks the contract ('Elixir.Board':t(),'Elixir.Integer','Elixir.Integer',elixir:char_list()) -> 'Elixir.Board':t()

was caused by

@spec new_from_string(String.t) :: Board.t
def new_from_string(string) do
  Map.new |> insert(0, 0, String.to_char_list(string))
end

because Map.new returns a map and I pass that map into insert/4 rather than a Board.t. But I get the same errors even if I rewrite the code as:

@spec new_from_string(String.t) :: t
def new_from_string(string) do
  empty_board |> insert(0, 0, String.to_char_list(string))
end

@spec empty_board :: t
defp empty_board do
  Map.new
end

I’ve read through some of the type specs in the Elixir standard library sources but I wasn’t ab\le to find any examples that helped. I’ve tried other things a bit haphazardly and I wanted to try a more systematic approach. I figured that I should be able to build a very general type spec that I would pass and then make it increasingly more specific until I encountered the error. This would allow me to idenitfy which types are the problem:

`Board.insert/4` Type spec	Result
no type spec	Dialyzer runs clean
`@spec insert(any, any, any, any) :: map`	supertype warning
`@spec insert(t, any, any, any) :: t`	supertype warning
`@spec insert(t, Integer, any, any) :: t`	Broken contract!
`@spec insert(t, non_neg_integer(), any, any) :: t`	supertype warning
`@spec insert(t, integer(), integer(), string()) :: t`	supertype warning

Where “supertype warning” means something like this:

board.ex:22: Type specification 'Elixir.Life.Board':insert(t(),non_neg_integer(),any(),any()) -> t() is a supertype of the success typing: 'Elixir.Life.Board':insert(#{},non_neg_integer(),non_neg_integer(),string()) -> #{}

and “Broken contract!” means:

board.ex:5: The specification for 'Elixir.Life.Board':new_from_file/1 states that the function might also return #{} but the inferred return is none()
board.ex:6: Function new_from_file/1 has no local return
board.ex:11: The specification for 'Elixir.Life.Board':new_from_string/1 states that the function might also return #{} but the inferred return is none()
board.ex:12: Function new_from_string/1 has no local return
board.ex:13: The call 'Elixir.Life.Board':insert(#{},0,0,string()) breaks the contract (t(),'Elixir.Integer',any(),any()) -> t()
board.ex:22: Invalid type specification for function 'Elixir.Life.Board':insert/4. The success typing is (#{},non_neg_integer(),non_neg_integer(),string()) -> #{}
board.ex:24: The call 'Elixir.Life.Board':insert(map@1::#{},0,pos_integer(),list@1::string()) breaks the contract (t(),'Elixir.Integer',any(),any()) -> t()
board.ex:27: The call 'Elixir.Life.Board':insert(new_map@1::#{},pos_integer(),y@1::non_neg_integer(),list@1::string()) breaks the contract (t(),'Elixir.Integer',any(),any()) -> t()

Futhermore, if I use the following typespec then Dialyzer runs clean:

@spec insert(t, non_neg_integer(), non_neg_integer(), char_list) :: t

But it seems wrong to me. I prefer

@spec insert(t, integer(), integer(), string()) :: t

even though Dialyzer issues the supertype warning. The reason for this is that Dialyzer seems to use the values 0, 0 passed in this call

@spec new_from_string(String.t) :: t
def new_from_string(string) do
  Map.new |> insert(0, 0, String.to_char_list(string))
end

to decide that the type should be non_neg_integer() instead of integer(). If I, for example, change the code to

@spec new_from_string(String.t) :: t
def new_from_string(string) do
  Map.new |> insert(-1, -1, String.to_char_list(string))
end

Then the success typing changes. I find this a little bit confusing - it seems a little strange to me that usage impilies typing. To understand this better I read parts of the original Dialyzer paper Success Typing. Section 6.2 “Module system to the rescue” describes that unexported (private) functions do use information from calls to refine the function’s domain. Section 6.3 goes on to describe that data flow analysis also informs the type inference. So in this case the usage does imply non_neg_integer(). But, I will use integer() in Board.insert/4’s type spec as integer() matches my intention for the function.

In Dialyzer, usage affects the typing of private functions.

Another thing that confused me is that integer() is compatible with the success typing for Board.insert/4 but Integer is not. According to Kernel.TypeSpecs Integer is

Integer :: integer
         | ElixirInteger                # ..., -1, 0, 1, ... 42 ...
         | ElixirInteger..ElixirInteger # an integer range

so Integer should be a supertype of integer() as well as non_neg_integer() (by the transitive property of supertypes). For quite some time I didn’t understand the problem here. But eventually I realized that Integer is too wide of a type. The fact that it is a supertype of integer() is the problem. The reason being this head of insert function:

defp insert(map, _x,  y, [10 | list]), do: insert(map, 0, y + 1, list)

Kernel +value has type

+number :: number

That is, addition only works on number() and not Integer. Integer includes integer ranges and addition doesn’t support ranges.

Conclusion

I’ve learned a lot about Elixir type specs while writing this post. I’ve only written six specs but have run into a few intriguing issues with Dialyzer. I think there is still a lot to learn about Dialyzer and more practice to had before I can be successful using it. But, I do belive that the type checking will be worth the effort. Also, I found that adding the type annotations after the fact was tedious - in the future I plan to add them as I write the code.

Joseph Kain