Archeological Semiotics: The Birth of the Pipeline Symbol, 1994
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 <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
> <isabelle.in.tum.de/repos/isabelle/rev/daca5b594fb3> and
> <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 <
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