[m-users.] Existential higher-order type

[Julien Fischer]

On Tue, 11 Oct 2022, Volker Wysk wrote:

> Am Dienstag, dem 11.10.2022 um 21:49 +1100 schrieb Zoltan Somogyi:
>>
>> On Tue, 11 Oct 2022 12:38:18 +0200, Volker Wysk <post at volker-wysk.de> wrote:
>>> Am Dienstag, dem 11.10.2022 um 19:27 +1100 schrieb Mark Brown:
>>>> I assumed you _weren't_ doing that. I think the reference manual
>>>> leaves this behaviour unspecified if a det predicate has no outputs
>>>> (i.e., it doesn't require that the exception is thrown), so that would
>>>> mean your code doesn't say what you intend it to, or the reference
>>>> manual doesn't say what we intend it to. Either way, I'd avoid it
>>>> personally.
>>>
>>> Could someone who knows how it is, please clarify this?
>>>
>>> I thought the compiler would keep track of which parts can throw an
>>> exception. There's the "erroneous" determinism category for such parts...
>>
>> A predicate with the signature "pred(in) is det)" has no outputs,
>> and its determinism says it succeeds exactly once. This means that
>> it has no effect on the rest of the computation at all. When the
>> optimizer sees such a call, it is allowed to delete it, and it *will*
>> delete it at most optimization levels.
>
> Hmm... I'm trying to get the compiler to delete such a call, but it doesn't,
> even with the "-O6" parameter:
>
> :- pred wirf(int::in) is det.
>
> wirf(I) :-
>    ( if I < 0 then throw("Geworfen.")
>               else true ).
>
> main(!IO) :-
>    wirf(-1).

Optimization levels are only half of the story. Whether the above call
to wirf/1 is deleted also depends on the selected language semantics.
In Mercury's default semantics (the strict commutative semantics -- see
the reference manual), goals that are equivalent to true will only be
optimised away if the compiler can prove (1) that the goal always
terminates and (2) that the goal does not throw an exception.

If you choose a different semantics, then will get a different result.
For example, compiling your program with --no-fully-strict will allow
the compiler to "improve" completeness by optimising away the above
call to wirf/1.

>> *If* the predicate's signature were "pred(in) is erroneous",
>> the compiler would know not to delete it.
>>
>> The idea is that the compiler will preserve exceptions that you encounter
>> in the process of trying to compute some result, but won't even try to
>> preserve exceptions in computations that have no visible result.
>
> This seems to make sense...
>
>> An output argument, being declared erroneous, and being declared
>> impure are three different ways to tell the compiler "I am computing
>> something you cannot see", but the code Mark was talking about
>> contains none of these things.
>
> How would you define such a predicate with no output argument, that does
> nothing but throw an exception, depending on its input? If you want to use
> exceptions?
>
> I've taken a peek at the "Impurity declarations" chapter of the Language
> Reference Manual and tried this:
>
> :- impure pred wirf(int::in) is det.
>
> But the compiler says: "warning: declared impure but actually pure.". And I
> needed to promise main to be pure, what might not be the case (I don't fully
> comprehend).

The standard library's builtin module provides the predicate
impure_true/0, which is useful for making otherwise pure things, impure.

Julien.