Type checker for the simply typed lambda calculus
123456789101112131415
% 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.
Erlang
INFO