prook

prook

Confused about spec/dialyxir: "Invalid type specification for function"

Hi,

I’m trying to get hang of specs, but I’ve hit a wall. I’m writing a thin facade over Nerves’ SystemRegistry, basically stuff like:

defmodule ConfigRegistry do
  @spec update(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  def update(scope, value) do
    SystemRegistry.update([:config | scope], value)
  end
end

Running mix dialyzer on that results in

lib/config_registry.ex:2:invalid_contract
Invalid type specification for function.

Function:
ConfigRegistry.update/2

Success typing:
@spec update([any()], _) :: %SystemRegistry.Transaction{
  :delete_nodes => MapSet.t(_),
  :deletes => MapSet.t(_),
  :key => _,
  :opts => Keyword.t(),
  :pid => pid(),
  :update_nodes => MapSet.t(_),
  :updates => map()
}

A quick look at

tells me there are two updates, one that can be used standalone (this is the one I’m interested in), and the other one for use with an open transaction.

The functions are specced like this:

@spec update(one, scope, value :: any) :: Transaction.t() when one: Transaction.t()
@spec update(one, value :: any, opts :: Keyword.t()) ::
          {:ok, {new :: map, old :: map}} | {:error, term}
        when one: scope

I can sort of understand dialyxir’s complaint, if I make an assumtion that it cannot recognize [:config | scope] as something that is not a SystemRegistry.Transaction.t(). But that assumption seems very wrong.

So… Either (and most likely) I’m missing some crucial and basic knowledge of spec, there is an error in SystemRegistry.update spec, or a bug in Dialixyr.

How can I persuade Dialyxir my code will always call the standalone update function?

Marked As Solved

prook

prook

(8 hours ago: Hmmm, I should probably do that…)

This has gotten interesting. First, I’ve reduced the warning-inducing code to this:

defmodule WhatTheSpec do
  @type key :: atom()
  @type transaction :: map()

  def put(_, _, _ \\ nil)

  @spec put(one, key(), any()) :: transaction() when one: transaction()
  def put(t, _, _) when is_map(t), do: t

  @spec put(one, any(), Keyword.t()) :: :ok when one: key()
  def put(_, _, _), do: :ok

  @spec put_foo(any()) :: :ok
  def put_foo(value) do
    put(:foo, value)
  end
end

Next, I realized that Keyword.t() does not include nil, yet the third parameter may be nil indeed. So the spec

@spec put(one, any(), Keyword.t()) :: :ok when one: key()

should actually be

@spec put(one, any(), Keyword.t() | nil) :: :ok when one: key()

And sure enough, Dialyxir goes green! So it was lack of understanding on my part after all! Also, this means there’s a similar problem in SystemRegistry @spec of update/3, which sent me on this trip! And furthermore, I point my finger at Dialyxir as well! *gasp!*

Dialyxir’s warning is misleading to say the least:

lib/spec.ex:13:invalid_contract
Invalid type specification for function.

Function:
WhatTheSpec.put_foo/1

Success typing:
@spec put_foo(_) :: map()

As I grok it, @spec put_foo(_) :: map() is not a success typing, as there is actually none. I reason this is a bug, as the complaint about map() being a return type goes away after the | nil fix. It should either stay there (no, it should not!), or never appear at all, right?

Also, changing update_foo from the original example (i. e., before the | nil fix) to

  @spec put_foo(any()) :: :ok
  def put_foo(value) do
    put(:foo, value, nil) # note the explicit nil here
  end

makes Dialyxir barf completely:

Please file a bug in Issues · jeremyjh/dialyxir · GitHub with this message.

Failed to format warning:
@spec a(:one, any(), Keyword.t()) :: 'ok’whenone :: key()\ndef a() do\n :ok\nend\n”

Legacy warning:
lib/spec.ex:7: The contract ‘Elixir.WhatTheSpec’:put(one,key(),any()) → transaction() when one :: transaction();(one,any(),‘Elixir.Keyword’:t()) → ‘ok’ when one :: key() cannot be right because the inferred return for put(‘foo’,_value@1::any(),‘nil’) on line 15 is ‘ok’ | map()


lib/spec.ex:14:no_return
Function put_foo/1 has no local return.


@jeremyjh, It seems I’ve hit some murky parts of Dialyxir with this. :slight_smile:

Also Liked

peerreynders

peerreynders

This is where your mental model breaks down: there is only and there can only be one update/3 function. That function may be implemented in terms of multiple function clauses - but they all belong to the same function.

The Erlang style of specs make that much clearer:

-spec foo(pos_integer()) -> pos_integer()
         ; (integer()) -> integer().

So strictly speaking the return type of SystemRegistry.update/3 is the sum type Transaction.t() | {:ok, {new :: map, old :: map}} | {:error, term}.

A more type-aware module API would have

  • SystemRegistry.update_with_scope/3
  • SystemRegistry.update_with_transaction/3
  • And a convenience function SystemRegistry.update/3 that delegates appropriately.

but given that Erlang/Elixir is dynamically typed you will run into functions that have only been typed after the fact rather than being designed with types in mind.

peerreynders

peerreynders

Tried this approach?

  def update(scope, value) do
    case SystemRegistry.update([:config | scope], value) do
      %SystemRegistry.Transaction{} ->
        {:error, :undefined} # i.e. this will never happen
      result ->
        result
    end
  end

or even more explicitly, intention revealing

  @spec update(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  def update(scope, value),
    do: update_with_scope(scope, value)

  @spec update_with_scope(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  defp update_with_scope(scope, value) do
    case SystemRegistry.update([:config | scope], value) do
      %SystemRegistry.Transaction{} ->
        {:error, :undefined} # i.e. this will never happen
      result ->
        result
    end
  end
jeremyjh

jeremyjh

Everything is worth fixing, and I’ve found the Erlang group to be very responsive and helpful on past Dialyzer bugs. My only hesitation again is that its possible the when spec doesn’t really intend to behave like we think it would. I’d probably post it on erlang-bugs before opening a Jira, but either way would be fine.

Where Next?

Popular in Questions Top

pmjoe
I have a relationship of love and hate with Elixir. Lots of things are just absolutely right, but there are some things that are kind of ...
New
pgiesin
This should be a simple problem but I just can’t seem to figure it out. I have a standalone Elixir app that won’t find the database. Dep...
New
sacepums
Hey guys. I'm new to elixir and im really stocked about it. But I ran into a bit of problem - I need to convert a date sting, for examp...
New
makeitrein
Hey all, just started picking up Elixir last week and am writing a scraper as a learning project. Baby step #1 is extracting the number ...
New
alice
Hey, Just curious what are the main benefits of Elixir compared to Clojure? When is Elixir more useful than Clojure and vice versa? Th...
New
gonzofish
I’m currently trying to understand how to join three tables using Ecto. All the examples I’ve seen use 2, so maybe I’m just missing somet...
New
vonH
When I run the Plug and I recompile I wind up having to use Ctrl C to quit iex and start again. Witht the help of rlwrap I can use the cu...
New
hpopp
To simplify some tasks at work, I wrote and published this package yesterday. It’s a simple macro that enables Access behaviour on struct...
New
Mooodi
Given a string, how can I get access to its character by index? Enum.at("my_string", 2) doesn't work. Or rather, not char, but a substr...
New
lanycrost
Hi everyone! I need implement if…else if…else condition from my elixir code, and anymore of this control flow structures not work proper...
New

Other popular topics Top

yurko
Here are few pieces of (common) Linux knowledge that we use for reasonably small one server apps. We use Ubuntu but this should work for ...
New
aalberti333
As the title describes, I’m trying to run Enum.map() over a list of key/value pairs, where the value is a map. My data looks like this: ...
New
script
If I have a string “1000 cfu/ml” . I want to remove the characters and / and space . So the string is like this "1000" What is the ...
New
chrismccord
As promised, the first release candidate of Phoenix 1.3.0 is out! This release focuses on code generators with improved project structure...
New
rms.mrcs
Hi, I need to transform a list of numbers into a map where the keys are the indexes and the values are the original values of the list....
New
alice
Hey, Just curious what are the main benefits of Elixir compared to Clojure? When is Elixir more useful than Clojure and vice versa? Th...
New
vonH
When I run the Plug and I recompile I wind up having to use Ctrl C to quit iex and start again. Witht the help of rlwrap I can use the cu...
New
stefanluptak
Hello everybody, usually, I use a 29" ultra-wide monitor for VSCode which can easily accomodate explorer (files panel) + file with code ...
New
lucidguppy
I have a super simple question about elixir - how would I take a file like this foo bar baz and output a new file that enumerates th...
New
romenigld
I am trying to run a deploy with docker and I successfully runned with this command: docker build -t romenigld/blog-prod . but when I t...
New

We're in Beta

About us Mission Statement