Uploaded image for project: 'Erlang/OTP'
  1. Erlang/OTP
  2. ERL-373

Add the concept of "purity" to Erlang type specifications

    XMLWordPrintable

    Details

    • Type: New Feature
    • Status: Open
    • Priority: Trivial
    • Resolution: Unresolved
    • Affects Version/s: None
    • Fix Version/s: None
    • Component/s: None
    • Labels:
      None

      Description

      Currently, in the Erlang programming language, the only things that are "pure" are guard expressions. The only allowed functions in guard expressions are guard functions which can not currently be user-defined functions. This feature would only be focused on asserting the purity of an Erlang function in the Erlang type specification, and would not attempt to allow user-defined guard functions, though that may be an additional (later) step in this direction.

      To make this "purity" concept more concrete it seems necessary to break the concept of purity into two types of purity (I am not sure about well accepted names for these concepts, if they exist):

      • "operational purity" is the practical concept of purity where the compilation platform does not change regardless of how/when you get the result in a function (this concept of purity is present in the Haskell programming language, due to things like https://hackage.haskell.org/package/base-4.9.1.0/docs/System-Info.html providing pure functions)
      • "mathematical purity" is a stricter concept of purity where everything behaves with strict mathematical laws

      Representing the "operational purity" concept for Erlang functions in Erlang type specifications would allow developers to focus on high-level nondeterminism for more thorough testing and possible refactoring, making it easier to manage Erlang source code development. The "operational purity" concept in Erlang type specifications could be a pure or impure optional prefix keyword within Erlang type specifications as shown below:

      % would be in the stdlib ets module:
      -spec impure match_delete(Tab, Pattern) -> 'true' when
            Tab :: tab(),
            Pattern :: match_pattern().
      

      A simpler approach to make the usage of this feature more gradual and backward compatible would be to add both a pure and an impure attribute that may be used instead of the spec attribute:

      % would be in the stdlib ets module:
      -impure match_delete(Tab, Pattern) -> 'true' when
            Tab :: tab(),
            Pattern :: match_pattern().
      

      The ets:match_delete/2 is impure (with either concept of purity) due to a write to global state (erlang:put/2 is also impure, though the state is isolated within an Erlang process, since the state is global to all function calls the Erlang process calls after the erlang:put/2 function). A read of global state of a value that may change during runtime (not the compilation platform, but any mutable state concept that is present) is impure. It is also impure to catch exceptions, but not to throw exceptions, so any functions that use catch or try...catch would need to be marked as impure.

      The main examination of purity in Erlang is the paper "Purity in Erlang" by Mihalis Pitidis and Konstantinos Sagonas (http://dl.acm.org/citation.cfm?id=2050144 http://user.it.uu.se/~kostis/Papers/purity.pdf). However, the focus of this paper is on the "mathematical purity" concept mentioned above, as the concept may be applied to user-defined guard functions. For example, the paper would want filename:basename/1 to be marked as an impure function due to reading a global constant value that determines the platform being used for the runtime. With the "operational purity" concept mentioned in this issue, the filename:basename/1 would be marked as a pure function, and that approach would be consistent with the concept of purity in the Haskell programming language.

      There was work done by Joe Armstrong, described in his PhD thesis, that classifies AXD301 function/module usage into "clean" and "dirty" which relates to this feature. This can be found in section 8.3 on pages 171 to 174. In this approach, the receive expression is considered impure because it prevents the function from being strictly referentially transparent.

      The optional usage of pure and impure in Erlang type specifications would help dialyzer recognize any impure Erlang source code if pure is used in an Erlang type specification for a function that calls Erlang functions that are impure. The change to the Erlang type specification described above is only a suggestion, while the concept of "operational purity" in Erlang source code is what is important, so the syntax usage may want/need to be different from the use of impure and pure atoms before the function name.

        Attachments

          Activity

            People

            Assignee:
            otp_team_vm Team VM
            Reporter:
            okeuday Michael Truog
            Votes:
            2 Vote for this issue
            Watchers:
            4 Start watching this issue

              Dates

              Created:
              Updated: