[mercury-users] List comprehensions?

[Fergus Henderson]

On 28-Apr-2001, Robert Bossy <bossy at ccr.jussieu.fr> wrote:
> > The list comprehensions in the functional programming language Clean
> > are a very compact and powerful way to express list manipulation. For
> > example the square of all integers from 1 to 10 that are not dividable
> > by three are computed by the program:
> > 
> > Start = [n*n \\ n <- [1..10] | n rem 3 <> 0]
> 
> Of course it is possible, thanks to higher order predicates and functions:
> 
> Start = filter_map((func(N) = N * N is semidet :- N mod 3 \= 0),1 `..` 10).

Peter Schachte has proposed a nice extension to Mercury syntax 
called "sequence quantification" that would make it possible
to express that kind of thing without using higher-order functions.

Under his proposal, you'd be able to write that as

	(forall N*N in Start as N in 1 `..` 10 when N mod 3 \= 0)

or something similar (the exact details of the syntax haven't been finalized).

Here's a brief description; this is from the minutes of one of our meetings
<http://www.cs.mu.oz.au/mercury/information/reports/minutes_15_12_00.html>.

 | 	The problem that sequence quantification is aimed
 | 	at addressing is that there is no way of writing
 | 	loops in Mercury without using explicit recursion
 | 	or higher-order code, both of which are conceptually
 | 	somewhat complicated. 
 | 
 | 	Sequence quantification adds a new kind of goal:
 | 
 | 		forall Var1 in Seq1
 | 		    as Var2 in Seq2
 | 		    as Var3 in Seq3
 | 		    ...
 | 		    Goal
 | 
 | 	This essentially just universally quantifies the
 | 	sequence over all corresponding elements in the
 | 	given sequences.
 | 	The declarative semantics of this can be given by
 | 
 | 		all [I] (
 | 		    (Var1 = Seq1 ^ elem(I),
 | 		     Var2 = Seq2 ^ elem(I),
 | 		     Var3 = Seq3 ^ elem(I))
 | 		=>
 | 		    Goal
 | 		)
 | 
 | 	where `Seq ^ elem(I)' is field accessor syntax
 | 	for a type class method call; `elem' is a method
 | 	of some `sequence' type class that gets the `I'th
 | 	element of the sequence.
 | 
 | 	However, operationally, the idea is that the compiler
 | 	will instead transform this into a call to a
 | 	recursive predicate.
 | 
 | 	That's the simple version; there are also some more
 | 	complicated extensions possible, including in
 | 	particular `initially ... finally ...' sequences,
 | 	which are goals of the form
 | 
 | 		forall Var1 in Seq1
 | 		    as Var2 initially Initial finally Final
 | 		    ...
 | 		    Goal
 | 
 | 	where Goal can refer to `next Var2'.
 | 	The declarative semantics of this can be defined as
 | 
 | 		forall Var1 in Seq1
 | 		    as Var2 in [Initial] ++ Accs
 | 		    as NextVar2 in Accs ++ [Final]
 | 		    ...
 | 		    Goal [with `next Var2'
 | 		    replaced by `NextVar2']
 | 
 | 	where `NextVar2' and `Accs' are both fresh variables.
 | 	i.e.
 | 
 | 		all [I] (
 | 		    (Var1 = Seq1 ^ elem(I),
 | 		     Var2 = ([Initial] ++ Accs) ^ elem(I),
 | 		     NextVar2 = (Accs ++ [Final]) ^ elem(I))
 | 		=>
 | 		    Goal
 | 		)
 | 	
 | 	For example:
 | 
 | 		:- func sum(list(int)) = int.
 | 		sum(L) = Sum :-
 | 			forall X in L
 | 			    as Acc initially 0 finally Sum
 | 			    next Acc = Acc + X.
 | 
 | 	The modes allowed for sequence quantification
 | 	are more general than what is allowed for
 | 	universal quantification in Mercury.
 | 	Universal quantifications can't have any
 | 	outputs.  But for sequence quantification we
 | 	can handle the modes by using mode inference
 | 	for the generated recursive predicate, which
 | 	will allow `forall' goals to produce outputs.
 ...
 | 	Tyson suggested that we could allow optional
 | 	explicit mode annotations on forall goals, i.e.
 | 
 | 		forall <Var1> in (<Seq1>::in)
 | 		    as <Var2> in (<Seq2>::in)
 | 		    as <Var3> in (<Seq3>::out)
 | 		    ...
 | 		    <Goal>
 | 
 | 	The general consensus was that this proposal for sequence
 | 	quantification seemed like a good idea.

For more information, see also
<http://www.cs.mu.oz.au/mercury/mailing-lists/mercury-developers/mercury-developers.0101/0003.html>.

Adrian Pellas-Rice <apell at students.cs.mu.oz.au> did quite a bit of work towards
implementing this in the Mercury compiler, but unfortunately didn't have time
to finish it; perhaps someone may be interested in picking up where he left off
(see <http://www.cs.mu.oz.au/mercury/mailing-lists/mercury-reviews/mercury-reviews.0104/0050.html>).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------