eep icon indicating copy to clipboard operation
eep copied to clipboard

Added eep draft for nominal types

Open lucioleKi opened this issue 1 year ago • 8 comments

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.

lucioleKi avatar Apr 11 '24 13:04 lucioleKi

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:

  • Nominal type a/0
  • A supertype to nominal type a/0
  • A compatible structural type.
  • ¿ A subtype to nominal type a/0 ?

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

  • Nominal type b/0
  • A supertype to nominal type b/0
  • A compatible structural type.
  • ¿ A subtype to nominal type b/0 ?

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

  • A compatible structural type.
  • A nominal subtype of structural type c/0

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

  • A compatible structural type.
  • A nominal subtype of structural type d/0

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

RaimoNiskanen avatar Apr 18 '24 07:04 RaimoNiskanen

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.

zuiderkwast avatar Apr 18 '24 10:04 zuiderkwast

@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:

  • Nominal type a/0

  • A nominal supertype to nominal type a/0

  • A compatible structural type.

  • A nominal subtype to nominal type a/0

lucioleKi avatar Apr 18 '24 11:04 lucioleKi

@lucioleKi, and what gives for return types?

RaimoNiskanen avatar Apr 18 '24 13:04 RaimoNiskanen

@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 avatar Apr 18 '24 13:04 lucioleKi

@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:

  • Nominal type b/0

  • A nominal supertype to nominal type b/0

  • A compatible structural type.

  • A nominal subtype to nominal type b/0

lucioleKi avatar Apr 18 '24 13:04 lucioleKi

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

RaimoNiskanen avatar Apr 18 '24 13:04 RaimoNiskanen

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...

RaimoNiskanen avatar Apr 22 '24 13:04 RaimoNiskanen