metaprogramming in Lean

Stream: new members

[Daniel Gavrila]

Hello, my first post here.

I‘ve experience  in C++ for more than  25 years and I‘ve discover Lean a couple of months ago so I have a very basic understanding how is working. 

After long time and a try and error approach seems that C++ will get reflection as is stated in this paper.

I started to read the Metaprogramming in Lean and I‘ve found this statement:

„One cool thing about Lean, though, is that it allows us to define custom syntax nodes and implement meta-level routines to elaborate them in the very same development environment that we use to perform object-level activities“

I understand very well that is not a trivially task to add a complex feature like metaprogramming to a 40+ years old language , my question is why in Lean the metaprogramming looks so „natural“. It was designed from the beginning to have metaprogramming features or this comes as a normal feature because of the Lean  DNA like dependent types, types are first class citizen etc.

[Abraham Solomon]

Daniel Gavrila said:

Hello, my first post here.

I‘ve experience  in C++ for more than  25 years and I‘ve discover Lean a couple of months ago so I have a very basic understanding how is working. 

After long time and a try and error approach seems that C++ will get reflection as is stated in this paper.

I started to read the Metaprogramming in Lean and I‘ve found this statement:

„One cool thing about Lean, though, is that it allows us to define custom syntax nodes and implement meta-level routines to elaborate them in the very same development environment that we use to perform object-level activities“

I understand very well that is not a trivially task to add a complex feature like metaprogramming to a 40+ years old language , my question is why in Lean the metaprogramming looks so „natural“. It was designed from the beginning to have metaprogramming features or this comes as a normal feature because of the Lean  DNA like dependent types, types are first class citizen etc.

You might like:
https://lean-forward.github.io/hitchhikers-guide/2023/

Its good for someone with CPP experience, and has some information about what i think you are asking. Hard to find a simple answer to that i think.

[Michael Bucko]

Abraham Solomon schrieb:

Daniel Gavrila said:

Hello, my first post here.

I‘ve experience  in C++ for more than  25 years and I‘ve discover Lean a couple of months ago so I have a very basic understanding how is working. 

After long time and a try and error approach seems that C++ will get reflection as is stated in this paper.

I started to read the Metaprogramming in Lean and I‘ve found this statement:

„One cool thing about Lean, though, is that it allows us to define custom syntax nodes and implement meta-level routines to elaborate them in the very same development environment that we use to perform object-level activities“

I understand very well that is not a trivially task to add a complex feature like metaprogramming to a 40+ years old language , my question is why in Lean the metaprogramming looks so „natural“. It was designed from the beginning to have metaprogramming features or this comes as a normal feature because of the Lean  DNA like dependent types, types are first class citizen etc.

You might like:
https://lean-forward.github.io/hitchhikers-guide/2023/

Its good for someone with CPP experience, and has some information about what i think you are asking. Hard to find a simple answer to that i think.

Thanks for sharing this! I'll read it for sure