hindley-milner-clean.pl

:- op(350, yfx, @).

:- set_prolog_flag(occurs_check, error).

:- det(inference/3).

inference(true, bool, _).

inference(false, bool, _).

inference(nat(N), nat, _) :- integer(N), N >= 0.

inference(A+B, nat, Tcx) :-
    inference(A, nat, Tcx),
    inference(B, nat, Tcx).

inference(var(X), Ty, Tcx) :-
    memberchk(X-ForallTy, Tcx),
    instantiation(Ty, ForallTy).

inference(Param->Body, ParamTy->BodyTy, Tcx) :-
    ExtTcx = [Param-forall([], ParamTy) | Tcx],
    inference(Body, BodyTy, ExtTcx).

inference(Fn@Arg, RetTy, Tcx) :-
    inference(Fn, FnTy, Tcx), % nat->bool
    inference(Arg, ArgTy, Tcx), % nat
    FnTy = (ArgTy->RetTy). % nat->bool = (nat->RetTy)

inference(let(X, Expr, Body), BodyTy, Tcx) :-
    inference(Expr, ExprTy, Tcx),
    generalization(ExprForallTy, ExprTy, Tcx),
    ExtTcx = [X-ExprForallTy | Tcx],
    inference(Body, BodyTy, ExtTcx).


instantiation(SimpleTy, forall(Vs, SimpleTy0)) :-
    copy_term(Vs, SimpleTy0, _FreshVs, SimpleTy).


% let id = x -> var(x) in pair(var(id)@nat(123), var(id)@true).
% id : A->A ==> forall([A], A->A)
generalization(forall(Vs, SimpleTy), SimpleTy, Tcx) :-
    term_variables(SimpleTy, TyVs),
    term_variables(Tcx, TcxVs),
    include({TcxVs}/[V]>>(
        maplist(\==(V), TcxVs)
    ), TyVs, Vs).


ex(
    (f ->
        let(f_copy, var(f),
            var(f_copy) @ true
        )
        % var(f) @ true
    )
        @ (x -> var(x) + var(x))
).