James_E
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
Where Next?
Trending in Questions
Other Trending Topics
Latest on Elixir Forum
Sponsor Spotlight
Supporting innovation across the BEAM ecosystem.
Categories:
Sub Categories:
Forums
Popular Tags
- #ecto
- #liveview
- #troubleshooting
- #learning-elixir
- #deployment
- #library
- #erlang
- #testing
- #genserver
- #mix
- #absinthe
- #remote-other
- #otp
- #plug
- #how-to-question
- #macros
- #postgres
- #elixirconf
- #channels
- #exunit
- #discussion
- #code-sync
- #javascript
- #podcasts
- #onsite
- #dialyzer
- #docker
- #authentication
- #umbrella
- #full-time-contract
- #podcasts-by-brainlid
- #ecto-query
- #blog-post
- #elixir-ls
- #ai
- #elixirconf-us
- #phoenix_html
- #iex
- #graphql
- #genstage
- #websockets
- #supervisor
- #advent-of-code
- #distillery
- #processes
- #api
- #forms
- #hex
- #security
- #metaprogramming
Our Sponsors
Build Elixir applications with speed and confidence.
Supporting innovation across the BEAM ecosystem.
We build reliable cloud platforms for business-critical systems.
Catch errors, track performance, monitor hosts and more.
Error tracking, logs, uptime, and Just Enough APM. Built for developers.
Master modern tools, write cleaner code, and tackle real-world challenges.
Bringing learning, work and compliance together since 1987.
Enabling companies to succeed by building software people love.
The team behind Membrane, Popcorn, LiveDebugger. Available for hire.
Courses that'll move you from confusion to "Aha, now I get it!"
Showing Posts 1 to 7- Show Best Posts
- Show All (oldest first)
- Show All (newest first)
LostKobrakai
@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: termJames_E
The specs I wrote, I believe, allow Dialyzer to prove that the return value is
twhenever it can prove that the parameter ist, don’t they? That’s what I was attempting to do.LostKobrakai
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: termnotation do you “hint” – not sure how hard a hint – that input and output are of the same typeJames_E
Would it be possible to do something similar for this function, which has even more entanglement between its types?
And is there any more comprehensive reference for how all this works? The hexdocs page on typespecs seems to barely scratch the surface…
James_E
That seems very strange. The documentation currently suggests that they can be “overloaded” without any particular caveats, and gives this as an example:
Are you saying that if this were done, and a developer were to call
function/1with anatom()argument, Dialyzer would still suggest that the return type might beatom()?LostKobrakai
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.
al2o3cr
FWIW, distinguishing situations like:
and:
(both of which Dialyzer collapses to
@spec function(integer | atom) :: integer | atom) is a key motivation for the set-theoretic type work: