What does 'statically typed' and 'dynamically typed' mean?

Stream: new members

[Ken Lee]

This is a more comp-sci question but : when I have a Lean file open in VS code, is Lean "always running" or "always compiling"? what's the diff between "run-time" and "compile-time"? Follow up Q : is Lean "dynamically typed" or "statically typed"?

[Huỳnh Trần Khanh]

lean is statically typed. I don't think the runtime/compile time distinction really applies to Lean 3, though this might change in Lean 4

[Huỳnh Trần Khanh]

lean proofs can be interactively checked by the language server (for example, if you are composing a proof in vscode) and they can also be compiled to olean files to precompute certain things for efficiency. when proofs are compiled to oleans, the time needed to check the proofs when you open vscode and interact with lean through the language server is significantly reduced because the language server can take advantage of the precomputation results stored in the olean files

[Ken Lee]

Huỳnh Trần Khanh said:

lean proofs can be interactively checked by the language server (for example, if you are composing a proof in vscode) and they can also be compiled to olean files to precompute certain things for efficiency. when proofs are compiled to oleans, the time needed to check the proofs when you open vscode and interact with lean through the language server is significantly reduced because the language server can take advantage of the precomputation results stored in the olean files

oh, I didn't know of this "language server" component. This is the thing that's checking the typing judgements?

[Huỳnh Trần Khanh]

yeah vscode interacts with the language server through STDIN/STDOUT. the word "server" is used here because the language server "serves" vscode, it doesn't mean that the language server is listening on a tcp port and accepting network connections

[Ken Lee]

so it looks more like "vscode <-- language server <-- Lean"? I thought the "compiling" is the "type checking" though?

[Kevin Buzzard]

I think the Lean type checkers like Trepplein etc do a lot less than Lean, which runs algorithms like ring etc.

[Huỳnh Trần Khanh]

no compiling is not type checking at all. and the language server _is_ lean :joy: it's an interface that lean provides

[Ken Lee]

maybe what I'm looking for is an overview of what happens from when I write example : N -> N := to the orange(?) line appearing in vscode saying I've forgotten something.

[Huỳnh Trần Khanh]

read this to sate your curiosity https://microsoft.github.io/language-server-protocol/

[Yakov Pechersky]

I think there is some confusion here. Lean (discussing lean 3) has a server mode lean --server. When you have a .lean file open in VSCode, the VSCode extension that understands lean files can spawn such a server. When viewing a file, VSCode passes information to the server using the LSP, and displays messages/results it receives, also via the LSP

[Yakov Pechersky]

The thing that is doing the "typing judgements" is the Lean server. The server has loaded in code (either interpreted from .lean files or from "compiled" .olean files), so it can understand the text VSCode is sending it. It sends back information, like tactic state, types, etc.

[Bryan Gin-ge Chen]

(Note that Lean 3's server doesn't use the LSP, but its own protocol. Lean 4's server does use the LSP.)

[Yakov Pechersky]

The orange line is a way that VSCode is interpreting an issue that is expressed using the protocol of communication. The issue was generated by Lean, given the line(s) VSCode made available to it. Additionally, the issue has information about where in the file the issue is at, which VSCode provides visually as the orange line.

[Ken Lee]

so pictorially... "current-file-in-vscode <--> Lean-server <-- oleans", where the Lean-server is Lean, the typing-judgements established coming from oleans as well as current-file-in-vscode?

[Yakov Pechersky]

I think so

[Ken Lee]

waait, so Lean-server is running "real time"? but this doesn't count as the "code running"?

(I apologise for my ignorance about computers :sweat: )

[Huỳnh Trần Khanh]

in some sense... this does count as the code running. some parts of proof checking involve running algorithms in a bytecode virtual machine

[Huỳnh Trần Khanh]

and generally speaking the lean language server is happy to run every algorithm you throw at it provided that the algorithm doesn't take too much time

[Huỳnh Trần Khanh]

docs#data.list.merge_sort for example is an algorithm

[Huỳnh Trần Khanh]

oops i mean https://leanprover-community.github.io/mathlib_docs/data/list/sort.html#list.merge_sort

[Ken Lee]

so is it more like... we're constantly "debugging" and Lean-server is the thing that helps us do that? (I confess I don't exactly know what 'debugging' means either.)

[Huỳnh Trần Khanh]

yes. we're constantly debugging. lean is a revolutionary programming language: the programming environment constantly verifies and executes the program

[Huỳnh Trần Khanh]

get used to the new normal

[Huỳnh Trần Khanh]

you'll never want to code in a traditional programming language ever again :joy:

[Julian Berman]

Revolution aside :P, I'd kind of look at it quite similarly to a traditional web application.

[Julian Berman]

When you edit a file, that's like making a web request to a web server, and the web server gets back to you with some response.