How to make Dialyzer more strict?

Sorry, I should have reread the typespec docs before posting. In that case, I think some typespecs should be updated to use this

Not that it would make much difference in practice.

I love types, but here

Jose says the future might be Clojure Spec

https://clojure.org/about/spec

which seems sensible to me.

Yet again, Elixir and Clojure show their likeness…

1 Like

Did you try the overspecs/underspecs flags? http://erlang.org/doc/man/dialyzer.html

Dialyzer is fine for the trade-offs it chose to make. Having something more strict most likely means rejecting code that is completely valid today. Or in the best case scenario, forcing types to be explicit and not relying on inference.

@tmbb is correct here. There aren’t low hanging fruits when it comes to types. Adding a type system involves many compromises and the compromises you are willing to make change a lot when the language already exists.

If you want to have type inference, then many Elixir idioms will no longer be supported. Elixir code is based on unions (it returns {:ok, _} | :error) and intersections (different clauses of a function) and those are very expensive for an inference engine.

We could add requirements, such as obligatory typing of inputs, but that doesn’t solve the problem that we have both typed and non-typed code and we should likely check the values at the boundaries, adding runtime cost.

If you want to keep the language the same and support all of the existing idioms and also not worry about conversion costs: that’s Dialyzer.

Long story short: we could have other type systems but you need to start from scratch and you will have to compromise in many ways.

Apologies but I did not mean that Clojure Spec is the future. It is unlikely we will have something like Clojure Spec in Elixir per-se, especially because we have typespecs and guards and adding a third option is going to bring only marginal gains. If somebody wants to explore something like Clojure Spec as a package, then please do!

7 Likes

Would it be possible through a module attribute or macro to have the compiler insert additional pattern matching / guard clauses to check parameters and return values respect the typespecs at runtime?

Something like a combination of dialyzer and expat would be great.

Yes, I tried, it seems :underspecs not affect at all to my example

Dialyzer with flag :overspecs generated weird warning not related to problem in example

lib/hello.ex:1: Type specification 'Elixir.Hello':'__info__'('attributes' | 'compile' | 'functions' | 'macros' | 'md5' | 'module' | 'deprecated') -> atom() | [{atom(),any()} | {atom(),byte(),integer()}] is a subtype of the success typing: 'Elixir.Hello':'__info__'('attributes' | 'compile' | 'deprecated' | 'functions' | 'macros' | 'md5' | 'module') -> any()
done (warnings were emitted)

I also tried other flags, it not resolves the problem

I had a similar question in this post and got a nice answer from @peerreynders.

You could do

  @type good_hello() :: map() 
  @type bad_hello() :: map() 

  @spec hello(integer()) :: good_hello() | bad_hello()
  def hello(int) do
    case int do
      1 -> good()
      _ -> bad()
    end
  end

  @spec good() :: good_hello()
  def good(), do: %{hello: "world"}

  @spec bad() :: bad_hello()
  def bad(), do: :wtf

This way You would catch spec error with dialyzer.

5 Likes

Thanks, so short answer is to not use literals for structures, maps, lists and other terms, but use functional wrapper with its own typespec which will return term as expression without any branching inside?

1 Like

I was trying to port example from [Functional Programming] Domain Modeling Made Functional (Pragprog) (F#) to Elixir. Of course F# is not Elixir, but the example remains interesting.

Thanks, so short answer is to not use literals for structures, maps, lists and other terms, but use functional wrapper with its own typespec which will return term as expression without any branching inside?

Yes, and then compose into bigger types, and bigger functions. Maybe like this.

  @type good_hello() :: map() 
  @type bad_hello() :: map() 
  @type any_hello() :: good_hello() | bad_hello()

  @spec hello(integer()) :: any_hello()

Yes, probably it will work, but I think it looks creepy :smiley:
And of course if you will introduce new type and function every time you need branching - it will gain 3x amount of code, and will gain overhead regarding function calls in runtime

Personnally, I would have written this like that :slight_smile:

  @spec hello(integer()) :: map()
  def hello(1), do: %{hello: "world"}
  def hello(_), do: :wtf

Conditional and branching are easily replaced by pattern matching :slight_smile:

Yes, ofc I like pattern matching - it makes code shorter etc,
but it not resolves problem with typespecs and Dialyzer here - try to compile it and run checks, Dialyzer will be happy with it

Actually it does. :slight_smile:

@type my_dict(key, value) :: [{key, value}]

I’d think you could?

@spec delete([t], t) :: [t]

Although I’m unsure how well dialyzer checks that (wow the syntax highlighting is bad on ::)? But I’m like 80% sure Dialyzer matches based on unbound names for handling passed in types.

Good thing the AST is so simple, just some primitive types, lists, 2-tuples, and 3-tuples. :slight_smile:
/me wishes it were just 3-tuples and primitives-inside-special-3-tuples

There are ways though, and since each form of an AST node is distinct then it could be a headless sum type safely (or heads without internal named distinction, which is easy to do). :slight_smile:

Ah yeah, the when might be necessary, unsure?

I don’t. It is runtime based, not entirely compile-time, which is point defeating.

Yep yep, it is a great positive typer, it was not designed to be an actual complete typing system.

It’s not too bad actually, especially if there is a ‘dynamic’ type that must be matched out for use in statically-strongly typed sections (deft as a typed def, or something that is module-wide?), then you can pretty well incrementally improve it knowing that the only unchecked areas are areas that are not typed. :slight_smile:

At least until you define such an Option.t type or so and baked in a few common patterns.

Not any more than current code already has to do, the dynamic->typed boundaries would still use matchers and guards to safely determine what it is, which is what you have to do anyway to determine the types of something. However inside the typed area then direct calls could be made that entirely bypass guards and other such checks for known paths.

Yeah I really wish Elixir started as a typed language, erlang being dynamically typed is one of the things I’ve hated most about it, only standing it because of dializer. Elixir started from the wrong side of typing even though it was made a-new still seemed entirely broken to me…

Actually I think it was @vic that made a library or two along that path. ^.^

Yep, it definitely would, though that would add overhead that the static type checking means wouldn’t need to exist anyway (proper static typing can remove a lot of checks and can generate a lot better code in a few areas).

Yeah overspecs are way too noisy because the quality of the specs in the overall engine and essentially all libraries are not made quite right in a lot of places (especially once you take macro’s in mind).

Like in a real full typing system! ^.^

Typespecs don’t generate code though.

/me really wants to work more on the TypedElixir experiment… blehg lack of time…

1 Like

Yes, but in an HM typesystem you need named constructors to write your macro, even if the internal implementation strips them… This is not a disaster, though, and you can work around it.

1 Like

I don’t think it is too creepy, one liner functions, more specs and types than code, and…

… no local variables :slight_smile:

  @type good_hello() :: map() 
  @type bad_hello() :: map() 
  @type any_hello() :: good_hello() | bad_hello()

  @spec hello(integer()) :: any_hello()
  def hello(1), do: good()
  def hello(_), do: bad()

  @spec good() :: good_hello()
  def good(), do: %{hello: "world"}

  @spec bad() :: bad_hello()
  def bad(), do: :wtf
2 Likes

That’s true for basic types but pretty much a nightmare for everything else. I can easily assert that something is a list. It is expensive to assert that something is a list of only As and Bs. Other times it is just plain impossible (guarantee that X is a stream capable of emitting only Y). Or assert module Z coming from runtime implements a certain behaviour or protocol.

1 Like

That would be assuming recursiveness, rather it should be dynamic fully internally, so a list would only contain a list of dynamics, each of those you’d test out (would would be very simple if they only expect one thing). Typing to a full resolved type is one of those things I keep saying is not efficient or good to do on dynamic/typed interaction boundaries. ALL integration points should be entirely dynamic typed, thus in OCaml’ize something like:

let sum_ints bb =
  let open BeamTypes in
  match bb with
  | List lst ->
    lst |> List.fold_left 0 (fun acc v-> match v with
      | Integer i -> i+acc
      (* See below *)
    )
  (* Passing in an unhandled type will crash at runtime in OCaml so I will leave it,
     though you also get a compile warning...
  *)

Thus Every-Single-Dynamic-Location has to be matched out only to the BeamTypes types, so a BeamTypes.List gets you a list of more beamtypes. This is really the only safe way to do it on something like the BEAM VM. You can of course make some kind of macro (or in OCaml terms, a PPX) that generates conversion and check functions if you don’t mind the runtime checking cost, but it’s not any more expensive then checking them in the BEAM as well, and if you just handle a single type each, like in the above example, then the codegen can just treat it like it straight anyway without any checks if it shows the usage confirms the type that it will be (I.E. that it would crash if invalid type). Or the user could define a default case and handle the errors any way they want (which would always put in a guard test at codegen).

Only atomically built units of modules could be fully properly typed. Message boundaries and so forth absolutely could not be. And manually hot-code loading non-atomic module-sections is of course ‘undefined behaviour’ (but a rare case even nowadays). ^.^

1 Like

Right, that would require the type-safe code to do conversions and inline code until the traversal point, which violates the modules boundaries. Or am I missing something? To me violating the module semantics is a no-no.

Rather on bounds that are designed to be called by untyped code or is calling out to (and getting back) untyped values then they’d need to be matched on by the author of the code, this requires the author to do it with whatever efficiency they deem best for that location. If untyped code calls typed code with a value that does not match the typespec then it is of course undefined behaviour (crash whenever it gets used in an unexpected way). :slight_smile:

I.E. you only get the type safety when calling from typed to typed code, otherwise it’s essentially the same as normal elixir/erlang calling normal elixir/erlang. It enhances usage, but does not require it (since the beam doesn’t enforce it anyway, meaning don’t try to hide it like alpaca is doing, instead embrace it).

Sure, you could do that, but it is also a trade-off you have to make and some people will be genuinely surprised by not type checking at the boundaries.

2 Likes

Could always be configurable as well. Perhaps a unique internal call that does not test types if not necessary, and a public interface that does test them (thus incurring the cost only when necessary) that way you have both (though it duplicates the public function count in modules that are marked as such). :slight_smile: