search

erlang / eep

Erlang Enhancement Proposals
http://www.erlang.org/erlang-enhancement-proposals/
264 stars 66 forks source link

Added eep draft for nominal types #60

Closed lucioleKi closed 4 months ago

lucioleKi commented 5 months ago

This commit adds the eep draft for nominal types. I plan to make a post on Erlang forum, introducing nominal types. The post will refer to this pull request.

RaimoNiskanen commented 5 months ago

I am missing a more formal definition for the suggested nominal types. As it stands now I have a hard time to follow the reasoning and examples...

Such as:

A function that has a -spec that states an argument to be nominal type a/0, accepts:

A function that has a -spec that it returns a nominal type b/0 may return:

A function that has a -spec that states an argument to be structural type c/0, accepts:

A function that has a -spec that it returns a structural type d/0 may return:

"supertype" and "subtype" also needs to be defined, and maybe "compatible structural type"

zuiderkwast commented 5 months ago

That's what I though opaque types are. My interpretation of opaque types is that you can't assume anything about what they are so you need to treat them as nominal types.

Type checkers probably differ here though. I don't know what Dialyzer does.

lucioleKi commented 5 months ago

@RaimoNiskanen It seems that my intentional avoidance of subtyping in the EEP draft causes more problems than benefits. I used 'nested nominals' instead of 'subtyping', because I wanted to emphasize that the supertypes and subtypes accepted are nominal supertypes and nominal subtypes. In Erlang, the only way to declare a nominal subtype is to declare a nested nominal of the form -nominal a() :: b() where b() is another nominal type.

I'd phrase it as follows (same for b/0):

A function that has a -spec that states an argument to be nominal type a/0, accepts:

RaimoNiskanen commented 5 months ago

@lucioleKi, and what gives for return types?

lucioleKi commented 5 months ago

@zuiderkwast Yes, opaque types have always been type-checked by names in Dialyzer, just with more restrictions. Dialyzer assumes no knowledge about opaque's structure, does not consider subtyping, etc. That's why the proposed nominal type-checking can cover opaque type-checking internally in Dialyzer. Nominal types are 'transparent' though. This EEP suggests a way to support nominal types and type-checking without opacity.

lucioleKi commented 5 months ago

@RaimoNiskanen The examples c/0 and d/0 behaves as you described. For a nominal type a() :: T and a structural type S, S is a 'compatible structural type' of a() when the intersection of T and S is non-empty. (I'm not sure if this definition is too technical. This is how Dialyzer does it internally.)

A function that has a -spec that it returns a nominal type b/0 may return the following without Dialyzer raising an error:

RaimoNiskanen commented 5 months ago

Great! I think these definitions should be in the EEP.

RaimoNiskanen commented 5 months ago

A general comment; I think the EEP should at least try to be less Dialyzer-centric.

When the text can be more generic, talk about "the type checker" and how nominals are supposed to be handled by "the type checker"; any type checker.

When talking about the implementation the text must of course talk about Dialyzer...