Type inference can be easy too, here is a 5mn Prolog thing:
type(X,_,number) :- number(X).
type(V,Env,T) :-
ground(V),
member(V:T,Env).
type(<(X,Y),Env,bool) :-
type(X,Env,number),
type(Y,Env,number).
type(or(A,B),Env,bool) :-
type(A,Env,bool),
type(B,Env,bool).
type(lambda(X,E),Env,XT -> ET) :-
type(E,[X:XT|Env],ET).
type(apply(F,E),Env,T) :-
type(E,Env,ET),
type(F,Env,ET->T).
type(let(X,XE,E),Env,ET) :-
type(XE,Env,XT),
type(E,[X:XT|Env],ET).
For example:
?- type(lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),[],T).
T = ((_232 -> _226) -> (_225 -> _232) -> _225 -> _226)
