EEP 61: Built-in dynamic type #

Abstract #

This EEP proposes a new built-in type dynamic() (in addition to existing built-in type term()) to make Erlang friendly to gradual type checking. Having a special dynamic type for gradual typing is a widely adopted industrial solution.

Gradual typing and dynamic type #

Erlang is one of many programming languages which started as pure dynamically typed languages with no static type information but then got extensions (or dialects) to specify type information (type hints, specs) in source code.

Erlang got extended with specs through EEP 8 (Types and function specifications).

The current documentation for types and specs can be found at https://www.erlang.org/doc/reference_manual/typespec.html.

Beyond being used for documentation purposes, types and specs can be used by tooling for static analysis. The existing tools include:

• dialyzer
• eqWAlizer
• Gradualizer and its Elixir frontend Gradient

Dialyzer uses type specs in the paradigm of success typing (documented in Pull Request 6281 “Document the meaning of specs” and in the original paper “A language for specifying type contracts in Erlang and its interaction with success typings”). It is worth to note that dialyzer handles specs very differently from traditional type checkers.

eqWAlizer uses type specs to perform type checking in a traditional manner.

As of now, the main industrial approach to adopt or retrofit static typing to dynamically typed languages is through gradual typing (https://en.wikipedia.org/wiki/Gradual_typing, http://samth.github.io/gradual-typing-bib). Gradual typing features a special type dynamic or ?, which allows to mix untyped (or dynamically typed) and statically typed code in a user-friendly manner and also helps adopt static typing incrementally in large projects. Having a special dynamic type for gradual typing is a widely adopted solution.

Since Erlang doesn’t have a built-in dynamic type in the surface syntax, eqWAlizer had to introduce its own type eqwalizer:dynamic() with special semantics for the purposes of gradual typing.

term()/any() and subtyping through examples #

Before starting discussing the dynamic type, it is worth to clarify the meaning and semantics of the built-in Erlang types term() and any().

• any() is the top type element of the subtyping lattice. This is clearly stated in Erlang documentation
• term() is an alias to any(). They are the same types. In the rest of the document we would use term() as it’s more Erlang-specific.

The type term() is similar to the following types in other languages and type-checkers:

• object in Python (see also the details about object in the typing documentation). mypy, PyRight, Pyre handle object the same way.
• unknown in Typescript
• top in Ruby 3 rbs (https://github.com/ruby/rbs/blob/master/docs/syntax.md)
• unknown in luau
• mixed in Hack
• mixed in Flow

Using term() value where a more concrete type is expected is a type error from the point of view of traditional static typing.

Let’s take a look at the examples.

Example 1. Erlang, eqWAlizer:

-module(example).

-spec foo(term()) -> number().
foo(N) ->
    N.
    ^ % type error. expected: number(), got: term()

-spec n(number()) -> number().
n(N) -> N.

-spec foo_n(term()) -> number().
foo_n(N) ->
    n(N).
      ^ type error. expected: number(), got term()

Example 2. Python, mypy:

def foo(n: object) -> int:
    return n
           ~ Incompatible return value type (got "object", expected "int")

def n_fun(n: int) -> int:
    return n

def foo_n(n: object) -> int:
    return n_fun(n)
                 ~ Argument 1 to "n_fun" has incompatible type "object";
                                              expected "int"  [arg-type]

Example 3. TypeScript:

function foo(x: unknown): number {
    return x;
    ~~~~~~~~~ Type 'unknown' is not assignable to type 'number'.(2322)
}

function n_fun(n: number): number {
    return n;
}

function foo_n(n: unknown): number {
    return n_fun(n);
                 ~ Argument of type 'unknown' is not assignable
                                  to parameter of type 'number'
}

dynamic() type #

eqWAlizer has a special type eqwalizer:dynamic() which is documented here.

The type is similar to the following types in other languages and type-checkers:

• Any in Python (mypy, PyRight, pyre handle it the same way)
• any in TypeScript
• untyped in Ruby/rbs
• untyped in Ruby/Sorbet
• any in luau
• dynamic in Hack
• any in Flow

eqWAlizer borrowed the name from Hack. The naming choice was dictated by the following considerations:

• eqwalizer:any() would misleading and confusion because of the built-in Erlang type any()
• eqwalizer:dynamic() is often used to mark “inherently dynamic code”: reading from ETS, message passing, deserialization and so on.

(In the rest of the document we use just dynamic() as an abbreviation for eqwalizer:dynamic().)

The rationale for introducing dynamic() type is given in eqWAlizer documentation and in the already mentioned resources for other languages and type checkers.

We propose to extend Erlang surface syntax with new dynamic() built-in type to make Erlang more friendly to tooling built on ideas of gradual typing (like eqWAlizer or Gradualizer) and ease its adoption (including using it for typing OTP libraries).

Can it be just one type? #

One may argue that just one type - term()/any() may be enough, and it’s up to tooling to interpret it as a proper top type or as a special dynamic type for gradual typing. This, however, would be limiting in the long run.

The stories of other similar languages and type checkers exhibit a commonality: they all ended up in having options or modes for different levels of strictness and guarantees. Or, roughly speaking - they have at least two modes: gradual mode and strict mode. Gradual mode is optimised for a non-intrusive incremental adoption while strict mode is optimised for type safety and strong sound guarantees.

• In large enough projects there appear places with strict typing and places with “mostly dynamic typing”.
• Differentiating between term() and dynamic() without introducing ambiguity or confusion becomes important.
• The language of types is not always expressive enough to write down precise types. In this case dynamic() type works as an escape hatch.
• In some mission-critical applications where correctness is of most importance, one may want to use term() type with verbose checks/guards to make sure that nothing escapes type-checking.
• Using only term()/any() has also proven problematic, in practice, in the development of Gradualizer. Originally, Gradualizer repurposed any() for the dynamic type and used term() as the top type. According to the Gradualizer’s authors it turned out to be confusing and incompatible with the pre-existing use of these types.

What does this mean for dialyzer? #

Internally, dialyzer already uses any()/term() as dynamic() with respect to specs.

An example:

-module(example).
-export([get_foo/1, get_bar/1, get_moo/1]).

-record(rec, {
  foo :: term() | atom(),
  bar :: number() | atom(),
  moo :: term()
}).

-spec get_foo(#rec{}) -> number().
get_foo(R) -> R#rec.foo.

-spec get_bar(#rec{}) -> number().
get_bar(R) -> R#rec.bar.

-spec get_moo(#rec{}) -> number().
get_moo(R) -> R#rec.moo.

Running dialyzer (dialyzer example.erl) produces the output:

example.erl:14:2: The success typing for example:get_bar/1 implies
                  that the function might also return atom()
                  but the specification return is number()

As for eqwalizer:dynamic() - it’s defined as an alias to any()/term() and can be used together with dialyzer. (However, defining it this way creates confusion for pedantic and curious users.)

Reference Implementation #

https://github.com/erlang/otp/pull/6993

Backward compatibility #

With PR 6335 (Allow local redefinition of built-in types) the change would be backward compatible in OTP 26.

Copyright #

This document is placed in the public domain or under the CC0-1.0-Universal license, whichever is more permissive.