I don't understand how I can do both with one function.
Yes, at first this seems odd, but then once you get the hang of it, you miss it in other languages.
The word you want to remember when referencing this is: mode
Also see Mercury Modes reference for more detail related to the Mercury programming language.
In Prolog an argument can be an input, and output, or both used as an input or output depending upon how it is called.
In Type, mode and determinism declaration headers at the bottom is listed 4 examples.
- length(+List:list, -Length:int) is det.
- length(?List:list, -Length:int) is nondet.
- length(?List:list, +Length:int) is det.
- True if List is a list of length Length.
and the definition of length/2
shows
length(?List, ?Int)
meaning
that for the List
argument, the list can be bound or unbound, and
that for the Int
argument, the value can be bound or unbound.
So for the two arguments with two options there are four ways to use length/2
Here they are listed again but in actual usage.
1.
length(+List:list, -Length:int) is det.
in this case List is bound and Length is unbound and always gives one answer.
?- length([1,2,3],N).
N = 3.
2.
length(?List:list, -Length:int) is nondet.
in this case List is unbound and Length is unbound and can return any number of answers.
?- length(List,N).
List = [],
N = 0 ;
List = [_5362],
N = 1 ;
List = [_5362, _5368],
N = 2 ;
List = [_5362, _5368, _5374],
N = 3 ;
List = [_5362, _5368, _5374, _5380],
N = 4 ;
List = [_5362, _5368, _5374, _5380, _5386],
N = 5
...
3.
length(?List:list, +Length:int) is det.
in this case List is unbound and Length is bound and always gives one answer.
?- length(List,4).
List = [_5332, _5338, _5344, _5350].
4.
True if List is a list of length Length.
in this case List is bound and Length is bound and always acts as predicate to return either true
or false
.
?- length([1,2,3],3).
true.
?- length([1,2,3],5).
false.
So how is this possible?
Prolog uses syntactic unification (↦) and NOT assignment (=).
If we look at the source code for length/2
using listing/1
we get
?- listing(length/2).
system:length(B, A) :-
var(A), !,
'$skip_list'(D, B, C),
( C==[]
-> A=D
; var(C)
-> C\==A,
'$length3'(C, A, D)
; throw(error(type_error(list, B), context(length/2, _)))
).
system:length(B, A) :-
integer(A),
A>=0, !,
'$skip_list'(D, B, C),
( C==[]
-> A=D
; var(C)
-> E is A-D,
'$length'(C, E)
; throw(error(type_error(list, B), context(length/2, _)))
).
system:length(_, A) :-
integer(A), !,
throw(error(domain_error(not_less_than_zero, A),
context(length/2, _))).
system:length(_, A) :-
throw(error(type_error(integer, A), context(length/2, _))).
which is too much detail but does do all 4 modes correctly.
To make it easier to understand we will use this version, but it doesn't support 1 of the modes correctly but it does do more than one mode so it works good enough to demonstrate.
length_2([] , 0 ).
length_2([_|Xs] , L ) :-
length_2(Xs,N),
L is N+1 .
Now to see the unification in action we will use the trace feature of SWI-Prolog and to enable all of the ports for the box model use visible/1 and so as not to stop it when running use leash/1.
?- visible(+all),leash(-all).
?- trace.
1.
[trace] ?- length_2([1,2,3],N).
Call: (8) length_2([1, 2, 3], _2352)
Unify: (8) length_2([1, 2, 3], _2352)
Call: (9) length_2([2, 3], _2580)
Unify: (9) length_2([2, 3], _2580)
Call: (10) length_2([3], _2580)
Unify: (10) length_2([3], _2580)
Call: (11) length_2([], _2580)
Unify: (11) length_2([], 0)
Exit: (11) length_2([], 0)
Call: (11) _2584 is 0+1
Exit: (11) 1 is 0+1
Exit: (10) length_2([3], 1)
Call: (10) _2590 is 1+1
Exit: (10) 2 is 1+1
Exit: (9) length_2([2, 3], 2)
Call: (9) _2352 is 2+1
Exit: (9) 3 is 2+1
Exit: (8) length_2([1, 2, 3], 3)
N = 3.
2.
[trace] ?- length_2(List,N).
Call: (8) length_2(_2296, _2298)
Unify: (8) length_2([], 0)
Exit: (8) length_2([], 0)
List = [],
N = 0 ;
Redo: (8) length_2(_2296, _2298)
Unify: (8) length_2([_2528|_2530], _2298)
Call: (9) length_2(_2530, _2550)
Unify: (9) length_2([], 0)
Exit: (9) length_2([], 0)
Call: (9) _2298 is 0+1
Exit: (9) 1 is 0+1
Exit: (8) length_2([_2528], 1)
List = [_2528],
N = 1 ;
Redo: (9) length_2(_2530, _2550)
Unify: (9) length_2([_2534|_2536], _2556)
Call: (10) length_2(_2536, _2556)
Unify: (10) length_2([], 0)
Exit: (10) length_2([], 0)
Call: (10) _2560 is 0+1
Exit: (10) 1 is 0+1
Exit: (9) length_2([_2534], 1)
Call: (9) _2298 is 1+1
Exit: (9) 2 is 1+1
Exit: (8) length_2([_2528, _2534], 2)
List = [_2528, _2534],
N = 2 ;
Redo: (10) length_2(_2536, _2556)
Unify: (10) length_2([_2540|_2542], _2562)
Call: (11) length_2(_2542, _2562)
Unify: (11) length_2([], 0)
Exit: (11) length_2([], 0)
Call: (11) _2566 is 0+1
Exit: (11) 1 is 0+1
Exit: (10) length_2([_2540], 1)
Call: (10) _2572 is 1+1
Exit: (10) 2 is 1+1
Exit: (9) length_2([_2534, _2540], 2)
Call: (9) _2298 is 2+1
Exit: (9) 3 is 2+1
Exit: (8) length_2([_2528, _2534, _2540], 3)
List = [_2528, _2534, _2540],
N = 3
3.
[trace] ?- length_2(List,3).
Call: (8) length_2(_5534, 3)
Unify: (8) length_2([_5724|_5726], 3)
Call: (9) length_2(_5726, _5746)
Unify: (9) length_2([], 0)
Exit: (9) length_2([], 0)
Call: (9) 3 is 0+1
Fail: (9) 3 is 0+1
Redo: (9) length_2(_5726, _5746)
Unify: (9) length_2([_5730|_5732], _5752)
Call: (10) length_2(_5732, _5752)
Unify: (10) length_2([], 0)
Exit: (10) length_2([], 0)
Call: (10) _5756 is 0+1
Exit: (10) 1 is 0+1
Exit: (9) length_2([_5730], 1)
Call: (9) 3 is 1+1
Fail: (9) 3 is 1+1
Redo: (10) length_2(_5732, _5752)
Unify: (10) length_2([_5736|_5738], _5758)
Call: (11) length_2(_5738, _5758)
Unify: (11) length_2([], 0)
Exit: (11) length_2([], 0)
Call: (11) _5762 is 0+1
Exit: (11) 1 is 0+1
Exit: (10) length_2([_5736], 1)
Call: (10) _5768 is 1+1
Exit: (10) 2 is 1+1
Exit: (9) length_2([_5730, _5736], 2)
Call: (9) 3 is 2+1
Exit: (9) 3 is 2+1
Exit: (8) length_2([_5724, _5730, _5736], 3)
List = [_5724, _5730, _5736]
Action (h for help) ? abort
% Execution Aborted
4.
[trace] ?- length_2([1,2,3],3).
Call: (8) length_2([1, 2, 3], 3)
Unify: (8) length_2([1, 2, 3], 3)
Call: (9) length_2([2, 3], _2058)
Unify: (9) length_2([2, 3], _2058)
Call: (10) length_2([3], _2058)
Unify: (10) length_2([3], _2058)
Call: (11) length_2([], _2058)
Unify: (11) length_2([], 0)
Exit: (11) length_2([], 0)
Call: (11) _2062 is 0+1
Exit: (11) 1 is 0+1
Exit: (10) length_2([3], 1)
Call: (10) _2068 is 1+1
Exit: (10) 2 is 1+1
Exit: (9) length_2([2, 3], 2)
Call: (9) 3 is 2+1
Exit: (9) 3 is 2+1
Exit: (8) length_2([1, 2, 3], 3)
true.
[trace] ?- length_2([1,2,3],5).
Call: (8) length_2([1, 2, 3], 5)
Unify: (8) length_2([1, 2, 3], 5)
Call: (9) length_2([2, 3], _2442)
Unify: (9) length_2([2, 3], _2442)
Call: (10) length_2([3], _2442)
Unify: (10) length_2([3], _2442)
Call: (11) length_2([], _2442)
Unify: (11) length_2([], 0)
Exit: (11) length_2([], 0)
Call: (11) _2446 is 0+1
Exit: (11) 1 is 0+1
Exit: (10) length_2([3], 1)
Call: (10) _2452 is 1+1
Exit: (10) 2 is 1+1
Exit: (9) length_2([2, 3], 2)
Call: (9) 5 is 2+1
Fail: (9) 5 is 2+1
Fail: (8) length_2([1, 2, 3], 5)
false.
and to turn the trace off
[trace] ?- notrace.
true.
[debug] ?- nodebug.
true.
I won't go through each of the lines in the trace output, but if you understand syntactic unification and can follow the trace, after working through the examples given you will see how variables in Prolog are unified resulting in different modes when compared to imperative programming.
Remember that variables are only bound once in Prolog, and never reassigned, and that the numbers on the left in the trace in parenthesis, e.g. (10), are the stack level, so when a call is made to a predicate again, a new set of variables are made available, and while it may seem the are being reassigned a value, it is actually another variable in the stack, just in a different stack frame.
As an aside when learning Prolog one piece of advise I give is that it is easier to learn if you set aside what you know about imperative and functional programming, except for maybe recursion, and start from the ground up with unification and then backward chaining.
If you can read OCaml, here is a simplified version of unification and backward chaining. Note that this is not a Prolog as it does not have list or the cut operator but if you can understand it, then the ways of unification and backward chaining become apparent.
I have to add that I am not totally satisfied with my answer as I know you are a beginner and this answer is to much information to digest and requires a lot of work on your part to work through the 4 trace examples. However it does answer the question and gives a practical example with more than enough meat on the bone. I am working on trying to think of a better example which would include logical purity and that demonstrates that not only unification but relationships are key to how multiple modes can be accomplishes in one predicate. Be glad I didn't use general relativity as paraphrased by the relativist John Archibald Wheeler, spacetime tells matter how to move; matter tells spacetime how to curve
.