Erlang records with both type and value restrictions as well as default values

Question

I am trying to write a record which represents a bank account:

-record(account, {  name :: atom(),
                    type :: atom(),
                    balance = 0 :: integer()  }).

I also want to restrict the balance to always be >= 0. How do I do this?

Answer 1

Something like balance = 0 :: 0 | pos_integer() might do the trick.

edit wasn't sure it existed, but non_neg_integer() would be better :

balance = 0 :: non_neg_integer()

Answer 2

As noted by others, the type specifications are merely inputs to analysis tools like PropEr and Dialyzer. If you need to enforce the invariant balance >= 0, the account type should be encapsulated, accessible only to functions that respect the invariant:

-module(account).

-record(account, { name :: atom(),
                   type :: atom(),
                   balance = 0 :: non_neg_integer() }).

%% Declares a type whose structure should not be visible externally.
-opaque account() :: #account{}.
%% Exports the type, making it available to other modules as 'account:account()'.
-export_type([account/0]).

%% Account constructor. Used by other modules to create accounts.
-spec new(atom(), atom(), non_neg_integer()) -> account().
new(Name, Type, InitialBalance) ->
    A = #account{name=Name, type=Type},
    set_balance(A, InitialBalance).

%% Safe setter - checks the balance invariant
-spec set_balance(account(), non_neg_integer()) -> account().
set_balance(Account, Balance) when is_integer(Balance) andalso Balance >= 0 ->
    Account#account{balance=Balance};
set_balance(_, _) -> error(badarg). % Bad balance

Notice how this resembles a class with private fields in object-oriented languages like Java or C++. By restricting access to "trusted" constructors and accessors, the invariant is enforced.

This solution doesn't provide protection against malicious modification of the balance field. It's entirely possible for code in another module to ignore the "opaque" type specification and replace the balance field in the record (since records are just tuples).