DSL mimicking Python

Stream: general

[Petar Maymounkov]

Hi all. In theory, I am curious to what extent can the Lean4 DSL-definition system implement the Python syntax? To put this in context, I wonder if it is possible to introduce Python syntax (as a DSL inside Lean) that is backed by a system of monads, say. Thank you!

[Arthur Paulino]

Do you mean to program in Lean 4 writing things as you would do in Python? Or do you mean to elaborate you DSL to a custom PythonAST inductive?

[Arthur Paulino]

that is backed by a system of monads

I don't understand what that means. Are you referring to an implementation of an evaluation routine for a inductive PythonAST?

[Arthur Paulino]

Something like def PythonAST.eval : PythonAST -> PythonM Value?

Or do you want

def sum_numbers(a: int, b: int) -> int:
    return a + b

to be translated to

def sum_numbers : Int → Int → Int :=
  fun a b => a + b

?

[Sebastian Ullrich]

Petar Maymounkov said:

In theory, I am curious to what extent can the Lean4 DSL-definition system implement the Python syntax?

I'm not terribly familiar with what the gruesome parts of the Python grammar are (whitespace sensitivity is one of them I assume, which we should have roughly covered), but I would say you can already get very close in current Lean 4 except for the lexical grammar, which currently cannot be customized apart from adding keywords. So you will not be able to replicate Python comment syntax, explicit line continuations, or the exact definition of Python identifiers such as it differs from Lean's, for example.

[Petar Maymounkov]

Thank you @Sebastian Ullrich. This answers my question regarding the power of the grammar. @Arthur Paulino Broadly I was curious whether both alternatives are possible. I imagine producing an AST is a given.

To be precise, my main question centered around the expressivity of the DSL grammar mechanics, as in how close can you make the DSL look like Python.

For the second part (producing a monad), I wasn’t expecting an answer since this is probably has a trickier question at its core, which is can Python imperative semantics be converted into monads.