Inferencia de tipos en Prolog

type_inference_prolog

type_of(_, true, bool).
type_of(_, false, bool).
type_of(_, X, num) :- integer(X).
type_of(_, "s1", str).
type_of(_, "s2", str).
type_of(_, "s3", str).
type_of(G, X, Y) :- nonvar(X), has_type(G, X, Y).

has_type([[X, Y]|_], X, Y).
has_type([_|T],      X, Y) :- has_type(T, X, Y).

% Operaciones sobre booleanos
type_of(G, and(X,Y), bool) :- type_of(G, X, bool), type_of(G, Y, bool).
type_of(G, or(X,Y), bool)  :- type_of(G, X, bool), type_of(G, Y, bool).
type_of(G, zero(X), bool)  :- type_of(G, X, num).

% Operaciones sobre numeros
type_of(G, sum(X,Y), num) :- type_of(G, X, num), type_of(G, Y, num).
type_of(G, sub(X,Y), num) :- type_of(G, X, num), type_of(G, Y, num).
type_of(G, mul(X,Y), num) :- type_of(G, X, num), type_of(G, Y, num).
type_of(G, div(X,Y), num) :- type_of(G, X, num), type_of(G, Y, num).

% Operaciones sobre strings
type_of(G, length(X), num) :- type_of(G, X, str).

% Construcciones del lenguaje
type_of(G, if(X,Y,Z), W) :- type_of(G, X, bool),
                            type_of(G, Y, W),
                            type_of(G, Z, W).

type_of(_, fun(P, TP, TB, _), flecha(TP, TB)) :- nonvar(P).

type_of(G, app(fun(P,TP,TB,B), E), TB) :- ...

% Ejemplos
% type_of([], if(zero(2), 3, 4), num).
% type_of([], fun(p,num,num,sum(p,p)), num).
% type_of([[p,str]], fun(p,str,num,sum(length(p), length(p))), num).
% type_of([], app(fun(p,str,num,sum(length(p),length(p))), "s2"), num).