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).

Hi,

It looks like there is a bug with the compiler's handling of combined higher-order types and insts which causes it to lose track of the inst of F at line 45. We will need to take a look at that. Writing this the more old fashioned (albeit verbose) way, using separate insts will work:

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

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

:- inst term for term/0
   ---> lam(pred(in(term), out(term)) is det)
   ;    pi(term, pred(in(term), out(term)) is det)
   ;    appl(term, term)
   ;    ann(term, term)
   ;    free_var(ground)
   ;    star
   ;    box.

:- pred unfurl(int, pred(term,term), term) .
:- mode unfurl(in, in(pred(in(term), out(term)) is det), out(term)) 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(term), out(term)) is det), in(pred(in(term), out(term)) is det), out(term), out(term)) 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(term),out(term)) 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(term), string::out) is det.

print_term(Lvl, lam(F), R) :-
    plunge(Lvl, F, Plunged),
    string.format("(λ%s)", [s(Plunged)], R).
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), term::out(term)) is det.

eval(lam(F), lam(pred(N::in(term), R::out(term)) 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(term), R::out(term)) 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 instead of predicates in the definition of the term/0 type would also work, for example:

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

Indeed, because Mercury treats higher-order terms involving the standard function mode (e.g. f(in,...) = out) specially,
this is probably the more concise approach.

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).