The Coq mailing list

[Erik Ernst <eernst AT cs.au.dk>]

Den 13/04/2012 kl. 12.26 skrev Makarius:

> On Fri, 13 Apr 2012, Stéphane Glondu wrote:
> 
>> Le 12/04/2012 19:30, Xavier Leroy a écrit :
>>> Short form: is there a tool / how would you go about writing a tool
>>> that, given the *statement* of a Coq theorem, shows all *definitions*
>>> involved in this statement, omitting all the stuff that contribute
>>> only to the *proof* of the theorem?
>> 
>> This can be done in a plugin. I've attached a proof of concept.
> 
> 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
> 
> Over the years, a few more variants of it were introduced that could also 
> help OCaml and Coq people to express function application and composition 
> concisely, without the extremism of the Haskell community in this respect.
> 
> 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)
> 
> The latter two are called #> and #-> in Isabelle/ML, but OCaml does not
> allow # in symbolic identifiers as it seems.


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 (so a pipeline like the one 
described on http://lorgonblog.wordpress.com/2008/03/30/pipelining-in-f/ is ;
very natural in BETA).  In the design of BETA, Kristen Nygaard and his 
co-workers specifically emphasized the benefits of aligning the order of 
evaluation and the syntax, and it's actually a rather fundamental element in 
the syntactic structure of this language.  (If you want to check it out there 
is "The BETA book" at http://www.daimi.au.dk/~beta/Books/index.html.)

  best regards,

-- 
Erik Ernst - 
eernst AT cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark