Reifying results

Not entirely sure this is the right term. Summary is that there are several occasions where want to capture the truth value of a goal without failing. Examples are execution in a thread or on a remote server. If the remote call fails you want it to report this rather than failing and not sending anything back. For this purpose, I often define a predicate like

reify(Goal, Result) :-
    (   catch(Goal, E, true)
    ->  (   var(E)
	    ->  Result = true
	    ;   Result = error(E)
	    )
    ;   Result = false
    ).

This works fine. Of course you also want to turn this into normal true/false/error, e.g.

unreify(true).
unreify(false) :- fail.
unreify(error(E)) :- throw(E).

I’m considering adding this to the library. Problem is notably naming the library and the two predicates. Is this part of a bigger class of functionality?

1 Like

Maybe the problem can be reduced by having the first predicate unify Result with throw(E) instead of error(E), thus making the second predicate equivalent to call/1.
Taking this a step further, we can think of the first predicate as mapping concrete goals to canonically simplified goals that have the same “result”. This perspective suggests calling it something like goal_canonical/2, although I’m not sure that’s any clearer than reify/2

Just my two cents :slight_smile:

That surely has the advantage that we do not have to invent a name :slight_smile: When used to deal with remote connections though it offers a bit of a security issue :slight_smile: It made me think that many dynamically typed garbage collected programming languages are considered “safe” as one cannot get trapped by the usual memory management issues. Most of them provide some mechanism to evaluate a string or make a call based on some data structure (similar to Prolog call/N). I’ve seen plenty of examples of people using that in server applications for handling requests or responses from clients. Not a good idea …

That is what the toplevel does: it prints a program consisting of =/2 conjunctions and disjunctions that produce the same result. That includes failure, but not exceptions (it would have to write throw(...) rather than a human readable error message). I wouldn’t call that canonical. More partial evaluation: given the context you create a simpler program.

I’m getting worried that the problem is similar to delete/3: there are simply too many scenarios one may one to handle using this type of “reification” (if that is the right term). As shows, provide the bindings through the original instantiated goal, provide the bindings as a reduced template that only contains the free variables in Goal, deal with non-determinism, etc.

I often think of that as mapping a non-Boolean type into Boolean type or error type. As you note, when writing code that interacts with code that returns non-Boolean results and needing a Boolean result so that the use of the non-Boolean code appears as a predicate such is often used. To this day the word reify is one of those terms I don’t really understand, just like closure, I have to read it in context to really understand its meaning. Personally I like the predicate but do not like the name for it; reify. The name alone is enough to make me avoid using it if I did not already know it.

When looking at both predicates, reify/2 and unreify/1, and then mentally adding the types the code makes even more sense to me. With the types mentally added and looking at the definition of reify it seems that reify is too broad as it is mapping into just a Boolean or error type, so maybe the name reify_boolean or reify_predicate is closer to what makes sense but I don’t like them either. :frowning_face:


Agree.

reify/2 seems a specific case of typing and some of my code modules are loaded with tens of typing predicates just for each abstract type in the module. When the term contains a list of types and then one needs to walk the list one creates many more predicates that then simplify down to predicates like

foo([],_) :- !.
foo([H|T],A) :-
    foo(H,A), !,
    foo(T,A).

foo([],_,_) :- !.
foo([H|T],A,B) :-
    foo(H,A,B), !,
    foo(T,A,B).

foo([],_,_,_) :- !.
foo([H|T],A,B,C) :-
    foo(H,A,B,C), !,
    foo(T,A,B,C).

foo([],_,_,_,_) :- !.
foo([H|T],A,B,C,D) :-
    foo(H,A,B,C,D), !,
    foo(T,A,B,C,D).

foo([],_,_,_,_,_) :- !.
foo([H|T],A,B,C,D,E) :-
    foo(H,A,B,C,D,E), !,
    foo(T,A,B,C,D,E).

foo([],_,_,_,_,_,_) :- !.
foo([H|T],A,B,C,D,E,F) :-
    foo(H,A,B,C,D,E,F), !,
    foo(T,A,B,C,D,E,F).

For those who use library(apply) this should seem like an old friend.

I know one could use =…/2 instead but the expanded code is for demonstration purposes.

As defined in https://en.wikipedia.org/wiki/Reification_(computer_science):

Reification is the process by which an abstract idea about a computer program is turned into an explicit data model or other object created in a programming language.

so reify seems quite appropriate to me, the “abstract idea” being success, failure, or error, and the “exlicit data model” being one of true, false and throw(Err) (using @oskardrums suggestion). Not sure what this has to do with types.

I think implicit unification when Result = true might just be the tip of the iceberg. What about other backtrackable side effects (global variables, setarg). These don’t really matter at the top level (just outputs a list of unifications) but may matter in a programming context. Probably simplest to just treat reify(Goal,true) as equivalent to call(Goal) in the absence of errors. (Also seems easier to explain.) In fact, I would use reify(Goal,true) as an elegant way (compared to catch/3) of turning errors into failures.

Unless there’s more to it than this, why wouldn’t you just make reify/2 a system meta-predicate like call.

reify/2 is based on catch/3 :). I don’t see a big different between reify(Goal, true) and catch(Goal, _, fail) although the first looks a little prettier.

Thanks for justifying the name. I’m reluctant to add stuff like this as a system predicate (unless it gets many likes :slight_smile: ). Just adding a library with one predicate of just a few lines seems wrong as well. Best seems to find a library where it makes sense or add a new library of we see we can define more similar predicates.

So far library(error) and library(apply) seems the only two remotely related libraries we have.

My point exactly. And as I’m not particularly fond of errors, I like to bury them.

Not a huge deal, but “un-reification” is just call and true, false and throw are all system predicates. So it feels to me more like a system level thing rather than anything in the libraries you mentioned (" A.3 library(apply): Apply predicates on a list" and " A.16 library(error): Error generating support").

IMO, if it isn’t a system predicate why not just leave it up to the application; it’s simple enough. But it would make a good example for " 4.10 Exception handling" documentation.

2 Likes

My two cents on an alternative name. How about truth/2 ?

truth(true, true) succeeds

Actually the biggest problem is the reverse name :slight_smile: I’ve done a little work on trying to turn this into a library that can also deal with nondet scenarios and scenarios where the execution happens in a remote environment (thread, process), so we must also include the bindings in the result. You get on the client side something like

  • prepare(Goal, Prepped),
  • send(Server, Prepped),
  • read result, re-read on backtracking. handle bindings and failure/exceptions.

And the server does

  • receive(Prepped),
  • reify(Prepped, Result),
  • Send result, check whether client wants next.

That smells a lot like Pengines :slight_smile: Just, more lightweight, Prolog ↔ Prolog only and abstracting from the transport using a primitive that can get a Prolog term to the other side.

That’s what I was thinking.

A few days ago when reading the first post and sleeping on it, it reminded me of Railway-Oriented-Programming which I mentioned a while ago, the concept is common among many programming systems and noticeable once understood.

So with regards to a name, as much as I hate to say this, maybe an operator or a few operators would be better.


EDIT

Ran across the following in my morning current events review and noting it here because much of what it talks about has connections with what I think Jan W. is trying to create, I could be wrong.

This is not a Monad Tutorial

When reading it if one does not understand the term happy path then see Railway Oriented Programming.

The interesting part for me was the connection to F# Computation Expressions and that they could/seem to be the few operators noted earlier. :slightly_smiling_face:


EDIT

Another item found in my morning current events review.

Recently OCmal has been upgraded with parallelism, OCaml 5.0
The part of note possibly related to this is Effect handlers but Parallel programming might also be of some value for ideas.

Hello,

Recently, I have stumbled on a use case of reify/2. However, the current implementation provided by Jan has one drawback for me. It cuts all choice points inside the reified goal if the goal succeed with choice points. In my opinion, a more correct logical implementation would keep all choice points of the reified goal and indicate a failed reified goal only if the reified goal has never succeeded. I found out that I can implement reify as I want using the deterministic/1 predicate:

reify(Goal, true) :-
   Goal,
   deterministic(Det),
   (   Det == true
   -> !
   ;   true
   ).
reify(_, false).

Here is an example of dcg code where I want to generate the longest possible sequence of a and b. I only want the longest sequence possible but I want to keep all combinations of a and b possible.

:- use_module(library(dcg/high_order)).

reify(Goal, true) -->
   Goal,
   {
      deterministic(Det),
      (  Det == true
      -> !
      ;  true
      )
   }.
reify(_, false) --> [].

ab(a) --> [a].
ab(b) --> [b].

abs(ABs) -->
   reify(ab(AB), Result),
   abs(Result, AB, ABs).
abs(true, AB, [AB | ABs]) -->
   abs(ABs).
abs(false, _, []) -->
   [].

When using sequence//2, the query gives an extra solution which I don’t want.

?- length(L, 1), phrase(sequence(ab, ABs), L, R).
L = ABs, ABs = [a],
R = [] ;
L = ABs, ABs = [b],
R = [] ;
L = R, R = [_],  % extra solution that I don't want
ABs = [].

When using Jan’s version of reify inside abs//1, I only obtain the first solution:

?- length(L, 1), phrase(abs(ABs), L, R).
L = ABs, ABs = [a],
R = [] ;

When using my version of reify, I obtain both solutions without the empty sequence:

?- length(L, 1), phrase(abs(ABs), L, R).
L = ABs, ABs = [a],
R = [] ;
L = ABs, ABs = [b],
R = [].

What are your thoughts on this ?

After some more testing, I think my version of reify/2 is flawed if the remaining choice point leads to a failure of the goal.

Did you manage to write a version of reify/2 that works for non-deterministic goals ?

I think you need to be comparing variables, rather than whether choicepoints exist.

Similar: lookup_other at if statement - Converting if-then in Prolog to multiple clauses with reification - Stack Overflow

I’m sorry, I don’t really understand which variable I should be comparing or the use of the lookup_other predicate.
However, from your stack overflow link, I found the soft cut operator *-> which seems to do what I want in this case:

reify2(Goal, Result) :-
   (  Goal
   *-> Result = true
   ;  Result = false
   ).

Do you see any drawback from this soft cut operator ?

Yes - it’s wrong for this purpose :wink:

Need to compare variables using ==, to know when alternates can be safely avoided, for determinism.

The variables in your code are the a and b in:

ab(a) --> [a].
ab(b) --> [b].

And the thing to reify is whether a and b are in the DCG list.

Take a look at my code. The == comparison goes on to perform a cut, because == means that e.g. it’s a ground a and therefore cannot be b, so we can add some nice determinism and prevent the comparison with b.

Or, if it’s e.g. var, then it can be either a or b, or something else (using dif/2 to prevent matching a or b).

The “other”, in your simple case, can be unification with [] to result in the end of the DCG list. For your simple example, [] can replace the usage of dif.

I should have been more precise with my purpose.
The ab/1 predicate is only an example and should not be modified for the purpose of reification.

In my use-case, the thing I want to reify is the success or failure of an arbitrary goal, because this information can help me remove possible answers that would be hard to otherwise.

Goals have variables. To cut paths short, I use == with the variables, leading to a cut.

Regarding your previous code snippet: *-> does not help in cutting the code path for the (what I call “other”) alternative of [].

Do you have a better example to consider?

pack(stoics_lib) has holds/2 with similar semantics.

It only returns (also takes) true/false as the second argument as the scenarios
it is used is for indexing clauses of subsequent called predicates.
And it is called within a single SWI environment so errors are as per usual.

As you ld expect I think holds/2 is a better name for my use case- yours is a bit more general.

Nicos Angelopoulos

https://stoics.org.uk/~nicos