[mercury-users] Higher-order semideterminism in discriminated unions

[André Platzer]

David Overton wrote:

>On Tue, Aug 26, 2003 at 12:36:02PM +0200, api at gmx.de wrote:
>  
>
>>Hello!
>>
>>When working with higher-order predicates that get a function as an
>>argument and have to store in a data structure defined by a
>>discriminated union, everything works only when the declared determinism
>>of the function argument is det. But as soon as it is changed to semidet
>>or worse, the compiled program crashes with a segmentation fault at
>>runtime. Also the mercury debugger produces invalid results.
>>
>>For example
>>:- module tst_hol_semidet.
>>:- interface.
>>:- import_module io.
>>
>>:- pred main(io__state::di, io__state::uo) is det.
>>
>>:- type storage(Y).
>>:- pred do(func(string)=Y, storage(Y)) .
>>:- mode do(in(func(in)=out is semidet), out) is det.
>>
>>:- func use(storage(Y), string) = Y.
>>:- mode use(in, in) = out is semidet.
>>
>>:- implementation.
>>:- import_module string, require.
>>
>>:- type storage(Y) ---> store(func(string)=Y).
>>
>>do(F, store(F)).
>>
>>use(store(F), A) = F(A).
>>
>>main -->
>>    {do(
>>        (func(A::in) = ((A ++ "1")::out) is semidet
>>        :- A \= "No"
>>        ),
>>        Storage
>>       )},
>>    { Res1 = use(Storage, "Yes") ->
>>      R1 = Res1
>>    ;
>>      error("Dunno Yes")
>>    },
>>    print(R1),
>>
>>    { Res2 = use(Storage, "No") ->
>>      R2 = Res2
>>    ;
>>      error("Dunno No")
>>    },
>>    print(R2)
>>    ;
>>    {error("did not work")}.
>>
>>
>>Contrary to the det version, this program crashes with
>>*** Mercury runtime: caught segmentation violation ***
>>This may have been caused by a stack overflow, due to unbounded
>>recursion.
>>exiting from signal handler
>>    
>>
>
>This appears to be a bug in the mode analyser in the compiler.  It
>should report a mode error for predicate do/2 because the higher-order
>value "loses" its higher-order mode information when it is stored in the
>data structure.  This is supposed to be disallowed for function terms so
>that the assumption you quoted from the reference manual is safe.
>
>I'll have a look at fixing that bug, but to get this to work you need to
>change your code so that the store has the information that the function
>it contains is semidet.  E.g. add an inst
>
>	:- inst store_semidet ---> store(func(in) = out is semidet).
>
>and change the mode declarations to
>
>	:- mode do(in(func(in) = out is semidet), out(store_semidet)) is det.
>	:- mode use(in(store_semidet), out) is semidet.
>
>  
>
>>>From the manuals I quote the "higher-order mode" section from which I
>>understand that Determinism=semidet should be legal.
>>
>>"In order to call a higher-order term, the compiler must know its
>>higher-order inst. This can cause problems when higher-order terms are
>>placed into a polymorphic collection type and then extracted, since the
>>declared mode for the extraction will typically be `out' and the
>>higher-order inst information will be lost. To partially alleviate this
>>problem, and to make higher-order functional programming easier, if the
>>term to be called has a function type, but no higher-order inst
>>information, we assume that it has the default higher-order function
>>inst `func(in, ..., in) = out is Determinism'."
>>
>>Does anyone know what to do then? I have tried to use instantiatedness
>>information for the storage but without success.
>>    
>>
>
>Have you tried the approach I describe above?  That should work
>(although I haven't tested it).
>
Erm, yes thanks. Of course you are right, in the simplified example I 
have provided this really solves the problem. But in my real application 
scenario, unfortunately this cannot be applied - as far as I know. 
Actually, storage is a typeclass so the example had better been like this

:- module tst_hol_semidet2.
:- interface.
:- import_module io.

:- pred main(io__state::di, io__state::uo) is det.

:- inst store_semidet ---> store(func(in) = out is semidet).


:- typeclass storage_class(Storage) where [
    some [Y] pred use(string, Y, Storage, Storage),
    mode use(in, out, in/*(store_semidet)*/, out/*(store_semidet)*/) is det
].


:- some [Storage] (pred do(func(string)=Y, Storage) => 
storage_class(Storage)).
:- mode do(in(func(in) = out is semidet), out/*(store_semidet)*/) is det.

:- implementation.
:- import_module string, require, std_util.

:- type storage(Y) ---> store(func(string)=Y).
:- instance storage_class(storage(Y)) where [
    (use(A, F(A), store(F), store(F)))
 ].
do(F, store(F)).


:- func cast_det(T::in) = (S::out) is det.
cast_det(X) = Y :-
    univ_to_type(univ(X), Y)
    ;
    error("casting failed").

main -->
    {do(
        (func(A::in) = ((A ++ "1")::out) is semidet
        :- A \= "No"
        ),
        Storage
       )},
    { use("Yes", Res1, Storage, Storage1) ->
      R1 = cast_det(Res1) `with_type` string
    ;
      error("Dunno Yes")
    },
    print(R1),

    { use("No", Res2, Storage, Storage2) ->
      R2 = cast_det(Res2) `with_type` string
    ;
      error("Dunno No")
    },
    print(R2)
    ;
    {error("did not work")}.

Here, the desired instantiatedness cannot be guaranteed at the 
invocation of use/4 since the appropriate mode will be declared in the 
typeclass storage/1. But this typeclass cannot know of  the individual 
instantiatedness trees of its respecitve instances. So the 
instantiatedness restrictions /*(store_semidet)*/ cannot be uncommented. 
Thus still the problem persists. What am I to do now?

P.S. By the way, what's the difference between the following two

    :- inst store_semidet1 ---> store(func(in) = out is semidet).
    :- inst store_semidet2 == bound(store(func(in) = out is semidet)).

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------