Lean 4 Question

Stream: general

[Andre]

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]

Are you aware of what a DSL is?

[Andre]

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

[Julian Berman]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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