[m-users.] Using type constructors in predicate heads

[Julien Fischer]

Hi Sean,

On Sun, 7 Nov 2021, Sean Charles (emacstheviking) wrote:

> I made your suggested change, it works fine but… can I push it a
> little further? I went back to the Mercury crash course page as it
> mentioned non_empty_list, I found no references in the reference guide
> or the library but plenty in the source code for my ROTD version… but
> I am unsure of the syntax, if possible, of stating that the the list
> of terms to the sexp() functor is guaranteed to be non empty because:
> 
>     ( if Term = sexp(_, [ tk(_,F) | _ ]) then
> 
> already established that fact prior to the call…but this leads me to
> my final question: —should— I be doing this? I ask because
> 
> :- mode do_gencall(in, renderer, in(sexp), in, out) is det.
> do_gencall(_L, R, sexp(_, [Functor|Args]), !T) :-
> 
> This obv. fails because the unification into head and tail could fail,
> but if I declare it as semidet then obv. I have to check the call
> further up the code, again I totally understand why but my question
> then is, should I do this at all ? I have not used Haskell in a while
> now, plumping for Mercury, but I was getting reasonably proficient at
> the concept of `programming with types` and this feels similar. If I
> instructed the compiler that the mode was something like
> 
> :- mode do_gencall(in, renderer, in(sexp-with-non-empty-args), in, out) is det.
> 
> then presumably the predicate could remain as `det`, everybody is
> happy and my code feels more rigorous for it. I refer to the sample of
> code in the file ‘./mercury-srcdist-20.06.1/browser/parse.m’ , lines
> 305 to 307:
> 
> :- pred lexer_arg(list(char)::in(non_empty_list), list(token)::out) is det.
> 
> lexer_arg([Head | Tail], Toks) :-
> 
> This clearly shows to me that by using non_empty_list the compiler is
> happy to let me deconstruct the list in the clause head with no
> problems. I am not sure how to combine the mode you showed me with the
> addition of the non empty constraint as well that’s all!

As a separate named inst:

    :- inst sexp_with_non_empty_args for snode/0
        --->    sexp(ground, non_empty_list).

    :- mode do_gencall(in, renderer, in(sexp_with_non_empty_args),
       in, out) is det.

or inline:

    :- mode do_gencall(in, renderer, in(bound(sexp(ground, non_empty_list))),
       in, out) is det.

Julien