[m-users.] Some help with understanding the mode system?

[Volker Wysk]

Hi, Anders

Let's shrink your program to this:

:- module ground_free_branches_error_1.
:- interface.

:- type t ---> a; b.

:- pred p(t,t).
:- mode p(in,out) is multi.

:- implementation.

p(a, _).
%p(_, b).

I find three errors in this code. 

1. The second argument of p is declared to be an output variable. That means
it must be bound. But the above code, it's free. 

2. When you add the clause "p(_, b)" to the above, shrinked version, you get
the message which you're mentioned. That's because the instantiatedness of
the variables in a disjunction must match between the branches. (The two
clauses are a disjunction.) I wouldn't make sense to have two branches with
different instantiations, because the mode predefines the one and only mode
of the argument.

3. The compiler doesn't enumerate the constructors of a data type and bind
them to a free variable. You have to explicitly bind all the constructors
when you want that.

Here's an improved version the implementation section:

:- implementation.

:- pred any_of_t(t::out) is multi.
any_of_t(a). 
any_of_t(b). 

p(a, B) :- any_of_t(B).
p(_, b).

This compiles, except for there not being any main predicate.


Cheers,
Volker


Am Freitag, dem 28.06.2024 um 21:17 +0200 schrieb Anders Lundstedt:
> Dear all,
> 
> 
> I am struggling to understand the mode system. A MWE illustrating my problems
> is below. Any help would be much appreciated! In particular, I would appreciate
> pointers to relevant documentation, tutorials, et cetera. (I am new to Mercury
> but have some experience with Prolog.)
> 
> 
> MWE, with comments explaining my reasoning:
> 
> :- module ground_free_branches_error.
> 
> :- interface.
> 
> :- type t ---> a; b.
> 
> % implemented such that p(t₁,t₂) succeeds iff at least one of t₁ and t₂ unifies
> % with a
> :- pred p(t,t).
> 
> % for ground t₁ and t₂, p(t₂,t₂) succeeds iff a∈{t₁,t₂}
> % thus p(in,in) ought to be semidet:
> :- mode p(in,in) is semidet.
> 
> % for ground t₁ and free t₂, p(t₁,t₂) succeeds iff t₁ = a or t₂ unifies with a
> % thus p(in,out) ought to be multi:
> :- mode p(in,out) is multi.
> 
> % for reasons similar to the previous case, p(out,in) ought to be multi:
> :- mode p(out,in) is multi.
> 
> % for free t₁ and t₂, p(t₁,t₂) always succeeds, with solutions:
> % t₁ = a, t₂ = a
> % t₁ = a, t₂ = b
> % t₁ = b, t₂ = a
> % thus p(out,out) ought to be multi:
> :- mode p(out, out) is multi.
> 
> :- implementation.
> 
> p(a, _).
> p(_, b).
> 
> % everything works if I change the implementation to:
> %
> % p(a,a).
> % p(a,b).
> % p(b,a).
> %
> % in this case this is doable, but:
> % - if t had more constructors such a solution could become impractical
> % - it might be the case that if t is extended with more constructors:
> %   - the above working implementation might need to be updated, which is easy
> %     to forget; while
> %   - the implementation with wild cards might always work as intended when t
> %     is extended
> 
> 
> Compilation errors below. The compiler complains for all modes except p(in,in).
> I understand the error messages, but I cannot square them with my conclusions
> in the comments above.
> 
> ground_free_branches_error.m:032: In clause for `p(in, out)':
> ground_free_branches_error.m:032:   mode mismatch in disjunction.
> ground_free_branches_error.m:032:   The variable `HeadVar__2' is ground in some
> ground_free_branches_error.m:032:   branches but not others.
> ground_free_branches_error.m:031:     In this branch, `HeadVar__2' is free.
> ground_free_branches_error.m:032:     In this branch, `HeadVar__2' is ground.
> ground_free_branches_error.m:032: In clause for `p(out, in)':
> ground_free_branches_error.m:032:   mode mismatch in disjunction.
> ground_free_branches_error.m:032:   The variable `HeadVar__1' is ground in some
> ground_free_branches_error.m:032:   branches but not others.
> ground_free_branches_error.m:031:     In this branch, `HeadVar__1' is ground.
> ground_free_branches_error.m:032:     In this branch, `HeadVar__1' is free.
> ground_free_branches_error.m:032: In clause for `p(out, out)':
> ground_free_branches_error.m:032:   mode mismatch in disjunction.
> ground_free_branches_error.m:032:   The variable `HeadVar__1' is ground in some
> ground_free_branches_error.m:032:   branches but not others.
> ground_free_branches_error.m:031:     In this branch, `HeadVar__1' is ground.
> ground_free_branches_error.m:032:     In this branch, `HeadVar__1' is free.
> ground_free_branches_error.m:032:   The variable `HeadVar__2' is ground in some
> ground_free_branches_error.m:032:   branches but not others.
> ground_free_branches_error.m:031:     In this branch, `HeadVar__2' is free.
> ground_free_branches_error.m:032:     In this branch, `HeadVar__2' is ground.
> 
> 
> 
> Best,
> 
> Anders Lundstedt
> _______________________________________________
> users mailing list
> users at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/users