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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
