Fun macro - bulleted argument lists

Stream: lean4

[David Thrane Christiansen]

Earlier today I saw some people using block arguments and single-statement do in Haskell to provide a structured way of providing arguments to a function as if they were bulleted lists. This doesn't work in Lean:

List.map
  do fun x => x + 1
  do [1, 2, 3]

This is because Lean demands a monad even if the desugaring of the do doesn't require it.

However, macros allow me to directly add this feature, rather than repurposing do:

/-- Provide a number of arguments as an indented bulleted list
-/
syntax term "with" many1Indent("•" term) : term

macro_rules
  | `(term| $e with $[• $a:term ]*) => `(term| $e $a*)

#eval
  List.map with
    • fun x => x + 1
    • [1, 2, 3]

It's also possible to use bullet points for other related constructors:

syntax &"List" "with" many1Indent("•" term) : term

macro_rules
  | `(term| List with $[• $a:term ]*) => `(term| [ $a,* ])

#eval
  List.map with
    • fun x => x + 1
    • List with
      • 1
      • 2
      • 88

I thought this was a fun little demo :-) It's probably too obscure for real code, but when list elements or function arguments are themselves large expressions and a let would for some reason make it harder to read, something like this starts getting tempting.

[James Gallicchio]

seems like a fantastic gateway drug leading to structured editors :joy:

[Anatole Dedecker]

Do you know about docs#Id ? It exists precisely to be able to make a monad out of something that isn’t to be able to use do notation. I think you just have to use Id.run do instead of do

[Anatole Dedecker]

But that doesn’t really help here since you’d need parentheses

[Anatole Dedecker]

The other option is to simply use <|

[Ioannis Konstantoulas]

This is lovely.

[Eric Wieser]

I'd argue that this would make more sense with · as the symbol, as this is already used for bullets within proofs

/-- Provide a number of arguments as an indented bulleted list
-/
syntax term "with" many1Indent("·" term) : term

macro_rules
  | `(term| $e with $[· $a:term ]*) => `(term| $e $a*)

#eval
  List.map with
    · fun x => x + 1
    · [1, 2, 3]

[Eric Wieser]

It would be neat if something like

#eval
  List.map with
    f x := x + 1
    l := [1, 2, 3]

were allowed as term version of the syntax

example :=
  List.map f l
where
  f x := x + 1
  l := [1, 2, 3]

or as notation for

let f x := x + 1
let l := [1, 2, 3]
List.map f l

[Ioannis Konstantoulas]

Eric Wieser said:

I'd argue that this would make more sense with · as the symbol, as this is already used for bullets within proofs

/-- Provide a number of arguments as an indented bulleted list
-/
syntax term "with" many1Indent("·" term) : term

macro_rules
  | `(term| $e with $[· $a:term ]*) => `(term| $e $a*)

#eval
  List.map with
    · fun x => x + 1
    · [1, 2, 3]

I would love this, especially if it could help eliminate some parentheses. A lot of the time I have (term-mode) code as follows:

Or.elim p
  (complicated
    stuff)
  (more_complicated
    stuff)

and getting lost in parentheses. It is worse when I have more than two arguments. If I could replace this with the dot, that would be great. Unfortunately, when I add your code to my file, I get hit with tons of errors of the form expected · in match statements.

Any ideas how to fix this error, and if some precedence rule magic can make it work like parentheses?

[Joachim Breitner]

@David Thrane Christiansen , neat! Have you been at the GHC Implementors Workshop 2017? I gave a lightning talk asking for that feature in Haskell (see https://www.joachim-breitner.de/blog/730-Less_parentheses, “Less parentheses 1: Bulleted argument lists”). It’s certainly on my list of syntactic ideas to consider if I ever get to write a new PL.

[Mario Carneiro]

One way you can avoid the parentheses is using tactics:

refine Or.elim p ?_ ?_ -- or apply Or.elim p
· exact complicated stuff
· exact more_complicated stuff

[Ioannis Konstantoulas]

Mario Carneiro said:

One way you can avoid the parentheses is using tactics:

refine Or.elim p ?_ ?_ -- or apply Or.elim p
· exact complicated stuff
· exact more_complicated stuff

This is neat, but using it for arbitrary functions (rather than just theorems) becomes cumbersome; I'd like to have this bulleted argument list for all applications to avoid parentheses.

[Mario Carneiro]

I definitely use refine in this way, even for definitions, mainly to avoid awkwardly nested large subterms by breaking them out into separate blocks

[Mario Carneiro]

bad:

example : (∀ x, x < 0) ↔ Nonempty (∀ y, y = y + 1) :=
  ⟨fun h => ⟨by
    some
    tactics
    here⟩,
  fun ⟨h⟩ => by
    some
    other
    tactics⟩

good:

example : (∀ x, x < 0) ↔ Nonempty (∀ y, y = y + 1) := by
  refine ⟨fun h => ⟨?_⟩, fun ⟨h⟩ => ?_⟩
  · some
    tactics
    here
  · some
    other
    tactics

[Joachim Breitner]

Does that mean that refine works as a term as well, not only in tactic mode? Or did you forget a by?

[Mario Carneiro]

forgot a by

[Ioannis Konstantoulas]

But do you also use it for normal programming? That is what I mean by "general functions"; do you go to tactic mode in order to invoke functions with complicated arguments? I am not saying it's wrong, it just feels a bit too much to me.

[Mario Carneiro]

Yes, sometimes. I would need a more realistic example to evaluate for sure

[Mario Carneiro]

I definitely try to avoid large subexpressions, but in a do block I would more likely accomplish that by binding the subexpressions to let binders

[David Thrane Christiansen]

Joachim Breitner said:

David Thrane Christiansen , neat! Have you been at the GHC Implementors Workshop 2017? I gave a lightning talk asking for that feature in Haskell (see https://www.joachim-breitner.de/blog/730-Less_parentheses, “Less parentheses 1: Bulleted argument lists”). It’s certainly on my list of syntactic ideas to consider if I ever get to write a new PL.

I was not there, unfortunately, but you seem to have made an impact :-)

It's beginning to sound like this quick hack of a macro deserves some more thought, to properly account for implicit arguments and by-name arguments, and then it could even end up being useful!

[Mac Malone]

@David Thrane Christiansen / @Eric Wieser / @Ioannis Konstantoulas Here is version that supports by-name arguments and function sugar:

import Lean.Parser.Term

open Lean
open Parser.Term

def funTk := leading_parser Lean.Parser.unicodeSymbol " ↦ " " => "
syntax funBulletArg := atomic(ident funBinder* (typeSpec)? funTk) term
syntax namedBulletArg := atomic(ident " := ") term

/-- An argument written in bullet form. -/
syntax bulletArg := "· " (namedBulletArg <|> funBulletArg <|> term)

/-- Provide a number of arguments as an indented bulleted list. -/
syntax:lead term:max " with' " ppIndent(many1Indent(ppLine bulletArg)) : term

macro_rules
  | `(term| $e with' $[· $as]*) =>
    as.foldlM (β := Term) (init := e) fun e a =>
      let k := a.raw.getKind
      match k with
      | ``namedBulletArg =>
        match a with
        | `(namedBulletArg| $id:ident := $a) => `($e ($id := $a))
        | _ => Macro.throwErrorAt a s!"ill-formed {k}"
      | ``funBulletArg =>
        match a with
        | `(funBulletArg| $id:ident $bs* $[$ty?]? => $a) =>
          `($e ($id := fun $bs* $[$ty?]? => $a))
        | _ => Macro.throwErrorAt a s!"ill-formed {k}"
      | _ => `($e $(⟨a.raw⟩)) -- term

#eval
  List.map with'
    · α := Nat
    · f x ↦ x + 1
    · [1, 2, 3]

It currently has to use with' to avoid clashing with match's, but this could be solved with a change in core that uses withForbiddenTk in match (and change).

[Eric Wieser]

I'd argue it should be f x := x not f x => x, else it's inconsistent with where and let syntax

[David Thrane Christiansen]

That's pretty great!

I'd tend to agree with @Eric Wieser about the color of the velocipede storage facility.

[Mario Carneiro]

to be fair, lean is quite inconsistent about := vs => elsewhere in the grammar anyway

[Mac Malone]

@Eric Wieser / @David Thrane Christiansen In that case, here you go:

import Lean.Parser.Term

open Lean
open Parser.Term

/-- A bullet argument: A nameable argument with sugar for functions. -/
syntax bulletArg := atomic(ident funBinder* (typeSpec)? " := ")? term

/-- Provide a number of arguments as an indented bulleted list. -/
syntax:lead term:max " with' " ppIndent(many1Indent(ppLine "· " bulletArg)) : term

macro_rules
  | `(term| $e with' $[· $as]*) =>
    as.foldlM (β := Term) (init := e) fun e a =>
      match a with
      | `(bulletArg| $id:ident $bs* $[$ty?]? :=%$dtk $a) =>
        if bs.size > 0 then
          `($e ($id :=%$dtk fun $bs* $[$ty?]? => $a))
        else
          if let some ty := ty? then
            match ty with
            | `(typeSpec| :%$tk $ty) =>
              `($e ($id :=%$dtk ($a :%$tk $ty)))
            | _ => Macro.throwErrorAt ty "ill-formed type specifier"
          else
            `($e ($id :=%$dtk $a))
      | `(bulletArg| $a:term) => `($e $a)
      | _ => Macro.throwErrorAt a "ill-formed bullet argument"

#eval
  List.map with'
    · α := Nat
    · f x := x + 1
    · [1, 2, 3]

[David Thrane Christiansen]

Now we just need to hope this beast never escapes the lab :⁠-⁠)

[Mac Malone]

Note that this syntax could be made simpler by dropping the bullet without introducing significant ambiguity (due to its already space-sensitive nature).

[Mario Carneiro]

aside: I would really like (f x := x + 1) to be legal for regular optional args as well

[Mario Carneiro]

that comes up in particular for (motive := _) args