Attempt of Calculus of Constructions in Mercury

mercoc-fn.m

% Mercoc: Calculus of Constructions in Mercury
% Attempt to rewrite https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 in Mercury

% Alternative approach using functions instead of predicates

:- module mercoc.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module list, string, int, bool.

:- type term
   ---> lam(func(term)= term)
   ;    pi(term, func(term)= term)
   ;    appl(term, term)
   ;    ann(term, term)
   ;    free_var(int)
   ;    star
   ;    box.

:- func unfurl(int, func(term)=term)= term .
unfurl(Lvl, F) = F(free_var(Lvl)).

:- pred unfurl2(int, func(term)=term,func(term)=term, term, term) .
:- mode unfurl2(in, in, in, out, out) is det.
unfurl2(Lvl, F, G, Term1, Term2) :- unfurl(Lvl, F)= Term1, unfurl(Lvl, G)=Term2.

:- pred plunge(int, func(term)= term, string).
:- mode plunge(in, in, out) is det.
plunge(Lvl, F, R) :- 
    L1 = Lvl + 1, unfurl(Lvl, F)=Q, print_term(L1, Q, R).

:- pred print_term(int::in, term::in, string::out).
print_term(Lvl, lam(F), R) :-
    string.format("(λ%s)", [s(Plunged)], R),
    plunge(Lvl, F,Plunged).
print_term(Lvl, pi(A, F), R) :-
    string.format("(Π%s.%s)", [s(PArg), s(PlungedF)], R),
    plunge(Lvl, F, PlungedF), print_term(Lvl, A, PArg).
print_term(Lvl, appl(M,N), R) :-
    string.format("(%s %s)", [s(PM), s(PN)], R),
    print_term(Lvl, M, PM), print_term(Lvl, N, PN).
print_term(Lvl, ann(M, A), R) :-
    string.format("(%s : %s)", [s(PM), s(PA)], R),
    print_term(Lvl, M, PM), print_term(Lvl, A, PA).
print_term(_, star, "*").
print_term(_, box, "☐").
print_term(_, free_var(N), R) :- string.format("%d", [i(N)],R).

:- func print_term(int, term) = string.
print_term(Lvl, T) = R :- print_term(Lvl, T, R).

:- pred eval(term::in, term:: out) is det.
eval(lam(F), lam(func(N)= R :- (F(N)=N1, eval(N1,R)))).
eval(free_var(X), free_var(X)).
eval(star,star).
eval(box,box).
eval(appl(M,N), Res) :-
    eval(M, Me), eval(N, Ne),
    (lam(F) = Me -> F(Ne)=Res; Res = appl(Me,Ne)).
eval(ann(M, _), R) :- eval(M,R).
eval(pi(A,F),pi(Ra, Rf)) :-
    eval(A, Ra),
    (Rf = (func(N)=R :- F(N)=FF, eval( FF, R))).


:- pred plunge_eq(int, func(term)=term,func(term)=term) .
:- mode plunge_eq(in, in, in).
plunge_eq(Lvl, F, G) :- equate(Lvl + 1, Fa, Ga), unfurl2(Lvl, F, G, Fa, Ga).

:- pred equate(int::in, term::in, term::in) is semidet.
equate(Lvl, lam(F), lam(G)) :- plunge_eq(Lvl, F, G).
equate(Lvl, pi(A1, F), pi(B1, G)) :-  equate(Lvl, A1, B1), plunge_eq(Lvl, F, G).
equate(Lvl, appl(M,N), appl(M1,N1)) :- equate(Lvl, M, M1), equate(Lvl, N, N1).
equate(Lvl, ann(M, A), ann(M1, A1)) :- equate(Lvl, M, M1), equate(Lvl, A, A1).
equate(_, star, star).
equate(_, box, box).
equate(_, free_var(N), free_var(N)).

:- func equate_dec(int, term, term) = bool.
equate_dec(Lvl, A, B) = R :- (equate(Lvl, A, B) -> R = yes; R = no).

% panic

% todo + error handling
:- pred infer_ty(int::in, list(term)::in, term::in, term::out) is semidet.
infer_ty(Lvl, Ctx, pi(A,F), Res) :-
    infer_sort(Lvl, Ctx, A, _), infer_sort(Lvl+1, [ EvaledA |Ctx], UnfurledF, Res),
    eval(A, EvaledA), unfurl(Lvl, F)= UnfurledF.
infer_ty(Lvl, Ctx, appl(M,N), Res) :-
    infer_ty(Lvl, Ctx, M, pi(A,F)), check_ty(Lvl, Ctx, N, A), F(N)= Res.
infer_ty(Lvl, Ctx, ann(M,A), Ea) :-
    infer_sort(Lvl, Ctx, M, A), eval(A, Ea), check_ty(Lvl, Ctx, M, Ea).
infer_ty(Lvl, Ctx, free_var(X), Res) :-
    Ind = (Lvl -X -1), list.index0(Ctx, Ind,Res).
infer_ty(_,_, star, box).

% todo err handling
:- pred infer_sort(int::in, list(term)::in, term::in, term::out) is semidet.
infer_sort(Lvl, Ctx, Term, Out) :-
    infer_ty(Lvl, Ctx, Term, Out), (Out = star; Out = box). 
% todo err handling

:- pred check_ty(int::in, list(term)::in, term::in, term::in) is semidet.
check_ty(Lvl, Ctx, lam(F), pi(A,G)) :-
    check_ty(Lvl+1, [A | Ctx], UF, UG), unfurl2(Lvl, F, G, UF, UG).
check_ty(Lvl,Ctx, T,Ty) :- 
    T = lam(_) -> fail; infer_ty(Lvl, Ctx, T, Inferred), equate(Lvl, Ty, Inferred).

%%%%%%%%%% usage
:- func curry1(func(term)=term)= term.
curry1(F) = lam(F).
:- func curry2(func(term,term)=term)=term.
curry2(F) = lam(func(X) = curry1(func(Y) = F(X,Y))).
:- func curry3(func(term,term,term)=term)=term.
curry3(F) = lam(func(X) = curry2(func(A,B) = F(X,A,B))).

% TODO: finish example usage section

main(!IO) :-
    D0 = lam(func(X)=X),
    D = appl(D0, box),
    (infer_ty(0, [],pi(star,func(DD)=DD),Qdd) -> Q=Qdd; Q=box),
    (infer_ty(0, [],D1,Q1q) -> Q1=Q1q; Q1=star),
    eval((D),D1),
        E = pi(star, func(AAA)=AAA),
        io.format("Hello, world %s %s %s!\n", [s(print_term(0, D)),s(print_term(0, D1)), s(print_term(0,E))], !IO),
        io.format("EE %s %s\n", [s(print_term(0,Q)),s(print_term(0,Q1))],!IO),
    io.write_string("Hello, world %v!\n", !IO).

mercoc.m

% Mercoc: Calculus of Constructions in Mercury
% Attempt to rewrite https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 in Mercury

% Compilation fails
% $ mmc --make mercoc
% Making Mercury/cs/mercoc.c
% mercoc.m:045: In clause for `print_term(in, in, out)':
% mercoc.m:045:   in argument 2 of call to predicate `mercoc.plunge'/3:
% mercoc.m:045:   mode error: variable `F' has instantiatedness `ground',
% mercoc.m:045:   expected instantiatedness was `(pred(in, out) is det)'.
% ** Error making `Mercury/cs/mercoc.c'.

:- module mercoc.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module list, string, int.

:- type term
   ---> lam(pred(term::in, term::out) is det)
   ;    pi(term, pred(term::in, term::out) is det)
   ;    appl(term, term)
   ;    ann(term, term)
   ;    free_var(int)
   ;    star
   ;    box.

:- pred unfurl(int, pred(term,term), term) .
:- mode unfurl(in, in(pred(in, out) is det), out) is det.
unfurl(Lvl, F, Term) :- F(free_var(Lvl), Term).

:- pred unfurl2(int, pred(term,term),pred(term,term), term, term) .
:- mode unfurl2(in, in(pred(in, out) is det), in(pred(in, out) is det), out, out) is det.
unfurl2(Lvl, F, G, Term1, Term2) :- unfurl(Lvl, F, Term1), unfurl(Lvl, G, Term2).

:- pred plunge(int, pred(term, term), string).
:- mode plunge(in, in(pred(in,out) is det), out) is det.
plunge(Lvl, F, R) :- 
    L1 = Lvl + 1, print_term(L1, Q, R), unfurl(Lvl,F,Q).

:- pred print_term(int::in, term::in, string::out).
print_term(Lvl, lam(F), R) :-
    string.format("(λ%s)", [s(Plunged)], R),
    plunge(Lvl, F,Plunged).
print_term(Lvl, pi(A, F), R) :-
    string.format("(Π%s.%s)", [s(PArg), s(PlungedF)], R),
    plunge(Lvl, F, PlungedF), print_term(Lvl, A, PArg).
print_term(Lvl, appl(M,N), R) :-
    string.format("(%s %s)", [s(PM), s(PN)], R),
    print_term(Lvl, M, PM), print_term(Lvl, N, PN).
print_term(Lvl, ann(M, A), R) :-
    string.format("(%s : %s)", [s(PM), s(PA)], R),
    print_term(Lvl, M, PM), print_term(Lvl, A, PA).
print_term(_, star, "*").
print_term(_, box, "☐").
print_term(_, free_var(N), R) :- string.format("%d", [i(N)],R).

:- pred eval(term::in, term:: out) is det.
eval(lam(F), lam(pred(N::in, R::out) is det :- (F(N,N1), eval(N1,R)))).
eval(free_var(X), free_var(X)).
eval(star,star).
eval(box,box).
eval(appl(M,N), Res) :-
    eval(M, Me), eval(N, Ne),
    (lam(F) = Me -> F(Ne,Res); Res = appl(Me,Ne)).
eval(ann(M, _), R) :- eval(M,R).
eval(pi(A,F),pi(Ra, Rf)) :-
    eval(A, Ra),
    (Rf = (pred(N::in, R::out) is det :- F(N,FF), eval( FF, R))).


main(!IO) :-
    D = lam(pred(X::in,X::out) is det),
    eval(appl(D, box),D1),
        E = pi(star, pred(X::in,X::out) is det),
        io.format("Hello, world %s %s %s!\n", [s(string(D)),s(string(D1)), s(string(E))], !IO),
    io.write_string("Hello, world %v!\n", !IO).

Using functions is the best approach here, I agree.
Thanks for helping me here, and thanks for developing Mercury itself!

There's also another workaround. It's bad, I'm posting it here in case it helps to identify the root cause of the bug:
you can wrap F into pred(X, Y) :- F(X, Y), like this:

print_term(Lvl, lam(F), R) :-
    string.format("(λ%s)", [s(Plunged)], R),
    NewF = (pred(X::in, Y::out) is det :- F(X, Y)),
    plunge(Lvl, NewF,Plunged).