EEP: Nominal Type

Erlang/OTP Proposals Proposals: RFC
1

Hi all! I’m Isabell. I’m working on adding nominal types to Erlang for my master thesis in Uppsala University, and I will be joining the OTP team after graduation. Now that I have a relatively stable implementation, I’d like to know more about how you think of this new feature. Thank you all in advance!
Here’s my EEP: Nominal type · Pull Request #60 · erlang_eep

20 Likes
2

Sounds really useful. I have one question though. Let’s suppose I have type definitions like this:

-nominal inch() :: integer(). % The imperial unit, 25.4 mm
-nominal zoll() :: integer(). % The German Zoll unit, 25.4 mm

If I want to create a function like this:

-spec inch_to_coll(inch()) -> zoll().
inch_to_coll(I) ->
  I.

Is it supposed to work or will dialyzer complain? If dialyzer complains, how do I make it work? This example may be far fetched, but what if I have lib_a:meter() and lib_b:meter() types?

3

Sounds promising, that could help a lot with confusion over list/string and could fit nicely with maps.

However, what is the exact reason for the new syntax? Is nominal/structural property of the type or the type checking mechanism? Everything that is nominally correct is structurally correct, but not the other way around. Could we have like “nominal” mode for dialyzer that would just check types nominally, without imposing any changes on the user code? If I understood it correctly, changes in the reference PR already do change the way Dialyzer handles opaques which seems counterintuitive to me if “nominal” is a new type of type.

What is also unclear to me from to EEP:

- **Maintainability**: Nominal type checking introduces no special cases for
Dialyzer.  All extra type checking functions specifically for opaques can
now be removed.

Does that mean that -nominal is a replacement for -opaque or am I missing the point?

4

Hi NAR! I ran your inch_to_coll/1 function through Dialyzer with my current implementation. Dialyzer doesn’t complain and it shouldn’t. This kind of function is one way to do conversion for nominal types that have the same structural type.

If we have two nominal types lib_a:meter() and lib_b:meter() (assuming they are both exported), they will not be compatible with each other. A nominal type is uniquely identified by a combination of 3 things: module name, nominal name, and arity. When two nominal types differ by module names, they are not compatible even though they are both named meter().

Thank you for the response! You’re asking very valid questions. I hope my explanation makes it clearer :wink:

2 Likes
5

Hi mmin! Thanks for giving my EEP this much thought. Answering questions about design choices makes me happy. Feel free to follow-up if I didn’t understand you correctly.

However, what is the exact reason for the new syntax?

The main reason is to not break backward compatibility for existing syntax. -type and -opaque have different meanings and use cases than -nominal. The -nominal syntax let user express a new intention that wasn’t supported by -type or -opaque: they are defining a non-opaque type that should be type-checked in the nominal way.
Since there has to be a new syntax, only replacing -type or -opaque with -nominal minimizes refactoring effort for users.

Is nominal/structural property of the type or the type checking mechanism?

It’s the type checking mechanism in Dialyzer. By defining nominal types using -nominal, the user enables the new nominal type checking mechanism in Dialyzer.

Could we have like “nominal” mode for dialyzer that would just check types nominally, without imposing any changes on the user code?

Technically it’s doable, but I’m unsure how useful it’d be. When the “nominal” mode is turned on, should all -type mean -nominal and use nominal type-checking rules? If so, the nominal mode seems to do a no-brain find-and-replace for the user.
Here’s an idea I’ve discussed with multiple people in the OTP team though: I could write an interactive tool that scans the codebase, and suggests which -type declarations might benefit from nominal type-checking. If the user enters ‘yes’ for the change, the tool replaces -type with -nominal, and then automatically reruns Dialyzer. If new inconsistencies arise, the tool reverts the change.
Does this sound useful?

If I understood it correctly, changes in the reference PR already do change the way Dialyzer handles opaques which seems counterintuitive to me if “nominal” is a new type of type.
Does [the Maintainability bullet point in the EEP] mean that -nominal is a replacement for -opaque or am I missing the point?

-opaque has different semantics than nominal types. Nominal types are ‘transparent’. There is no hidden documentation or restriction on how to interact with the type. Opaques have distinct use cases, and they will not be replaced at all.
Only Dialyzer’s internal type-checking functions for opaques are changed to use those of nominals. It is for optimization purposes within Dialyzer. If this EEP goes through, some more inefficient type-checking functions for opaques can be safely removed.

2 Likes
7

The ‘inches to zolls’ example would look like this in Ada.
type Inches is new Integer;
type Zolls is new Integer;
function Inches_To_Zolls(I: Inches) return Zolls is
begin
return Zolls(Integer(I)); – or just Zolls(I)
end Inches_To_Zolls;

What I’d really expect to see in Erlang would be something like
inches_to_zolls(inches(N)) → zolls(N),
And of course what I’m thinking of here is Haskell’s ‘newtype’:
newtype Inches = Inches Int
newtype Zolls = Zolls Int
inches_to_zolls (Inches n) = Zolls n
where Inches and Zolls are compile-time wrappers with zero run-time cost.

So I’m suggesting that
()
should be allowed in Erlang patterns and
()
should be allowed in Erlang expressions and
in both cases compilation would work by erasure
but type checking in a pattern would convert from
the derived type to the base type and in an expression
go from the base type to the derived type.

This would completely avoid any need for blowing a 20-foot hole
in your pressure hull to allow integer() and meter() to be mixed up.

1 Like
9

But it could make other software that rely on Erlang AST backward incompatible, especially other type checkers.

Okay, but if we agree that opaques should be always be checked nominally (as per PR), the only thing you want to change is -type → -nominal in places where you could benefit of it?

Yes, but there won’t be any change in the code itself, it would only instruct the dialyzer on how to compare types, either structurally or nominally. The benefit is that it would require 0 changes on the user side and you can switch to any system whenever you want without no changes is the code. The cost is reduced flexibility (you either have all your types nominal or none, nothing between). That would surely be more usable than switching all your codebase from type to nominal. The question is, are there situations where you really want to avoid having nominal types of this kind?

Also, isn’t nominal vs structural about comparing two types, not the type itself. By “structural types”, does one mean: “type that compares structurally with the other type”. What happens when you have to compare -type and -nominal? What if, in your example, meter() was declared as -type and feet() declared as -nominal(), what would be the result and what’s the reasoning behind it?

11

Now that I’ve thought about inch_to_coll/1 a bit more, a more “correct” way of doing the conversion would be inch_to_coll(I) -> I * 1 or inch_to_coll(I) -> I + 0.

12

I am confused when comparing inch_to_coll/1 and foo/0 example from the EEP:

-nominal inch() :: integer(). % The imperial unit, 25.4 mm
-nominal zoll() :: integer(). % The German Zoll unit, 25.4 mm
-spec inch_to_coll(inch()) -> zoll().
inch_to_coll(I) ->
  I.

% from the EEP
% Declaration of nominal types
-nominal meter() :: integer().
-nominal feet() :: integer().

% Constructor for nominal types
-spec meter_ctor(integer()) -> meter().
meter_ctor(X) -> X.
-spec foo() -> feet().
foo() -> meter_ctor(24). % error

Let me rewrite foo with a variable for more clarity:

-spec foo() -> feet().
foo() -> 
  Result = meter_ctor(24),
  Result.

My understanding (from your answer) is that inch_to_coll/1 is considered well-typed while (from the EEP) foo/0 is considered ill-typed. Why is that?

In foo/0 Result is of nominal type meter() where another nominal type (feet()) is expected - and there is a type error.
But in inch_to_coll/1 I is of nominal type inch() where another nominal type zoll()is expected - and it’s considered to be well typed. foo/0 and inch_to_coll/1 look the same to me. What am I missing?

13

Specs don’t yet constrain arguments going in, so I does not have nominal type inch() even though you’d expect it to. An upcoming EEP will change this behavior and make both of those versions illegal.

1 Like
14

I just came here to say thank you for the work. I know for a lot of people, it may not seem like a lot, but I have dived into the Dialyzer codebase. This is a real improvement, that will be felt and will have an impact across the field.

First because of the added expressiveness and ability to handle nested opaque and all. Which is already great.

But the speed up is the most important. Any second we can shave off Dialyzer runs have a tremendous impact on people using it. Not because it earns them time back but because the slowness of Dialyzer is one of the reasons it gets cut out of so many places. And usually, these effects are “cliff” effects. The moment the time taken to check a whole codebase goes back under a certain cliff, then usage grows.

So, this may not seem like a lot to people, but this is a lot of work, and it will have an impact. You made my weekend far better with this. Thank you, and thanks to the OTP team for helping. And good luck joining the team; I hope I have the opportunity to work with you on some PR in the future <3

6 Likes
15

But it could make other software that rely on Erlang AST backward incompatible, especially other type checkers.

Not really, because how compiler handles existing abstract formats is unchanged. The only change is that compiler now understands -nominal as a new attribute, just like compiler understands -doc after it was introduced as an attribute. It is Dialyzer that reads in the abstract format for nominal types and performs type-checking. Afaik, no other type checker for Erlang uses names of non-opaque types in their type-checking.
If you still think this change breaks backward compatibility, could you give an example?

If we agree that opaques should be always be checked nominally (as per PR), the only thing you want to change is -type → -nominal in places where you could benefit of it?

Yes. It’s totally up to the user if they want to use a -type syntax, so that Dialyzer performs the usual structural type-checking, or to use the new -nominal syntax, so that Dialyzer performs nominal type-checking, if they see the benefits of doing so.

The benefit is that it would require 0 changes on the user side and you can switch to any system whenever you want without no changes is the code. The cost is reduced flexibility (you either have all your types nominal or none, nothing between). That would surely be more usable than switching all your codebase from type to nominal . The question is, are there situations where you really want to avoid having nominal types of this kind?

I see your point now, and I agree with the benefit and the cost you mentioned. I think I need to do more experimentation or have more feedback from Erlang users, so that I have more idea about what kind of migration tool would be the most helpful.

By “structural types”, does one mean: “type that compares structurally with the other type”. What happens when you have to compare -type and -nominal ? What if, in your example, meter() was declared as -type and feet() declared as -nominal() , what would be the result and what’s the reasoning behind it?

Yes, for Dialyzer, “type that compares structurally with the other type” has no name tag and only the structural part. Names for -type types are stripped away. -type meter() :: integer() means that meter() is exactly integer(), not a nominal type. Using -type meter() when -nominal foot() is expected is allowed, and vice versa.
The reasoning is that when a user declares a type using -type, we assume that the user wants it to be type-checked structurally (or we have no evidence that the user wants nominal type-checking), so the name does not matter. There are cases where users define -type meter() to have meter() simply as an alias of integer().

1 Like
16

Well… you could probably use a -dialyzer(…). attribute in a module to specify that the types in the module should be analyzed nominally or structurally.

OTOH… An alternative to turning -type into -nominal everywhere could be to have another attribute like… -nominal_types([this/0, that/1, etc/3]).

1 Like
17

On the other hand, -nominal is a minimal change both to dialyzer and other tools, which can safely just treat -nominal like they do -type if they don’t want to deal with nominals yet. The alternatives suggested so far would, as far as I can tell, either be more complicated to implement or “break” other tools just as much.

1 Like