Type representation

[erszcz]

This module and its types, all modelled after Gradualizer code and erl_parse, show why packing AST node attributes into a list leads to unnecessarily convoluted code:

     1  -module(abstract_type_node_attributes).
     2
     3  -export([g/1]).
     4  -export([h/1]).
     5
     6  -include("include/gradualizer.hrl").
     7
     8  -type simple_type() :: {type, list | nonempty_list, [a | simple_type()]}
     9                       | {type, atom, {b}}.
    10
    11  -type simple_type_fixed() :: {type, list | nonempty_list, {a, simple_type()}}
    12                             | {type, atom, {b}}.
    13
    14  -spec g(simple_type()) -> b | simple_type().
    15  g({type, L, []}) when L =:= list; L =:= nonempty_list ->
    16      b;
    17  g({type, list, [a]}) ->
    18      b;
    19  g({type, nonempty_list, [a]}) ->
    20      b;
    21  g({type, list, [a, SimpleTy]}) ->
    22      %% This requires an ?assert_type(SimpleTy, simple_type()) or leads to an error
    23      SimpleTy;
    24  g({type, atom, {_InnerNode}}) ->
    25      b.
    26
    27  -spec h(simple_type_fixed()) -> b | simple_type().
    28  h({type, nonempty_list, {a, _}}) ->
    29      b;
    30  h({type, list, {a, SimpleTy}}) ->
    31      SimpleTy;
    32  h({type, atom, {_InnerNode}}) ->
    33      b.

$ ./bin/gradualizer abstract_type_node_attributes.erl
abstract_type_node_attributes.erl: The variable on line 23 at column 5 is expected to have type b | simple_type() but it has type a | simple_type()

g({type, list, [a, SimpleTy]}) ->
    %% This requires an ?assert_type(SimpleTy, simple_type()) or leads to an error
    SimpleTy;
    ^^^^^^^^

The warning is generated because without an extra hint from the programmer, the typechecker has no way to realise the convention by which [a | simple_type()] means that the first type in the list is going to be a and the second simple_type(). Using a tuple {a, simple_type()} instead of the list would encode that information directly in the type.

Gradualizer commit: 81385f6

[zuiderkwast]

We have chosen long ago to use the abstract format for the type representation, because it is well known, documented and already has pretty-printing and parsing in place. If we pick another representation, we would be able to do much more.

[erszcz]

I understand that, but what I'm arguing here is that the test of time (and some dog-fooding) shows it might've been a poor choice. That is, good to start with, but not that good with the information we have now.

To make it specific, what I'm arguing here is not devising a format from scratch, but introducing just that simple change - that is to rewrite the attribute lists that assign element type to position only by convention to tuples, which assign that type to element explicitly.

For example this erl_parse AST node type:

-type af_function_type() ::
        {'type', anno(), 'fun',
         [ {'type', anno(), 'product', [abstract_type()]} | abstract_type() ]}.

By convention is supposed to be handled like this:

compat_ty({type, _, 'fun', [{type, _, product, Args1} = Prod1, Res1]},
          {type, _, 'fun', [{type, _, product, Args2} = Prod2, Res2]},
          Seen, Env) ->
    {Ap, Cs} = compat_tys(Args2, Args1, Seen, Env),
    {Aps, Css} = compat(?assert_type(Res1, type()), ?assert_type(Res2, type()), Ap, Env),
    {Aps, constraints:combine(Cs, Css)};

I.e. only by convention we know that Prod1 :: {'type', anno(), 'product', [abstract_type()]} and Res1 :: abstract_type() - the type itself does not encode nor require that. This, in turn, requires us (the programmer-user) to do an explicit type assertion ?assert_type(Res1, type()) in the function body.

A rewrite from the original erl_parse to a more strict type would alleviate the need for an explicit assertion:

-type af_function_type() ::
        {'type', anno(), 'fun',
         { {'type', anno(), 'product', [abstract_type()]}, abstract_type() }}.

Such a rewrite from the original erl_parse format could be done when loading type information and undone just before printing.