Help Dialyzer Help You!

…or Why you should use specs if you use opaque types

Following the steps from Devon and Stavros, I wanted to write this article to highlight a not so obvious dialyzer lesson about opaque types and specs…

Help me help you — Jerry Maguire

TL;DR

For the impatient ones…

If you define an opaque type, you have to add specs to all the exported functions that use it (i.e. your module’s API).

Opaque Types

Since this article is about opaque types, I will do a quick intro first…

In Elixir, there are 3 ways to specify a user-defined type:

@type t1 :: boolean | atom # this type is exported
@typep t2 :: String.t # this type is private
@opaque t3 :: t1 | t2 # this type is opaque

The equivalent in Erlang is slightly more verbose…

-type t1 :: boolean() | atom().
-export_type [t1/0]. % This makes t1 exported
-type t2 :: string:t().
-opaque t3 :: t1 | t2.

Private types can only be used within the module that defines them. Exported types can be used anywhere and if you use them outside the module that defines them you have to use their fully qualified names (e.g. String.t, MyMod.my_type, etc.).

Opaque types are just like exported types in the sense that you can use them from outside of the module where you define them. But there is a subtle difference: You are not supposed to use the definition of an opaque type outside its module.

Check, for instance, the docs for HashSet.t(): there is only the name of the type there and that’s intentional. The docs won’t tell you how that type is implemented and that’s because you should treat those things as black-boxes. You’re not supposed to deconstruct or pattern-match a HashSet.t(), you’re supposed to use the functions in the HashSet module to work with it.

For comparison, check the types in the String module. There, all exported types expose their internal structure and that’s intentional again. The idea here is that you are more than allowed to pattern-match on them.

The internal representation of HashSet.t may eventually change and, since you never knew it, your code will still work. String.t, on the other hand, is not expected to ever change and you can benefit from the fact that it’s implemented as a binary() to write your code.

Dialyzer and Opaque Types

Now, opaque types (and types in general) are barely checked by the compiler (only with the right options will it warn you if you are using an unexistent private type, and that’s all). To validate that you’re actually respecting the rules stated above (i.e. not deconstructing instances of opaque types outside of their modules) you need to use Dialyzer.

Dialyzer (through, for instance, dialyxir in Elixir) will check your code and warn you if you ever break the opaqueness of a term. But there is a catch: Dialyzer can’t work alone. You have to help it do its job, as you will see below…

The Setup

My discovery of how to help dialyzer here begun with two very large modules that I have reduced considerably for you. They’re boring now, but they were very large and full of functions originally…

Again… very dumb names. Not the original ones, of course.

Well, I run dialyzer on my project and sure enough, I got these very very clear warnings…

lib/dialyzer_example.ex:19: Function print_odt/1 has no local return
lib/dialyzer_example.ex:19: The call 'Elixir.MyODT':f1(Vodt@1::#{'f2':=_, _=>_}) does not have an opaque term of type 'Elixir.MyODT':t() as 1st argument

WHAAAAT?

What’s going on here?

OK. As it usually happens with dialyzer… I had many questions, but I knew…

Dialyzer is NEVER wrong

So… Let’s see if we can figure this out because, as Sean so brilliantly expressed on his latest talk at CodeBeamSF, it must be just a little misunderstanding between me and dialyzer.

What dialyzer says

So, let’s do the obvious thing first… dialyzer says that my call to MyODT.f1/1 doesn’t have a proper MyODT.t argument. What I am using as an argument to that function is odt, a variable that, according to the spec I wrote for MyODTUser.print_odt is actually an instance of MyODT.t 🤔

Dialyzer also says that MyODTUser.print_odt will never return, but that’s likely because it’s considering the other discrepancy. If I fix that one, I’ll remove both of them at once.

What dialyzer MEANS

If you check Stavros talk (video below) you’ll learn that dialyzer works by inferring the broader possible type for each variable and emitting warnings when it can’t infer any possible type for one.

With that in mind, and since it’s complaining about odt, let’s try to figure out what dialyzer has inferred as its success type.

Actually, we don’t have to go too far for that. It’s in the warning itself: Vodt@1::#{'f2':=_,_=>_}. As you might have noticed Vodt@1 is just the Erlang representation for the variable odt and #{'f2':=_,_=>_}is its type.

That map is somewhat similar to our opaque type MyODT.t, but not quite… since it allows maps to have any keys and values, as long as they have a field called f2 and MyODT.t only allows f1 and f2 as keys (and both of them are required).

How could dialyzer found such a type for odt then? Well… let’s try to see what information was available when it was inferring the types.

There is a typespec for print_odt/1, but dialyzer only uses typespecs to narrow down the success types once they’re found. Which is not this case, so… that spec wasn’t on dialyzer’s mind at the time of the warning.

The only other info available was the fact that odt was used to call both MyODT.f1/1 and MyODT.f2/1. And that’s the key to solve our mystery! Because if you check the code for that module, you will notice that MyODT.f1/1 has a spec, but MyODT.f2/1 hasn’t.

Not having a spec for MyODT.f2/1, dialyzer does its best and figures out the type of odt has to be the success typing of the argument of that function (i.e. #{'f2':=_,_=>_}). And that type is not opaque. Since there is no spec that says so, there is no way for dialyzer to tell that f2 actually requires an instance of MyODT.t and not any map with an f2 key.

Then, when dialyzer tries to match that type against the success typing of the argument of MyODT.f1/1 (i.e. MyODT.t)… 💥 … There is no way to match a random map type against that opaque type. As a matter of fact, the only type that matches with an opaque type is that same opaque type. That’s the whole point. Even if you manage to build something that looks like the definition of the opaque type if dialyzer can’t prove that it is, in fact, the expected opaque type it will emit a warning. In other words: we are violating the opaqueness of that argument.

Simply adding a spec to MyODT.f2/1 removes both warnings. And that leads us again to the lesson of the day:

If you define an opaque type, you have to add specs to all the exported functions that use it (i.e. your module’s API).

What I would LIKE dialyzer to say

One day, someone will finish what Elli Fragkaki once started and dialyzer will tell us something along the lines of…

lib/dialyzer_example.ex:19: Function print_odt/1 has no local return
lib/dialyzer_example.ex:19: The call to 'Elixir.MyODT':f1/1 requires an opaque term of type 'Elixir.MyODT':t() as 1st argument and the variable that you're using for it (Vodt@1) must have type #{'f2':=_, _=>_} since it's also used in a call to 'Elixir.MyODT':f2/1

…or something even clearer and more helpful!

In Other News…

SpawnFest

Like every year since 2017, SpawnFest is coming!

This year it will happen on September 21st & 22nd.

Spawnfest is an annual 48-hour FREE online development competition for all beamers! You can build teams of up to four people and you’ll have 48 hours (a weekend) to create the best BEAM-based applications you can.

You can win some amazing prizes provided by our sponsors. Did I mention it’s FREE and ONLINE (i.e. you can play in your pajamas)?

Registration is open and you can either build a team yourself or register as an independent developer and our mystical algorithm™️ will help you find a great team.

We’re also looking for sponsors. If your company provides a service or a product and wants to give some of it as a prize for the winners, just like DigitalOcean did… please point them our way :)

ElixirConfLA

ElixirConf is coming to Latin America for the first time!

Thanks to our friends from PlayUS Media, we’ll meet on Medellín, Colombia for ElixirConfLA on October 24th & 25th.

We already have an amazing speaker lineup, including Verónica Lopez, Andrea Leopardi, Carlos Andres Bolaños, Francesco Cesarini, Mariano Guerra, Carolina Pascale Campos, Milton Mazzani and Simón Escobar, and the CFT is open until July 19th.

It will be a great event that you don’t want to miss.

You can still get Very Early Bird Tickets.

Erlang Battleground

As usual, a reminder: This publication is still looking for writers. If you want to join us, just get in touch with me (Brujo Benavides) and I’ll add you.