Type checker for the simply typed lambda calculus

% escript will ignore the first line

typeof({var, Name},                G) -> maps:get(Name, G);
typeof({abs, Param, ParamT, Body}, G) -> {ParamT, '->', typeof(Body, maps:put(Param, ParamT, G))};
typeof({app, Callee, Arg},         G) -> ArgT = typeof(Arg, G), {ArgT, '->', R} = typeof(Callee, G), R.

example(E, G) ->
    io:format("~p : ~p~n", [E, typeof(E, G)]).

main(_) ->
    example({var, "x"}, #{"x" => bool}),
    example({app, {var, "f"}, {var, "x"}}, #{"f" => {bool, '->', int}, "x" => bool}),
    example({abs, "x", int, {var, "x"}}, #{}),
    example({app, {abs, "x", int, {var, "x"}}, {var, "x"}}, #{"x" => int}),
    ok.