Zulip Chat Archive

Stream: general

Topic: Lean 4 Question


Andre (Nov 04 2021 at 20:24):

If Lean 4 is a programming language how can I understand the how and why of it's ability to create a DSL? The thought intrigues me but I have no idea what it is or where to go.

Patrick Stevens (Nov 04 2021 at 20:53):

Are you aware of what a DSL is?

Andre (Nov 04 2021 at 20:56):

Sort of. I know HTML is a type of DSL. Trying to understand it and organize it is currently the problem.

Julian Berman (Nov 04 2021 at 21:27):

What's leading you to ask the question (what's your goal in learning about them)? HTML is a DSL in the "true" sense of what DSL means, but not in what people normally mean when they talk about DSLs conversationally I think, especially not in the context of a language being able to make DSLs.

Julian Berman (Nov 04 2021 at 21:28):

A DSL is well, what it stands for -- a Domain Specific Language -- so a kind of language invented suitable for a specific (sub)-domain -- HTML for marking up hypertext (in short for laying out web pages more or less)

Julian Berman (Nov 04 2021 at 21:28):

But usually what people mean when they talk about a language, say Lean 4, being suitable for DSLs is whether you can use the constructs in the language (often things like parentheses-less function calling, macros, and little required syntax or boilerplate) to create other languages "embedded" inside valid lean 4 code

Andre (Nov 04 2021 at 21:45):

I suppose I'm curious if I can write my own DSL. I've come across Enso which is a visual interactive way to program.

https://github.com/enso-org/enso

My mind is kinda blown away that I can visually reason about the program and it can check if it's logically sound. I've then found out about:

https://enso-lang.org/

And now I'm trying to understand how this works because I want to create designs that are programmable.

Daniel Fabian (Nov 05 2021 at 08:28):

embedded DSLs in lean remain textual, though. One thing I did a while back, was use mini-parser to write things that closely resembled JSON objects.

This was done, so that I can test a code generation for JSON, so the test looked a lot like the kind of string it was meant to parse.

Eric Wieser (Nov 05 2021 at 08:37):

I'm curious to know how you did that (assuming Lean 3); did you need user_notation?

Patrick Massot (Nov 05 2021 at 09:23):

I'm pretty sure Daniel is talking about Lean 4.

Sebastian Ullrich (Nov 05 2021 at 09:41):

Correct: https://github.com/leanprover/lean4/blob/master/tests/lean/run/toFromJson.lean

Sebastian Ullrich (Nov 05 2021 at 09:42):

It's more of an elaborator than a parser. The parsing is done by Lean 4.


Last updated: Dec 20 2023 at 11:08 UTC