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

[Volker Wysk]

Am Dienstag, dem 02.11.2021 um 04:45 +1100 schrieb 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.

I've come up with a different solution. For every constructor I have a 
construction function and a deconstruction predicate:

:- pred und_deconstruct(tterm::in, tterm::out, tterm::out) is semidet.
und_deconstruct(und(T1,T2), T1, T2).

:- func und_construct(tterm, tterm) = tterm.
func(T1, T2) = und(T1,T2).

... same for oder/2 ...

Now my predicates can be passed one or both of those (as needed). So they
can (de)construct terms without needing to know the the constructor/functor
at compile time.

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

That doesn't surprise me at all...

Thanks for the explanation.


Cheers,
Volker
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.mercurylang.org/archives/users/attachments/20211102/1c34b9b6/attachment.sig>