[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

On 01/02/18 17:23, Tobias Nipkow wrote:
> 
> I think (simple) sections do indeed improve readbility. BUT in the light
> of your comments I am not keen on them in Isabelle. We do not need yet
> more syntactic sugar.

For the record, here are a few more questions:

>> Here are also some notes from Haskell:
>> https://wiki.haskell.org/Section_of_an_infix_operator that immediately
>> raise more questions:
>>
>>    * What to do with prefix "-" vs. infix "-"?
>>
>>    * What to do with iterated sections (a + b +)?
>>
>>    * Does all that actually help readability of expressions (e.g. for
>> mathematicians) or just appeal to strange Haskelloids?

  * Why are sections restricted to infixes? (Haskell provides backtick
notation to make infixes on the spot, but we don't have that.)

  * Why are implicit argument positions limited to the end points (left
or right section)?


It is probably better to see the problem as general partial application,
similar like "_" in Scala:
https://www.scala-lang.org/files/archive/spec/2.11/06-expressions.html#placeholder-syntax-for-anonymous-functions
https://www.scala-lang.org/files/archive/spec/2.11/13-syntax-summary.html

That has its own complexity, and I often get it wrong in practice (even
after 10 years of using Scala).


The general concept behind it is implicit abstraction, here with
explicit (( ... )) to delimit its scope (different notation would be
required in reality):

  ((a + _))  ~> %x. a + x
  ((_ + a))  ~> %x. x + a
  ((a + _ + b + _))  ~>  %x y. a + x + b + y
  ((_ < a))  ~> %x. x < a

E.g.

  filter ((_ < a)) list
  map ((_ - a)) list
  All ((_ < a))
  Collect ((_ < a))

We already have implicit underscore treatment for clausal definitions,
so the above would not be totally alien. (But I am not proposing to do
anything concrete now.)


	Makarius