Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Isabelle/ML "build" combinators

Email Gateway (Sep 22 2021 at 10:39):

From: Makarius <makarius@sketis.net>
* ML *

• The "build" combinators of various data structures help to build
  content from bottom-up, by applying an "add" function the "empty" value.
  For example:

  • type 'a Symtab.table etc.: build
  • type 'a Names.table etc.: build
  • type 'a list: build and build_rev
  • type Buffer.T: build and build_content

For example, see src/Pure/PIDE/xml.ML:

val content_of = Buffer.build_content o fold add_content;

This refers to Isabelle/4974c3697fee.

It may be seen as the final capstone for our approach to "canonical argument
order": it has turned out very beneficial to Isabelle/ML readability and
conciseness since 2005 (especially in contrast to the monadic bloat seen in
Haskell libraries).

We did not have "build" combinators in the past, because most applications
were for plain lists where "empty" is just []. For other data structures, it
does help to make the point more clear.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Jul 15 2022 at 23:21 UTC