Introduce `?TYPE` macro

[michalmuskala]

It allows explicitly using PropEr's "native types" feature.

This is more powerful than the current automatic parse transform-based inference:

• it can be used outside of ?FORALL to produce PropEr types & combine them with other PropEr or native types.
• it allows using the "native types" feature with the proper parse transform disabled
• it allows expressing more types directly, without creating additional type aliases, for example: ?TYPE(atom() | float()).

The semantics are identical to automatic inference, if the expression was wrapped in a simple id type (when the syntax allows expressing such a type). For example:

-record(foo, {}).
-type id(X) :: X.

% semantically equivalent definitions:
?FORALL(X, id(#foo{}), Prop).
?FORALL(X, ?TYPE(#foo{}), Prop).

Original PR message:

This allows running proper, with the `PROPER_NO_TRANS` flag, with no loss of functionality in practice, by replacing the implicit type usage introduced by the parse transform, by explicit calls to a new `?TYPE` macro. In practice, this is even more powerful than the parse transform. In particular, it's possible to define ad-hoc types with `?TYPE(X | Y)`, where before defining a one-off type alias was necessary.

[kostis]

Thanks for the PR, but I have some questions / concerns about it.

I understand the rationale for allowing the possibility to run PropEr without the parse_transform, but the current description of the PR is very vague (and slightly contradictory). Most notably, it does not come with any description of what is allowed (or not allowed) to be the argument of the ?TYPE macro. Module local types only (as the single, very simple, example shows) or remote types too? Can one specify records there and how are these handled? In short, does it allow for everything that the current language of types allows or not?

Second, can I use ?TYPE independently of whether the PROPER_NO_TRANS flag is set (when compiling the module)?

• If no, why do I have to specify both (as in the simple example)?
• If yes, what does/should it do in this case?

Third, I am a bit uncertain whether allowing to write X | Y types are a good idea. Note that this suddenly allows for the type notation to be used in arbitrary places in the code, when before this PR only Erlang terms were allowed. Is this a good idea?

Finally, but perhaps these are only minor issues, I have a slight trouble with the phrasing that the PR message uses.

1. What does

   with no loss of functionality in practice

   mean? That there is some loss in theory? If so, what?

2. I do not see anything that is replaced here. I only see the introduction of a new ?TYPE macro that adds some particular functionality. What exactly is replaced ? (or is it just unfortunate phrasing)

[michalmuskala]

Hi @kostis, thank you for your feedback. I updated the description to make it clearer, and I've also updated the documentation to mention the ?TYPE macro.

Indeed, this is adding a new feature. The fact that it enables using PropEr's "native types" feature without the parse transform is a side-effect (quite desirable to me, though, and the initial trigger for developing this feature).

I believe the updated commit message and documentation should address your concerns & questions. I believe the only element that is not addressed is: "is this a good idea":

I believe it is, making PropEr more powerful and succinct in what it can express. Moreover, the X | Y types are already partially supported by PropEr, just not in all the cases, for example:

-type id(X) :: X.

?FORALL(X, id([atom() | float()]), ...).

I believe this change makes PropEr more consistent allowing the same syntax to be used everywhere and not be subject to the limitations of the Erlang parser/compiler.

[codecov-commenter]

Codecov Report

Merging #296 (4814f7e) into master (cfc29e7) will increase coverage by 0.08%. The diff coverage is n/a.

@@            Coverage Diff             @@
##           master     #296      +/-   ##
==========================================
+ Coverage   85.34%   85.42%   +0.08%     
==========================================
  Files          14       14              
  Lines        4591     4591              
==========================================
+ Hits         3918     3922       +4     
+ Misses        673      669       -4     

Impacted Files	Coverage Δ
src/proper_typeserver.erl	78.86% <ø> (ø)
src/proper_gen.erl	86.25% <0.00%> (-0.48%)	:arrow_down:
src/proper.erl	71.01% <0.00%> (-0.25%)	:arrow_down:
src/proper_types.erl	94.77% <0.00%> (ø)
src/proper_erlang_abstract_code.erl	94.24% <0.00%> (+0.16%)	:arrow_up:
src/proper_statem.erl	94.67% <0.00%> (+1.90%)	:arrow_up:

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update cfc29e7...4814f7e. Read the comment docs.

[michalmuskala]

Is there anything missing here from my side?