New post: Lean for JavaScript Developers

Stream: new members

[Dan Abramov]

https://overreacted.io/lean-for-javascript-developers/

As always, factual corrections and feedback are appreciated!

[Aaron Liu]

I intentionally did not say “a main function” because main is not a function. (You can hover over it to learn the type of the main but we won’t focus on that today.)

I feel like whether main is a function or not depends on your interpretation of what a function is. Also, main can be a function (it can optionally take the list of command line arguments as a List String).

[Aaron Liu]

(Sidenote: You might also see syntax like fun x ↦ x * 2 rather than fun x => x * 2. Here, ↦ is typed as \maps, and mathematicians prefer it aesthetically to =>. Lean doesn’t distinguish them so you’ll see => in codebases like Lean itself while ↦ shows up in “mathy” codebases like Mathlib. They do exactly the same.)

↦ and => only do the same thing when you're defining a function. If you try to use ↦ in a not-a-function it probably won't work (so for example match n with | 0 ↦ none | n + 1 ↦ some n is a parse error).

[Dan Abramov]

I feel like whether main is a function or not depends on your interpretation of what a function is.

Can you tell me more about this?

[Shreyas Srinivas]

the distinction between functions and values is artificial

[Shreyas Srinivas]

The main you have declared is simply a zero argument function

[Dan Abramov]

Ah, that's fair. I guess I think "zero argument functions don't exist" is maybe a simpler mental model for teaching but maybe not.

[Shreyas Srinivas]

not in lean

[Shreyas Srinivas]

You want people to get accustomed to treating functions as first class citizens right off the bat

[Shreyas Srinivas]

The easiest way to do this is to not give javascript programmers an analogy to javascript's trichotomy between values and functions and closures

[Shreyas Srinivas]

It's very hard to unlearn these intuitions once people learn them (like the monads are burritos tutorials)

[Shreyas Srinivas]

I also recommend not discussing proofs in an intro to lean for programmers

[Shreyas Srinivas]

There's enough to learn on the programming side as it is

[Dan Abramov]

I can see that point but I also think it's very unappealing to most people to learn a new language for no reason, and showing something they couldn't do before serves as a way to hook in some people. Personally I was uninterested in Lean as a programming language until I've seen how the two worlds interact. So I'm trying to strike a balance with this.

[suhr]

Shreyas Srinivas said:

the distinction between functions and values is artificial

Is it? A function is something you can apply to value of one type to get a value of other type. You can't apply 42 : Nat to value of any type, thus it is not a function.

[Kevin Buzzard]

42 isn't a term of a Pi type, which is probably a reasonable definition of function in Lean's type theory

[Aaron Liu]

IO α is IO.RealWorld → EStateM.Result IO.Error IO.RealWorld α (though arguably this is an implementation detail)

[Shreyas Srinivas]

Kevin Buzzard said:

42 isn't a term of a Pi type, which is probably a reasonable definition of function in Lean's type theory

A function is also technically a value in functional languages. You can pass it as arguments to other functions, and produce it as the result of evaluating a function. This wasn’t always the case in imperative languages. Not in a straightforward way.

This idea only became popular in the JavaScript world and several other languages starting in the years around 2010, and they sometimes tacked on new syntax to make it work. The idea itself was older ofc.

[Sebastian Ullrich]

Shreyas Srinivas said:

The main you have declared is simply a zero argument function

Just to make it very explicit, this is not a helpful mental model in a functional language with currying. "Functions are values" is correct and helpful, "values are functions" is not.