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 operations:

  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 MHonArc.