[m-users.] How to decompose a term with a variable data constructor

[Zoltan Somogyi]

On Mon, 01 Nov 2021 18:29:23 +0100, Volker Wysk <post at volker-wysk.de> wrote:

> Hi.
> 
> I have a simple term type, like this:
> 
> :- type tterm
>    ---> thema(string)
>    ;    und(tterm, tterm)
>    ;    oder(tterm, tterm).
> 
> Now I want to decompose such a term:
> 
> Konstr(T1, T2) = und(thema("aaa"), thema("bbb"))
> 
> Konstr is a ground variable, which has been passed as an input argument to
> my predicate. T1 and T2 are free variables. My idea was that the above
> statement should succeed if Konstr is "und", and fail otherwise.

It seems you want Konstr to be a sort-of disembodied function symbol,
with no fixed arity, and able to be applied to an arbitrary number of arguments.
There is no such construct in Mercury.

> This would
> mean to pass "und" to the predicate as a function of type (func(tterm,tterm)
> = tterm). But this won't work.

No, it won't. Your diagnosis of the reason why it wouldn't, i.e. ...

> I realize that the compiler can't unify a function call with a discriminated
> union. This would mean to calculate the function backwards - the arguments
> from the result.

... is correct.

> Now, my question is: How can you decompose a discriminated union when the
> data constructor isn't known at compile time? Something like
> 
> Constr(T1, T2) = und(thema("aaa"), thema("bbb"))
> 
> which would result in 
> 
> Constr = und,        % ???
> T1 = thema("aaa"), 
> T2 = thema("bbb")

If you want to preserve static typing, you would need another type,
such as this:

:- type tterm_functor
   ---> thema_f
   ;      und_f
   ;      oder_f.

You could then write something like

ConstrF = und_f, Constr = und(thema("aaa"), thema("bbb"))

This would separate ConstrF, which says which function symbol you want
for the term you want to construct, from Constr, which would then hold that term.

If that approach does not work for you, you could consider the deconstruct
predicate from the deconstruct module of the standard library, but that
predicate and its friends work on univs, which means that typeckecking
would be done partially at runtime.

In our experience, the approach using static typing is better in pretty much
all cases where it is actually applicable. The approach that defers typechecking
partially to runtime should be used only if there is no other choice.

Zoltan.