beam_types: Improve the type lattice documentation

2 files changed, 36 insertions, 10 deletions

diff --git a/lib/compiler/src/beam_types.hrl b/lib/compiler/src/beam_types.hrl
index 846ce732e8..323c715da7 100644
--- a/lib/compiler/src/beam_types.hrl
+++ b/lib/compiler/src/beam_types.hrl
@@ -47,6 +47,32 @@
 %% reduced it to 'any'. Since few operations can make direct use of this extra
 %% type information, types should generally be normalized to one of the above
 %% before use.
+%%
+%% When adding a new type it's important that the lattice stays consistent [1].
+%% In brief, the following properties must hold:
+%%
+%% * All types must be unambiguous; any given value must narrow down to a
+%%   single type, and multiple supertypes are not allowed.
+%%
+%% * `meet` is used when we know more about a value (e.g. type tests), so it
+%%   must not return a more general type than either of its arguments. In other
+%%   words, we're only allowed to *add* knowledge in a `meet`.
+%%
+%% * `join` is used when we know less about a value (e.g. phi node), so it
+%%   must not return a more specific type than either of its arguments. In
+%%   other words we're only allowed to *remove* knowledge in a `join`.
+%%
+%% * Both `join` and `meet` must be commutative, associative, and idempotent.
+%%
+%% Maintaining the above may seem trivial but subtle errors can creep in when
+%% adding fields or restrictions to a type. ?TUPLE_ELEMENT_LIMIT is a great
+%% example of this.
+%%
+%% The property test suite ensures that the above holds, so don't forget to
+%% add your new types there. You should also consider increasing ?REPETITIONS
+%% during development to ensure it hits all nooks and crannies.
+%%
+%% [1] https://en.wikipedia.org/wiki/Lattice_(order)#General_lattice
 
 -define(ATOM_SET_SIZE, 5).
 
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
index 8e1cb9b131..adc6e06ead 100644
--- a/lib/compiler/test/property_test/beam_types_prop.erl
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -50,10 +50,10 @@ absorption_1() ->
             absorption_check(TypeA, TypeB)).
 
 absorption_check(A, B) ->
-    %% a ∨ (a ∧ b) = a,
+    %% a ∨ (a ∧ b) = a
     A = join(A, meet(A, B)),
 
-    %% a ∧ (a ∨ b) = a.
+    %% a ∧ (a ∨ b) = a
     A = meet(A, join(A, B)),
 
     true.
@@ -69,12 +69,12 @@ associativity_1() ->
             associativity_check(TypeA, TypeB, TypeC)).
 
 associativity_check(A, B, C) ->
-    %% a ∨ (b ∨ c) = (a ∨ b) ∨ c,
+    %% a ∨ (b ∨ c) = (a ∨ b) ∨ c
     LHS_Join = join(A, join(B, C)),
     RHS_Join = join(join(A, B), C),
     LHS_Join = RHS_Join,
 
-    %% a ∧ (b ∧ c) = (a ∧ b) ∧ c.
+    %% a ∧ (b ∧ c) = (a ∧ b) ∧ c
     LHS_Meet = meet(A, meet(B, C)),
     RHS_Meet = meet(meet(A, B), C),
     LHS_Meet = RHS_Meet,
@@ -91,10 +91,10 @@ commutativity_1() ->
             commutativity_check(TypeA, TypeB)).
 
 commutativity_check(A, B) ->
-    %% a ∨ b = b ∨ a,
+    %% a ∨ b = b ∨ a
     true = join(A, B) =:= join(B, A),
 
-    %% a ∧ b = b ∧ a.
+    %% a ∧ b = b ∧ a
     true = meet(A, B) =:= meet(B, A),
 
     true.
@@ -106,10 +106,10 @@ idempotence_1() ->
     ?FORALL(Type, type(), idempotence_check(Type)).
 
 idempotence_check(Type) ->
-    %% a ∨ a = a,
+    %% a ∨ a = a
     Type = join(Type, Type),
 
-    %% a ∧ a = a.
+    %% a ∧ a = a
     Type = meet(Type, Type),
 
     true.
@@ -118,10 +118,10 @@ identity() ->
     ?FORALL(Type, type(), identity_check(Type)).
 
 identity_check(Type) ->
-    %% a ∨ [bottom element] = a,
+    %% a ∨ [bottom element] = a
     Type = join(Type, none),
 
-    %% a ∧ [top element] = a.
+    %% a ∧ [top element] = a
     Type = meet(Type, any),
 
     true.