# Module proper_typeserver

- Description
- Data Types
- Function Index
- Function Details

Erlang type system - PropEr type system integration module.

Copyright © 2010-2017 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas

Version: Jan 2 2021 16:13:06

Behaviours: `gen_server`.

Authors: Manolis Papadakis.

## Description

Erlang type system - PropEr type system integration module.

PropEr can parse types expressed in Erlang's type language and convert them to its own type format. Such expressions can be used instead of regular type constructors in the second argument of `?FORALL`s. No extra notation is required; PropEr will detect which calls correspond to native types by applying a parse transform during compilation. This parse transform is automatically applied to any module that includes the `proper.hrl` header file. You can disable this feature by compiling your modules with `-DPROPER_NO_TRANS`. Note that this will currently also disable the automatic exporting of properties.

The use of native types in properties is subject to the following usage rules:

- Native types cannot be used outside of `?FORALL`s.
- Inside `?FORALL`s, native types can be combined with other native types, and even with PropEr types, inside tuples and lists (the constructs `[...]`, `{...}` and `++` are all allowed).
- All other constructs of Erlang's built-in type system (e.g. `|` for union, `_` as an alias of `any()`, `<<_:_>>` binary type syntax and `fun((...) -> ...)` function type syntax) are not allowed in `?FORALL`s, because they are rejected by the Erlang parser.
- Anything other than a tuple constructor, list constructor, `++` application, local or remote call will automatically be considered a PropEr type constructor and not be processed further by the parse transform.
- Parametric native types are fully supported; of course, they can only appear instantiated in a `?FORALL`. The arguments of parametric native types are always interpreted as native types.
- Parametric PropEr types, on the other hand, can take any kind of argument. You can even mix native and PropEr types in the arguments of a PropEr type. For example, assuming that the following declarations are present:

               my_proper_type() -> ?LET(...).
               -type my_native_type() :: ... .

  Then the following expressions are all legal:

               vector(2, my_native_type())
               function(0, my_native_type())
               union([my_proper_type(), my_native_type()])

- Some type constructors can take native types as arguments (but only inside `?FORALL`s):
  - `?SUCHTHAT`, `?SUCHTHATMAYBE`, `non_empty`, `noshrink`: these work with native types too
  - `?LAZY`, `?SHRINK`, `resize`, `?SIZED`: these don't work with native types
  - `?LET`, `?LETSHRINK`: only the top-level base type can be a native type
- Native type declarations in the `?FORALL`s of a module can reference any custom type declared in a `-type` or `-opaque` attribute of the same module, as long as no module identifier is used.
- Typed records cannot be referenced inside `?FORALL`s using the `#rec_name{}` syntax. To use a typed record in a `?FORALL`, enclose the record in a custom type like so:

               -type rec_name() :: #rec_name{}.

  and use the custom type instead.
- `?FORALL`s may contain references to self-recursive or mutually recursive native types, so long as each type in the hierarchy has a clear base case. Currently, PropEr requires that the toplevel of any recursive type declaration is either a (maybe empty) list or a union containing at least one choice that doesn't reference the type directly (it may, however, reference any of the types that are mutually recursive with it). This means, for example, that some valid recursive type declarations, such as this one:

               ?FORALL(..., a(), ...)

  where:

               -type a() :: {'a','none' | a()}.

  are not accepted by PropEr. However, such types can be rewritten in a way that allows PropEr to parse them:

               ?FORALL(..., a(), ...)

  where:

               -type a() :: {'a','none'} | {'a',a()}.

  This also means that recursive record declarations are not allowed:

               ?FORALL(..., rec(), ...)

  where:

               -type rec() :: #rec{}.
               -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).

  A little rewritting can usually remedy this problem as well:

               ?FORALL(..., rec(), ...)

  where:

               -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
               -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).

- Remote types may be referenced in a `?FORALL`, so long as they are exported from the remote module. Currently, PropEr requires that any remote modules whose types are directly referenced from within properties are present in the code path at compile time, either compiled with `debug_info` enabled or in source form. If PropEr cannot find a remote module at all, finds only a compiled object file with no debug information or fails to compile the source file, all calls to that module will automatically be considered calls to PropEr type constructors.
- For native types to be translated correctly, both the module that contains the `?FORALL` declaration as well as any module that contains the declaration of a type referenced (directly or indirectly) from inside a `?FORALL` must be present in the code path at runtime, either compiled with `debug_info` enabled or in source form.
- Local types with the same name as an auto-imported BIF are not accepted by PropEr, unless the BIF in question has been declared in a `no_auto_import` option.
- When an expression can be interpreted both as a PropEr type and as a native type, the former takes precedence. This means that a function `foo()` will shadow a type `foo()` if they are both present in the module. The same rule applies to remote functions and types as well.
- The above may cause some confusion when list syntax is used:
  - The expression `[integer()]` can be interpreted both ways, so the PropEr way applies. Therefore, instances of this type will always be lists of length 1, not arbitrary integer lists, as would be expected when interpreting the expression as a native type.
  - Assuming that a custom type foo/1 has been declared, the expression `foo([integer()])` can only be interpreted as a native type declaration, which means that the generic type of integer lists will be passed to `foo/1`.
- Currently, PropEr does not detect the following mistakes:
  - inline record-field specializations that reference non-existent fields
  - type parameters that are not present in the RHS of a `-type` declaration
  - using `_` as a type variable in the LHS of a `-type` declaration
  - using the same variable in more than one position in the LHS of a `-type` declaration

You can use these functions to try out the type translation subsystem.

CAUTION: These functions should never be used inside properties. They are meant for demonstration purposes only.

## Data Types

### fin_type()

    fin_type() = proper_types:type()

### mod_name()

    mod_name() = atom()

### rich_result()

    rich_result(T) = {ok, T} | {error, term()}

## Function Index

demo_is_instance/3 | Checks if `Term` is a valid instance of native type `TypeExpr` (which should be provided inside a string).
demo_translate_type/2 | Translates the native type expression `TypeExpr` (which should be provided inside a string) into a PropEr type, which can then be passed to any of the demo functions defined in the `proper_gen` module.

## Function Details

### demo_is_instance/3

    demo_is_instance(Term :: term(),
                     Mod :: mod_name(),
                     TypeExpr :: string()) ->
                        boolean() | {error, term()}

Checks if `Term` is a valid instance of native type `TypeExpr` (which should be provided inside a string). PropEr acts as if it found this type expression inside the code of module `Mod`.

### demo_translate_type/2

    demo_translate_type(Mod :: mod_name(), TypeExpr :: string()) ->
                           rich_result(fin_type())

Translates the native type expression `TypeExpr` (which should be provided inside a string) into a PropEr type, which can then be passed to any of the demo functions defined in the `proper_gen` module. PropEr acts as if it found this type expression inside the code of module `Mod`.

Generated by EDoc