Prologの練習です。
以下で定義される簡単な式の型を推論し、その値を評価します。

* 数値はint型
* t, nilはbool型
* XがT型、YがU型のとき、ペアX & YはT & U型
* FがT -> U型、XがT型のとき、関数適用F $ XはU型

組み込み関数はadd, eq, and, neg, car, cdr, identity, applyの8種類を用意しました。

変数とかは使えないただの型推論器もどきのようなものですが、この程度であればPrologなら非常に簡単に作ることができます。

実際に実行してみると、以下のような感じで式の型と実行結果を評価することができます。

?- [types].
true.

?- eval(3, T, R). % eval(式, 型, 評価結果)
T = int,
R = 3.

?- eval(car $ 3 & t, T, R).
T = int,
R = 3.

?- add $ 2 :: T.
T = int->int.

?- (add $ 2) $ 3 :: T.
T = int.

?- eval((add $ 2) $ 3, T, R).
T = int,
R = 5.

以下ソースコード

% types.pl

:- op(400, xfy, [&]).
:- op(500, xfy, [$]).
:- op(600, xfy, [->]).
:- op(900, xfx, [::]).

% type(T): T は型である
% プリミティブな型は int, bool のみ
type(int).
type(bool).
% T & U で T と U の直積を表す
type(T & U) :-
    type(T),
    type(U).
% T -> U で T を取って U を返す関数を表す
type(T -> U) :-
    type(T),
    type(U).

% 式の型
:- discontiguous (::)/2.
% 数値は int 型
X :: int :-
    number(X).
% t, nil は bool 型
t :: bool.
nil :: bool.
% F :: T -> U と X :: T について、関数適用 F $ X は U 型
F $ X :: U :-
    F :: T -> U,
              X :: T.
% X :: T と Y :: U について、ペア X & Y は T & U 型
X & Y :: T & U :-
    X :: T,
    Y :: U.

% 式の評価
eval(E, T, Res) :-
    E :: T,
    eval_(E, Res),
    !.

:- discontiguous eval_/2.

% プリミティブな値の評価
eval_(X, Res) :-
    number(X),
    Res is X.
eval_(t, t).

% ペア
eval_(nil, nil).
eval_(X & Y, Res) :-
    eval_(X, XRes),
    eval_(Y, YRes),
    Res = XRes & YRes.

% 関数適用の評価方法は後で

% 関数
add :: int -> int -> int.
eval_((add $ X) $ Y, Res) :-
    eval_(X, XRes),
    eval_(Y, YRes),
    Res is XRes + YRes.

eq :: T -> T -> bool :-
    comparable(T).
% comparable(T): T は同値比較可能な型である。
comparable(int).
comparable(bool).
comparable(T & U) :-
    comparable(T),
    comparable(U).
eval_((eq $ X) $ Y, Res) :-
    eval_(X, XRes),
    eval_(Y, YRes),
    eq_value(XRes, YRes, Res).
eq_value(X, Y, t) :-
    number(X),
    number(Y),
    X is Y,
    !.
eq_value(t, t, t) :- !.
eq_value(nil, nil, t) :- !.
eq_value(X & Y, A & B, t) :-
    eq_value(X, A),
    eq_value(Y, B),
    !.
eq_value(_, _, nil) :- !.

and :: bool -> bool -> bool.
eval_((and $ X) $ Y, t) :-
    eval_(X, t),
    eval_(Y, t).
eval_((and $ X) $ Y, nil) :-
    not(eval_((and $ X) $ Y, t)).

neg :: bool -> bool.
eval_(neg $ t, nil).
eval_(neg $ nil, t).

car :: T & U -> T.
eval_(car $ X & _, Res) :-
    eval_(X, Res).

cdr :: T & U -> U.
eval_(cdr $ _ & Y, Res) :-
    eval_(Y, Res).

identity :: T -> T.
eval_(identity $ X, Res) :-
    eval_(X, Res).

apply :: (T -> U) -> T -> U.
eval_((apply $ F) $ X, Res) :-
    eval_(F, FRes),
    eval_(X, XRes),
    eval_(FRes $ XRes, Res).