A simple example of type inference in Prolog using Constraint Handling Rules

type_inference.pl

:- initialization(main).
:- set_prolog_flag('double_quotes','chars'). ;this is for SWI-Prolog
:- use_module(library(chr)).
:- chr_constraint type/2.
type(A,B) \ type(A,B) <=> true.
type((A;B),C) ==> C = bool,type(A,bool),type(B,bool).
type((A,B),C) ==> C = bool,type(A,bool),type(B,bool).
type(A>B,C) ==> C = bool,type(A,number),type(B,number).
type(A<B,C) ==> C = bool,type(A,number),type(B,number).
type(A+B,C) ==> C = number,type(A,number),type(B,number).
type(A-B,C) ==> C = number,type(A,number),type(B,number).
type(A*B,C) ==> C = number,type(A,number),type(B,number).
type(A/B,C) ==> C = number,type(A,number),type(B,number).
type(append(A,B,C))
type(A is B,C) ==> C = number,type(A,number),type(B,number).
type(A = B,C) ==> type(A,C),type(B,C).
type(A \= B,C) ==> type(A,C),type(B,C).
type(append(A,B,C))
type(true,bool).
type(false,bool).
type(A,B) ==> number(A) | B=number.

main :- type((B>D),C),writeln(C).