The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Mon, 16 Apr 2012, Erik Ernst wrote:

> > Stéphane seems to like the |> operator, which was intruced in 
> > Isabelle/ML in 1994 and later made its way into F#.  See also 
> > http://blogs.msdn.com/b/dsyme/archive/2011/05/17/archeological-semiotics-the-birth-of-the-pipeline-symbol-1994.aspx
> >
> > This is the essential starter kit in OCaml notation:
> >
> >  let (|>) x f = f x
> >  let (|->) (x, y) f = f x y
> >
> >  let (@>) f g x = g (f x)
> >  let (@->) f g (x, y) = g (f x y)
>
> Considering the history it's worth noting something that happened a 
> couple of decades earlier than 1994:  The language BETA has used this 
> syntactic structure for application since approx. 1977
>
> If you want to check it out there is "The BETA book" at 
> http://www.daimi.au.dk/~beta/Books/index.html.

That is interesting.  Maybe you should add a comment to the above blog of 
Don Syme, where he collects the history.  He explicitly says "If you know 
of an earlier use of this symbol for reverse function application, please 
let me know!"


After pipelining applications in ML for several years, we discovered that 
the following fold combinators with so-called "canonical argument order" 
fit particularly well with it (now in SML notation):

(*fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b*)
fun fold _ [] y = y
  | fold f (x :: xs) y = fold f xs (f x y);

(*fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b*)
fun fold_rev _ [] y = y
  | fold_rev f (x :: xs) y = f x (fold_rev f xs y);

(*fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b*)
fun fold_map _ [] y = ([], y)
  | fold_map f (x :: xs) y =
      let
        val (x', y') = f x y;
        val (xs', y'') = fold_map f xs y';
      in (x' :: xs', y'') end;

Now you can write

  b |> f a1 |> f a2 |> f a3

as

  b |> fold f [a1, a2, a2]

etc.

There are further advantages of the above. I am still hoping for more 
people to rediscover these useful patterns.

Please excuse my SML.  Next time I will try harder to write it in OCaml or 
Coq notation, to stay on-topic for this mailing list.


        Makarius