Regarding the code in question, it is possible to write it a bit more elegantly and more compactly, with a combination of techniques. For example, let's consider this snippet from lines 110 to 119:
type(Ctx, case(T0, {z, Tz}, {s(V), Ts}), Ty) :- !,
isvar(V),
type(Ctx, T0, nat),
type(Ctx, Tz, Ty),
CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
type(Ctx, case(T0, {inl(Vl), Tl}, {inr(Vr), Tr}), Ty) :- !,
isvar(Vl), isvar(Vr),
type(Ctx, T0, uni(Ty1, Ty2)),
Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).
It is clear that the two clauses are mutually exclusive if the second argument is known, because they differ in various terms already in the head. For instance, {z, Tz} is clearly different from {inl(Vl), Tl}. A Prolog system with
deep indexing, which is also used by Mercury, can detect this, and in such a system, we can therefore remove the two occurrences of !/0 in the code, yielding a more general and shorter version:
type(Ctx, case(T0, {z, Tz}, {s(V), Ts}), Ty) :-
isvar(V),
type(Ctx, T0, nat),
type(Ctx, Tz, Ty),
CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
type(Ctx, case(T0, {inl(Vl), Tl}, {inr(Vr), Tr}), Ty) :-
isvar(Vl), isvar(Vr),
type(Ctx, T0, uni(Ty1, Ty2)),
Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).
The isvar/1 tests can be removed if we use a better representation of our data. For instance, if we use the wrapper v/1 to denote variables in the data, we can replace these clauses by:
type(Ctx, case(T0, {z, Tz}, {s(v(V)), Ts}), Ty) :-
type(Ctx, T0, nat),
type(Ctx, Tz, Ty),
CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
type(Ctx, case(T0, {inl(v(Vl)), Tl}, {inr(v(Vr)), Tr}), Ty) :-
type(Ctx, T0, uni(Ty1, Ty2)),
Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).
Finally, the variables CtxS, Ctx1 and Ctx2 are only used once each, so we can simply write:
type(Ctx, case(T0, {z, Tz}, {s(v(V)), Ts}), Ty) :-
type(Ctx, T0, nat),
type(Ctx, Tz, Ty),
type([{V, nat} | Ctx], Ts, Ty).
type(Ctx, case(T0, {inl(v(Vl)), Tl}, {inr(v(Vr)), Tr}), Ty) :-
type(Ctx, T0, uni(Ty1, Ty2)),
type([{Vl, Ty1} | Ctx], Tl, Ty),
type([{Vr, Ty2} | Ctx], Tr, Ty).
With the necessary provisions in place, it may be possible to shorten it further, by generating such code automatically from more declarative descriptions, using a mechanism called
term expansion which is available in most Prolog systems. It is analogous to what other languages such as Rust call
macros.