Maps and opaque types

map_adt.erl

-module(map_adt).

-compile(export_all).

-export_type([t/0, t/1, m/0, s/1, sm/1]).

-opaque t()    :: #{atom() => integer()}.

-opaque t(A)   :: #{A => integer()}.

-opaque m()    :: #{t() => integer()}.

-type   mt()   :: #{t() => integer()}.

-opaque s(K)   :: #{K => integer(), integer() => atom()}.

-opaque sm(K)  :: #{K := integer(), integer() := atom()}.

-type   smt(K) :: #{K := integer(), integer() := atom()}.

-spec t0() -> t().

t0() ->
    #{}.

-spec t1() -> t(integer()).

t1() ->
    #{3 => 1}.

-spec m0() -> m().

m0() ->
    #{#{} => 3}.

-spec mt0() -> mt().

mt0() ->
    #{#{} => 3}.

-spec s0() -> s(atom()).
s0() -> #{}.

-spec s1() -> s(atom()). %% No contract breakage (bad warning)
s1() -> #{3 => a}.

-spec s2() -> s(atom() | 3).
s2() -> #{3 => a}. %% Contract breakage

-spec s3() -> s(atom() | 3).
s3() -> #{3 => 5, a => 6, 7 => 8}.

-spec s4() -> s(integer()).
s4() -> #{1 => a}. %% Actual contract breakage (good warning)

-spec s5() -> s(1).
s5() -> #{2 => 3}. %% Contract breakage (not found)

-spec s6() -> s(1).
s6() -> #{1 => 3}.

-spec s7() -> s(integer()).
s7() -> #{1 => 3}.

-spec sm1() -> sm(1). %% No contract breakage (bad warning)
sm1() -> #{1 => 2, 3 => a}.

-spec smt1() -> smt(1).
smt1() -> #{3 => a}. %% Contract breakage

-spec smt2() -> smt(1).
smt2() -> #{1 => a}.  %% Contract breakage

-spec smt3() -> smt(1).
smt3() -> #{1 => 1}. %% Slight contract breakage (probably requires better map type)

-spec smt4() -> smt(1).
smt4() -> #{1 => 2, 3 => a}.

map_use.erl

-module(map_use).

-compile(export_all).

-export_type([t/0, t/1]).

-opaque t()  :: #{atom() => integer()}.

-opaque t(A) :: #{A => integer()}.

tt1() ->
    A = t0(),
    B = t1(),
    A =:= B. % never 'true'

-spec t0() -> t().

t0() ->
    #{a => 1}.

-spec t1() -> t(integer()).

t1() ->
    #{3 => 1}.

adt_tt1() ->
    A = adt_t0(),
    B = adt_t1(),
    A =:= B. % opaque attempt

adt_tt2() ->
    A = adt_t0(),
    B = adt_t1(),
    #{A => 1
     ,B => 2 % opaque attempt
     }.

adt_tt3() ->
    A = adt_t0(),
    #{A => 1}. %% Should we warn here?

adt_mm1() ->
    A = adt_t0(),
    M = adt_m0(),
    #{A := R} = M, % opaque attempt
    R.

%% adt_ms1() ->
%%     A = adt_t0(),
%%     M = adt_m0(),
%%     M#{A}. % opaque attempt

adt_mu1() ->
    A = adt_t0(),
    M = adt_m0(),
    M#{A := 4}. % opaque attempt

adt_mtm1() ->
    A = adt_t0(),
    M = adt_mt0(),
    #{A := R} = M, % opaque attempt
    R.

%% adt_mts1() ->
%%     A = adt_t0(),
%%     M = adt_mt0(),
%%     M#{A}. % opaque attempt

adt_mtu1() ->
    A = adt_t0(),
    M = adt_mt0(),
    M#{A := 4}. % opaque attempt

adt_t0() ->
    map_adt:t0().

adt_t1() ->
    map_adt:t1().

adt_m0() ->
    map_adt:m0().

adt_mt0() ->
    map_adt:mt0().