How to typecheck `let`-expressions?

[re-xyr]

How to typecheck `let`-expressions?

[ice1000]

• 👍 for having local modules
• 👎 for simple let like in Arend

@re-xyr is not allowed to cast vote

[ice1000]

During Walpurgis night, we decide to go to Arend style let

[ice1000]

We think modules in let being to complicated

[re-xyr]

I thought about let-expressions. If it is going to be so weak (only provide aliases for terms), we can implement it simply as a syntactic sugar. It can be directly desugared to lambda in the parser and we need not change anywhere else; or it can also be converted to lambda in typechecking.

[ice1000]

Sometimes we want let bindings to be irreducible within the body (and only reduce when applied)

[re-xyr]

Like when?

[ice1000]

Like when?

In Arend they have \have. You can check it out

[re-xyr]

I read about it but don’t know when we would want to use it. Do other languages have this feature too?

[ice1000]

@re-xyr Idk but it's used a lot in the stdlib

[re-xyr]

If we translate let to lambda, it will be like \have. We should substitute the let variables into the term at the concrete stage to get \let.

[ice1000]

@re-xyr I wonder which one is useful

[re-xyr]

Maybe you could ask valis?

[ice1000]

Fixed!