Simple gradual typechecker with parametricity & inference written in Prolog.

typechecker.pl

% begin

% --- typing environment ---
% empty context always fails on queries,
% that is, there are unbound variables...

% find :: env * var * type -> prop
find([ type(X, T) | _ ], X, T).

find([ _ | E ], X, T) :-
  find(E, X, T).

% --- typing relations ---
% casts are only allowed to concrete types
% type :: dynamic | unit | bool | nat
type(dynamic).
type(unit).
type(bool).
type(nat).

% this order implies type inference's result,
% so, the precendence is for identical types.
% used on subsumption/substituition of types.
% subtype :: type * type -> prop
subtype(arrow(A, B), arrow(C, D)) :-
  subtype(C, A),
  subtype(B, D).

subtype(T, T).

subtype(dynamic, _).

% supertype :: type * type -> prop
supertype(A, B) :-
  subtype(B, A).

% this doesn't imply type inference's result.
% used to compare types for proper explicit
% casts, otherwise, the cast is invalid, that
% is, only upcasts and dowcasts on dynamic
% type are allowed...
% equiv :: type * type -> prop
equiv(T, T).
equiv(dynamic, _).
equiv(_, dynamic).

% --- lambda terms ---
% nat :: zero | succ (nat)
nat(zero).
nat(succ(N)) :- nat(N).

% expr :: unit
%       | true
%       | false
%       | nat
%       | if (expr, expr, expr)
%       | cast (expr, type)
%       | var (X)
%       | abstr (X, expr)
%       | abstr (X, type, expr)
%       | appl (expr, expr)
%       | let (X, expr, expr)
%       | let (X, type, expr, expr)
expr(unit).
expr(true).
expr(false).
expr(N) :- nat(N).

expr(if(X, Y, Z)) :-
  expr(X), expr(Y), expr(Z).

expr(cast(X, _)) :-
  expr(X).

expr(var(_)).

expr(appl(M, N)) :-
  expr(M), expr(N).

expr(abstr(X, M)) :-
  expr(var(X)),
  expr(M).

expr(abstr(X, _, M)) :-
  expr(abstr(X, M)).

expr(let(X, M, N)) :-
  expr(var(X)),
  expr(M),
  expr(N).

expr(let(X, _, M, N)) :-
  expr(let(X, M, N)).

% --- "bidirectional" typechecker ---
% this is a subtle fact, but there's no such
% bidirectional typechecker algorithm written
% in logic programming languages, so, in some
% way, it's a kind of design pattern on FP to
% fake some Logic Programming properties...
% also, typing rules from Type Theory map (near)
% one-to-one in Logic Programming clauses...

% Γ ⊢ M:α → β
% Γ ⊢ N:γ    γ ≤ α
% —————————————————
% Γ ⊢ (M N):β
infer(E, appl(M, N), B) :-
  expr(appl(M, N)),
  infer(E, M, arrow(A, B)),
  infer(E, N, C),
  subtype(A, C).

% Γ, x:α ⊢ •
% ———————————
% Γ ⊢ x:α
infer(E, var(X), A) :-
  expr(var(X)),
  find(E, X, A).

% Γ, x:α ⊢ M:β
% ———————————————————
% Γ ⊢ (λx:α.M):α → β
infer(E, abstr(X, M), arrow(A, B)) :-
  expr(abstr(X, M)),
  infer([ type(X, A) | E ], M, B).

infer(E, abstr(X, T, M), arrow(T, A)) :-
  expr(abstr(X, T, M)),
  infer(E, abstr(X, M), arrow(T, A)).

% Γ ⊢ M:β    Γ, x:β ⊢ N:α
% ————————————————————————
% Γ ⊢ (let x:β = M in N):α
infer(E, let(X, M, N), A) :-
  expr(let(X, M, N)),
  infer(E, M, B),
  infer([ type(X, B) | E ], N, A).

% Γ ⊢ M:β    Γ, x:τ ⊢ N:α
% β ≤ τ
% —————————————————————————
% Γ ⊢ (let x:τ = M in N):α
infer(E, let(X, T, M, N), A) :-
  expr(let(X, T, M, N)),
  infer(E, M, B),
  subtype(T, B),
  infer([ type(X, T) | E ], N, A).

% Γ ⊢ M:α    α ~ τ
% —————————————————
% Γ ⊢ (M as τ):τ
infer(E, cast(M, T), T) :-
  expr(cast(M, T)),
  type(T),
  infer(E, M, A),
  equiv(A, T).

% Γ ⊢ M:bool    Γ ⊢ N:β
% Γ ⊢ O:γ    β ≤ α    γ ≤ α
% ———————————————————————————
% Γ ⊢ (if M then N else O):α
infer(E, if(M, N, O), A) :-
  expr(if(M, N, O)),
  check(E, M, bool),
  infer(E, N, B),
  infer(E, O, C),
  subtype(A, B),
  subtype(A, C).

% --- axioms ---
%
%
% —————————————
% Γ ⊢ unit:unit
infer(_, unit, unit).

% ——————————————
% Γ ⊢ true:bool
infer(_, true, bool).

% ———————————————
% Γ ⊢ false:bool
infer(_, false, bool).

% ——————————
% Γ ⊢ 0:nat
%
% —————————————————————
% Γ, n:nat ⊢ (n+1):nat
infer(_, N, nat) :-
  nat(N).

% aliases
check(E, X, T) :-
  infer(E, X, T).

infer(X, T) :-
  infer([ ], X, T).

check(X, T) :-
  check([ ], X, T).

% end