Hello,

I'm worrying that there are too many constraints put on the definition
of a function's domain. Thus, if you agreed on the domains of take, drop,
etc. and their semantics, please give a definition, say D, of these functions
in terms of the ordinary list constructors. I would consider any
implementation of take, e.g., to terminate for at least the input values
for which it terminates, if defined by D.

I agree, that the following equation is very useful:

    take n xs ++ drop n xs == xs

I would also prefer monotonicity, i.e., 

    take (n-1) xs   always be a prefix of    take n xs
and
    drop (n+1) xs   always be a suffix of    drop n xs

A definition respecting this would be:

    take n xs     | n<=0 = []
    take n []     | n>0  = []
    take n (x:xs) | n>0  = x : take (n-1) xs
and
    drop n xs     | n<=0 = xs
    drop n []     | n>0  = []
    drop n (x:xs) | n>0  = drop (n-1) xs

Termination of take works also if xs is an infinite list.

-- 
 Christoph Herrmann
 E-mail:  [EMAIL PROTECTED]
 WWW:     http://brahms.fmi.uni-passau.de/cl/staff/herrmann.html


Reply via email to