[mercury-users] full and empty lists

[David Overton]

On Sun, Jan 13, 2002 at 10:52:37PM +1100, Dave Slutzkin wrote:
> 
> I have a type 'timeline' (which should probably be a
> typeclass - at the moment it isn't), implemented using
> the standard 'list' module.  But I've tried to put
> wrappers around all of the functions that access it so
> I can change it easily later.  I have a snippet of
> code that looks like this:
> 
> :- mode ne_tl_io == ground >> non_empty_list.
> :- mode ne_tl_in == non_empty_list >> non_empty_list.
> 
> :- func empty_timeline = (timeline::out) is det.
> :- pred full_timeline(timeline::ne_tl_io) is semidet.
> 
> empty_timeline = [].
> full_timeline([_|_]).

You may want to declare empty_timeline as

:- func empty_timeline = (timeline::out(empty_list)) is det.

where

:- inst empty_list = bound([]).

which is more precise.

> 
> Bascially - I was hoping that empty_timeline and
> full_timeline could be used in a switch statement the
> same way as [] and [_|_].
> 
> Also, after a call to full_timeline, I was hoping that
> the compiler would realise that I had a non-empty list
> and so I could save this checking in many later
> predicates.  Another snippet:
> 
> :- pred crop_timeline(timeline::in,time::in,
> timeline::out) is det.
> crop_timeline(Line,T,NewLine) :-
>     Line = empty_timeline ,
>     NewLine = empty_timeline
> ;
>     full_timeline(Line) ,
>     % we know we have a non-empty list here
>     E = first_event(Line) ,
> .

If the function first_event/1 is declared to take a non_empty_list as
input, i.e.

	:- mode first_event(ne_tl_in) = out is det.

then it (and other calls after it) will be able to use the information
that Line is non-empty.

> .
> .
> 
> Note the use of empty_timeline and full_timeline in
> the switch (are they guards?).  And also that
> first_event can be deterministic, because it takes a
> non-empty list so will always succeed.
> 
> Well, it doesn't work.  The compiler still sees this
> code as nondeterministic - I quote:
> 
> event.m:108:   In the return value of call to function
> `event:empty_timeline/0':
> event.m:108:   unification with `Line' can fail.
> event.m:111:   call to
> `full_timeline((event:ne_tl_io))' can fail.

> However, it still works when I replace empty_timeline
> with [] and full_timeline with [_|_] - although
> without the mode benefits of non_empty_list.

What _mode_ benefits do you get from using empty_timeline and
full_timeline rather than [] and [_|_] ?

As Ralph pointed out, the determinism analysis won't currently detect
that empty_timeline and full_timeline are mutually exclusive and
exhaustive (although there is someone working on allowing you to promise
this).  However, as far as _modes_ are concerned, using the constructors
directly instead of wrapping them in appropriately declared predicates
should make no difference.

> 
> Is there anything I can do about this?  Does anyone
> even understand the problem?  Otherwise I'll have to
> go back to the less modular, less deterministic
> version.
> 
> thanks,
> 
> Dave.
> 
> http://my.yahoo.com.au - My Yahoo!
> - It's My Yahoo! Get your own!
> --------------------------------------------------------------------------
> 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
> --------------------------------------------------------------------------

-- 
David Overton      Department of Computer Science & Software Engineering
PhD Student        The University of Melbourne, Victoria 3010, Australia
+61 3 8344 9159    http://www.cs.mu.oz.au/~dmo
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------