I started by adding an @spec to the function count_live_neighbors/3 as it seemed straighforward:
I didn’t get the spec right but Dialyzer’s error message was helpful:
I rewrote the spec as:
Thinking about this more, I could have also looked up the return type of Enum.sum:
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:
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
and put it to use in module Life
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:
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
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:
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:
Digging into Dialyzer broken contracts
The most difficult specs to write revolved aroun my Board constructors:
Adding the type specs to new_from_file and new_from_string worked but insert broke the contracts.
The first thought I had is that this error
was caused by
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:
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
no type spec
Dialyzer runs clean
@spec insert(any, any, any, any) :: map
@spec insert(t, any, any, any) :: t
@spec insert(t, Integer, any, any) :: t
@spec insert(t, non_neg_integer(), any, any) :: t
@spec insert(t, integer(), integer(), string()) :: t
Where “supertype warning” means something like this:
and “Broken contract!” means:
Futhermore, if I use the following typespec then Dialyzer runs clean:
But it seems wrong to me. I prefer
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
to decide that the type should be non_neg_integer() instead of integer(). If I, for example, change the code to
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.TypeSpecsInteger is
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:
Kernel +value has type
That is, addition only works on number() and not Integer. Integer includes integer ranges and addition doesn’t support ranges.
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.