Re: [isabelle] List.span
On Wed, 14 Aug 2013, Christian Sternagel wrote:
One (tiny) pro is that "span P xs" is shorter to type than "(takeWhile P
xs, dropWhile P xs)". I'm not sure how often this pattern occurs in
actual formalizations though.
Isabelle/HOL is Isabelle/ML, but in the latter we have the following
val take: int -> 'a list -> 'a list
val drop: int -> 'a list -> 'a list
val chop: int -> 'a list -> 'a list * 'a list
In that terminology the above would be take_while, drop_while, and
chop_while (instead of "span").
The chop operation was introduced in addition to the older take / drop to
support canonical argument order in ML, i.e. to optimize clarity and
readability of the sources in certain situations. (If abused this leads
to agglomerates of pointless combinators.)
There was never a consideration to "optimize" runtime to avoid a second
walk through the list or intermediate tupling. Such low-level accounting
has hardly any impact on complex applications running on complex hardware
(with lots of caches, cores etc.).
This archive was generated by a fusion of
Pipermail (Mailman edition) and