Collapsing/compressing redundant typespecs?

Questions & Help Questions
1

I’m writing a multiset library. It’s got 2 modules: one which works on raw “multisets” (which are maps of elements to quantities), and another which is just a Struct type wrapping the same functionality in much nicer ergonomics.

For the former module, all the methods support so-called “lax” multisets, where some element => 0 records may be included; but many methods include a strict \\ :lax :: :lax | :strict parameter that can be used to switch on better codepaths whenever the caller can guarantee the multiset isn’t “lax”.

I’m trying to write the type system to support that, so that Dialyzer will be helpful to any consumers. However, the type signature for one method, delete, has turned out suspiciously verbose; I’m wondering if there’s any way to shore this up with some syntax that more clearly semantically indicates “this type in the output is the same as this type in the input, and said type must in any case fit some constraint, and you should try fitting the allowed types in this particular priority order”, without this combinatorial explosion:

@type t(value) :: %{optional(value) => pos_integer()}
@type t() :: t(term)

@type t_lax(value) :: %{optional(value) => non_neg_integer()}
@type t_lax() :: t_lax(term)

@type t0(value) :: Enumerable.t({value, non_neg_integer()})
@type t0() :: t0(term)

# …

@spec delete(t(e), term) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term) :: t_lax(e) when e: term
@spec delete(t(e), term, :all) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term, :all) :: t_lax(e) when e: term
@spec delete(t(e), term, non_neg_integer()) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term, non_neg_integer()) :: t_lax(e) when e: term
def delete(ms, element, count)

def delete(ms, element, :all), do: Map.delete(ms, element)

def delete(ms, element, count) when is_pos_integer(count) do
  case ms do
    %{^element => n1} ->
      n2 = n1 - count

      if n2 > 0 do
        %{ms | element => n2}
      else
        Map.delete(ms, element)
      end

    %{} ->
      ms
  end
end

def delete(ms, _, 0), do: ms
2

@spec delete(mset, term) :: mset when mset: t(term) | t_lax(term)

The specs you wrote would be merged to the following anyways:

@spec delete(t(e) | t_lax(e), term) :: t(e) | t_lax(e) when e: term

3

The specs I wrote, I believe, allow Dialyzer to prove that the return value is t whenever it can prove that the parameter is t, don’t they? That’s what I was attempting to do.

4

No. Multiple specs for a single function(/arity) will be merged where all the individual parameters and the return type are put into union. Only if you do the @spec fun(x) :: x when x: term notation do you “hint” – not sure how hard a hint – that input and output are of the same type

5

Would it be possible to do something similar for this function, which has even more entanglement between its types?

# guaranteed non-lax return when input is non-lax
@spec put(t(e1), e2, non_neg_integer) :: t(e1 | e2) when e1: term, e2: term
# when input is lax, return may be lax
@spec put(t_lax(e1), e2, non_neg_integer) :: t_lax(e1 | e2) when e1: term, e2: term

And is there any more comprehensive reference for how all this works? The hexdocs page on typespecs seems to barely scratch the surface…

6

That seems very strange. The documentation currently suggests that they can be “overloaded” without any particular caveats, and gives this as an example:

@spec function(integer) :: atom
@spec function(atom) :: integer

Are you saying that if this were done, and a developer were to call function/1 with an atom() argument, Dialyzer would still suggest that the return type might be atom()?

7

The hexdocs page describes the typespec syntax, not dialyzer – the type checker using the specs. These are really separate things. But I’m not aware of a comprehensive suite of docs around how dialyzer works. I essentially treat is as best effort checking, because really that’s what it does. E.g. it will switch out granular types, when getting bigger in complexity, for less granular types when checking. In the end the only guarantee dialyzer makes is that there is an issue (even if just with the typespecs) if it reports an issue. Exhaustiveness in finding issues was never a goal of dialyzer.

As for your example I don’t think there is a better way to write this given the distinct type parameters used between input and return value.

8

FWIW, distinguishing situations like:

@spec function(integer) :: atom
@spec function(atom) :: integer

and:

@spec function(integer) :: integer
@spec function(atom) :: atom

(both of which Dialyzer collapses to @spec function(integer | atom) :: integer | atom) is a key motivation for the set-theoretic type work: