The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Thanks, Makarius, for that history lesson!  I had been looking for a 
reference a couple of times before, unsuccessfully.

You can count me to the fans of |>, I have added it to my language 
MiniAgda some months ago.

  http://www2.tcs.ifi.lmu.de/~abel/miniagda

[Digression:
SML's case-of statement is superfluous if you have |>, because instead of

  case e of
     p1 => t1
   | p2 => t2

you can just write

  e |> fn p1 => t1
        | p2 => t2

(This is more useful for >>= than for |>, see below.)
End of Digression.]

I have also added <| for ordinary application, but frankly, I am more 
used to Haskell's $.

Regarding the "extremism of the Haskell community", aeh, I think that 
all kinds of application and composition operators, just to mention

  ., $, <$>, =<<, >>=, <=<, >=> ...

are quite helpful I you have to program with explicit monads and 
applicative functors.

Unfortunately, Haskell is missing "fn", thus instead of

  e >>= fn p1 -> t1
           p2 -> t2

I have to introduce an auxiliary variable and write

  x <- e
  case e of
    p1 -> t1
    p2 -> t2

Cheers,
Andreas

P.S.:

On 13.04.12 12:26 PM, Makarius wrote:
> 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

I think I have seen

  let (||>) (x,y) f = f x y

then you can continue

  let (|||>) (x,y,z) = f x y z

etc.

> 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.
>
>
> Makarius

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/