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