How to typecheck `let`-expressions?

[re-xyr]

trafficstars

I've been thinking about the details of this. Firstly, if we don't have let-expressions, we only have to detect all definitions at the top-level and submodules and form a dependency graph out of it. However if we have let-expressions, I think the solution is like this:

• Detect all top-level definitions and submodule definitions (but not definitions in let-expressions);
• Form a dependency graph out of them (note that if some def C in some A uses B then A depends on B too);
• When typechecking a definition and we meet a let-expression, we form a dependency graph of the module of the let-expression, typecheck them, and go on.

Why not directly form a dependency graph out of all definitions, including those in the let-expressions?

• We need to ensure that when we typecheck let-expressions, the localCtx has the variables of the outer definition.
• Hence, we should not lift the definitions of let-expressions outside like we did to modules; because this way we could not ensure the localCtx. We should typecheck them only when we meet them, at that time the localCtx will be complete.

Why won't this cause a problem in dependency?

• If the def in let-expression depends on another definition outside, then that definition is also depended on by the outer definition of the let-expression. So when we check the let-expression, its dependencies are all checked too.
• Another definition outside cannot depend on a definition inside let-expression at all.

[ice1000]

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

[ice1000]

We think modules in let being to complicated

[ice1000]

• :+1: for having local modules
• :-1: for simple let like in Arend

@re-xyr is not allowed to cast vote

[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!