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

[David Overton]

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



David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------