Many people like F#'s pipeline operator and associate it with the language.

Like most others I'm a lover of history and knowing the "source" of things. Now, while this may not be the last word in the matter, in this case we think we've found it; Tobias Nipkow, in May 1994.

> recently on the boat on the Seine river I promised to dig into my old
> mail folders to uncover the true story behind |> in Isabelle/ML, which
> also turned out popular in F#, and people have already transferred it
> to other languages and libraries (e.g. see http://paste.pocoo.org/show/134013/
> for some example from Scala -- it cites "F#'s pipeline operator"). 

> In the attachment you find the original mail thread of the three of us,
> coming up with this now indispensible piece of ML art in April/May 1994.
> The mail exchange starts as a response of Larry to my changes
> http://isabelle.in.tum.de/repos/isabelle/rev/daca5b594fb3 and
> http://isabelle.in.tum.de/repos/isabelle/annotate/e9ba9f7e2542/src/Pure/sign.ML#l545 

> As you can see, I was the one to use 'also' in practice for the first time.
> Despite Larry's enthusiasm, Tobias was quite reluctant to make it a "standard",
> but he came up with the actual name |> in the end. There were many more important
> things happening at that time, I have omitted some long mails on these threads that
> were mainly about the then evolving type "theory" in the Isabelle kernel.  I have
> also shortened the formal mail headers, but did not touch any body text -- for
> historical authenticity.

Thanks to Makarius Wenzel for this wonderful bit of archeology, to Tobias for making a nice choice amongst all those ASCII character combinations, and to Larry for Isabelle, which is such a wonderful application of ML-family programming. The very-1990s-email-thread is shown in its complete form below, with permission from Makarius, Larry and Tobias, including the lovely 1990s ASCII art side-comment, a joke which Larry admits passed him by on this particualr occasion:

     To make programming in ML more fun I suggest using :->

Kind regards

Don

p.s. If you know of an earlier use of this symbol for reverse function application, please let me know!


 

 

From: Lawrence C Paulson <

Larry.Paulson@cl.cam.ac.uk>

Date: Fri, 29 Apr 1994 16:31:33 +0100

The "also" infix is nice, but all other "add_XXX" functions in Isabelle are

themselves infixes, so yours could be also. Do they have to be curried?

Larry

 

From wenzelm Fri Apr 29 16:44:07 1994

To: Larry.Paulson@cl.cam.ac.uk (Lawrence C Paulson)

Subject: Re: datatype theory etc (Re: store_thm)

Date: Fri, 29 Apr 1994 16:44:07 +0100 (MESZ)

> The "also" infix is nice, but all other "add_XXX" functions in Isabelle are

> themselves infixes, so yours could be also. Do they have to be curried?

The 'also' infix has the following advantages:

- thousands of infix declarations issued at the ML toplevel avoided,

- you may use long idents, e.g. "also Sign.add_classes ...",

- curried infixes simulated, e.g. "also add_axclass (...) [...]",

which adds to user convenience in some cases.

Markus

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Markus Wenzel <wenzelm@informatik.tu-muenchen.de>

Subject: Re: datatype theory etc (Re: store_thm)

Date: Fri, 29 Apr 1994 17:27:54 +0100

> The 'also' infix has the following advantages:

> - thousands of infix declarations issued at the ML toplevel avoided,

> - you may use long idents, e.g. "also Sign.add_classes ...",

> - curried infixes simulated, e.g. "also add_axclass (...) [...]",

> which adds to user convenience in some cases.

All true, but there's still the problem of confusion with the other add_XXX

functions. A different prefix (say, new_XXX) would solve this.

While on the subject of names, we need to think of a more appropriate name for

"also", which is a general-purpose "apply" operator. A symbolic name might be

preferable, almost anything, say ##. It could be used quite heavily in the

code.

Larry

 

From wenzelm Wed May 11 10:43:23 1994

To: nipkow (Tobias Nipkow), Larry.Paulson@cl.cam.ac.uk (Larry Paulson)

Subject: names of 'add_XXX' and 'also'

Date: Wed, 11 May 1994 10:43:23 +0100 (MESZ)

[about names of add_consts, add_axioms, ...]

> there's still the problem of confusion with the other add_XXX

> functions. A different prefix (say, new_XXX) would solve this.

I'm not sure about this, but I do not like new_XXX very much. What about

ext_XXX?

 

> While on the subject of names, we need to think of a more appropriate name

> for "also", which is a general-purpose "apply" operator. A symbolic name

> might be preferable, almost anything, say ##.

"also" is the best alphabetic name I can currently think of. If we really

want a symbolic name, "##" seems to be ok (looks a bit black perhaps).

BTW, "##" may look even more teriffic (or somewhat mind-boggling), e.g.:

thy ##add_consts [..] ##add_axioms [..] ##add_instance (..) [..] [..]

 

Markus

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Markus Wenzel <wenzelm@informatik.tu-muenchen.de>

Cc: nipkow@informatik.tu-muenchen.de

Subject: Re: names of 'add_XXX' and 'also'

Date: Wed, 11 May 1994 11:43:38 +0100

> I'm not sure about this, but I do not like new_XXX very much. What about

> ext_XXX?

What about more_consts, etc.?

> "also" is the best alphabetic name I can currently think of. If we really

> want a symbolic name, "##" seems to be ok (looks a bit black perhaps).

"also" is best for your particular usage. But in general, there's no reason

why f x should be written x also f.

More generally, h(g(f(x))) is clearer if written say x ## f ## g ## h.

An arrow-like symbol such as #> might look better.

Clearly ## (or whatever we call it) should associate to the left. I wonder

whether its precedence should be high or low?

Larry

 

From: Tobias.Nipkow@Informatik.TU-Muenchen.De

To: Larry.Paulson@cl.cam.ac.uk

CC: wenzelm@informatik.tu-muenchen.de

Subject: Re: names of 'add_XXX' and 'also'

Date: Wed, 11 May 1994 18:56:13 +0100

> More generally, h(g(f(x))) is clearer if written say x ## f ## g ## h.

> An arrow-like symbol such as #> might look better.

Help! Are you redesigning SML??? Unless you expect ordinary Isabelle users to

use these wonderful infixes (which I hope you don't!) I must say I fail to

see the point...

Tobias

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Tobias.Nipkow@Informatik.TU-Muenchen.De

Cc: wenzelm@informatik.tu-muenchen.de

Subject: Re: names of 'add_XXX' and 'also'

Date: Wed, 11 May 1994 19:02:13 +0100

> Help! Are you redesigning SML??? Unless you expect ordinary Isabelle users to

> use these wonderful infixes (which I hope you don't!) I must say I fail to

> see the point...

I did actually hope long ago that a backwards "apply" operator would make it

into Standard ML. Of course, it didn't. If we are going to have one now, we

ought to define it so that it can be used for anywhere in the sources, not

just for theories.

Larry

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: nipkow@informatik.tu-muenchen.de, wenzelm@informatik.tu-muenchen.de

Subject: also

Date: Fri, 20 May 1994 17:54:33 +0100

I attach an example where a 'reverse apply' operator might be useful. Which

version you prefer may be a matter of taste, though with more and more

functions, the ## notation becomes clearer.

Larry

infix ##;

fun x ## f = f x;

val ordermap_surj =

standard

(rewrite_rule [symmetric ordertype_def]

(ordermap_type RS surj_image));

val ordermap_surj =

(ordermap_type RS surj_image) ##

rewrite_rule [symmetric ordertype_def] ##

standard;

 

From: Tobias.Nipkow@Informatik.TU-Muenchen.De

To: Larry.Paulson@cl.cam.ac.uk

CC: wenzelm@informatik.tu-muenchen.de

Subject: Re: also

Date: Sun, 22 May 1994 10:21:03 +0100

I would suggest "then" instead of "##" and "also", except that alphanumeric

infixes tend to be harder to read. How about |>?

Tobias

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Tobias.Nipkow@Informatik.TU-Muenchen.De

Cc: wenzelm@informatik.tu-muenchen.de

Subject: Re: also

Date: Mon, 23 May 1994 10:39:33 +0100

|> is better than ## (which I choose at random). Some sort of arrow is

helpful.

Larry

 

From: Tobias.Nipkow@Informatik.TU-Muenchen.De

To: Larry.Paulson@cl.cam.ac.uk

CC: wenzelm@informatik.tu-muenchen.de

Subject: Re: also

Date: Mon, 23 May 1994 15:35:32 +0100

> Some sort of arrow is helpful.

To make programming in ML more fun I suggest using :->

Tobias

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Tobias.Nipkow@Informatik.TU-Muenchen.De

Cc: wenzelm@informatik.tu-muenchen.de

Subject: Re: also

Date: Mon, 23 May 1994 16:12:03 +0100

> To make programming in ML more fun I suggest using :->

A bit long, don't you think? I'd prefer |>

 

Larry

 

From wenzelm Thu May 26 10:52:58 1994

To: Tobias.Nipkow@Informatik.TU-Muenchen.De

Cc: Larry.Paulson@cl.cam.ac.uk (Larry Paulson)

Subject: Re: also

Date: Thu, 26 May 1994 10:52:58 +0200 (MESZ)

> I would suggest "then" instead of "##" and "also",

Unfortunately, nice names like "then" or "and" are reserved keywords.

> infixes tend to be harder to read. How about |>?

> :->

These are too hard to type, IMHO.

Markus

 

From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>

To: Markus Wenzel <wenzelm@informatik.tu-muenchen.de>

Cc: nipkow@informatik.tu-muenchen.de

Subject: Re: also

Date: Thu, 26 May 1994 11:49:06 +0100

|> is quite easy to type on my keyboard: they are both shift characters. (On

the other hand, := is a pain.) In any event that's a pretty minor

consideration. I think |> is the best option.

Larry

 

From wenzelm Thu May 26 11:57:41 1994

To: Larry.Paulson@cl.cam.ac.uk (Lawrence C Paulson)

Cc: nipkow (Tobias Nipkow)

Subject: Re: also

Date: Thu, 26 May 1994 11:57:41 +0200 (MESZ)

> I think |> is the best option.

OK.

Markus

 

From: Tobias.Nipkow@Informatik.TU-Muenchen.De

To: Larry.Paulson@cl.cam.ac.uk

CC: wenzelm@informatik.tu-muenchen.de

Subject: Re: also

Date: Thu, 26 May 1994 11:52:43 +0100

No more discussion then. |> it will be.


Tobias