First maintenance release of Functional Programming in Lean

Stream: general

[David Thrane Christiansen]

I'm happy to announce the first maintenance release of Functional Programming in Lean, an introductory book on using Lean as a programming language, which is intended to serve both programmers wanting to get into theorem proving and mathematicians wondering what this monad transformer thing is and why it's helpful for proof automation. In this release, a number of mistakes have been fixed and the text has been brought up to date with the changes in Lean version 4.1.0.

It's here: https://lean-lang.org/functional_programming_in_lean/

[Ioannis Konstantoulas]

Thank you very much for this update; without FPIL, I would have never gotten around to using Lean.

[Filippo A. E. Nuccio]

I am posting here a question about Section 2.2, but I wonder whether this is the right place (@David Thrane Christiansen : should FPIL have a dedicated stream?). I start by saying that I am a complete newby insofar "programming" is concerned, and I find the book deeply inspiring, incredibly well written and very clear: I am really sure my misunderstanding comes from my utter ignorance.

I am trying to understand the code

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

and I am puzzled about the usefulness of the first two lines. AFAIU, at the point where let stdin ← IO.getStdin is executed, no input has been provided (and similarly, when let stdout ← IO.getStdout is executed, no output exists yet). So, I do not understand what stdin and stdout really are after this execution. I suspect that (part of) my misunderstanding comes from a confusion about this IO business. In particular, although I have appreciated the "cook vs. counter worker" metaphor in 2.1, I have the impression that no definition of what an "effect" or "side effect" was given. So the sentence

The cook's notes represent IO actions that are produced by evaluating Lean expressions, and the counter worker's replies are the values that are passed back from effects.

is very dense for me: I really do not know neither what IO actions nor what effects are.

[Mario Carneiro]

So, I do not understand what stdin and stdout really are after this execution.

They are "handles", to the input and output streams respectively. This controls whether your putStrLn goes to the console output, as compared to the output of a child process, a file, or some other thing

[Mario Carneiro]

in this context an "effect" is something like a change in the state of the real world, e.g. the words How would you like to be addressed? appearing on your console

[Mario Carneiro]

IO actions are the elements of type IO A, they represent instructions to do a thing in the real world (an effect) and then report a result back (of type A)

[Mario Carneiro]

for example IO.getStdout is an IO action which (describes the act of) going and retrieving a handle to the current console output stream, and stdout.putStrLn "How would you like to be addressed?" is an IO action which (describes the act of) printing How would you like to be addressed? to the stream identified by the stdout handle

[Filippo A. E. Nuccio]

Ah ok. So the actions that print the lines "Hi there!" into a .tex file or into a .txt file would both be represented by some IO term (probably of different, but similar type)?

[Mario Carneiro]

they would probably have the same type, namely IO Unit

[Mario Carneiro]

which is the type of all IO actions that do a thing in the real world and return no result

[Mario Carneiro]

they would have different bodies though (they would be different terms of this type)

[Filippo A. E. Nuccio]

Ah, so " writing something in the console/in a text file" is not a result?

[Mario Carneiro]

no, the result is the pure value produced as a result of the action, this is usually bound to a variable with the let x <- action syntax

[Mario Carneiro]

so IO.getStdout is an action with a result (the output stream which we bind to variable stdout), while stdout.putStrLn "..." has no result (or rather, it has a result of type Unit that we don't bother to bind to a variable)

[Mario Carneiro]

it has an effect on the real world, but it doesn't pass any pure values back to the code

[Filippo A. E. Nuccio]

Mario Carneiro said:

it has an effect on the real world, but it doesn't pass any pure values back to the code

Oh, I guess that the "back" in this sentence is crucial.

[Filippo A. E. Nuccio]

Do you have an example of an action of type IO Nat, if that makes any sense at all?

[Mario Carneiro]

def foo : IO Nat := IO.getNumHeartbeats

this gets some global state (the current state of the heartbeat counter)

[Mario Carneiro]

Anything with some kind of nondeterminism or real-world-state dependence is going to be an IO A

[Mario Carneiro]

because lean functions have to be pure functions, you can't have a Unit -> Nat function which returns a different value every time you run it

[Mario Carneiro]

but foo is effectively that, if you do

#eval do
  let x ← foo
  let y ← foo
  println! "{x} =?= {y}"

then there is no guarantee that x and y end up with the same value

[Filippo A. E. Nuccio]

Oh, I see. So

def foo : fun n => n+1

has type Nat -> Nat while

def bar : fun n => n + IO.getWeekNumber

(supposing that IO.getWeekNumber exists, for the sake of this example) is of type Nat -> IO Nat?

[Filippo A. E. Nuccio]

Mario Carneiro said:

because lean functions have to be pure functions, you can't have a Unit -> Nat function which returns a different value every time you run it

Can you speculate a bit about your use of "pure" here? What kind of gadget would you qualify as "non-pure function"?

[Mario Carneiro]

You also have to use bind in order to "sequence" IO actions, unlike pure functions. n + IO.getWeekNumber does not typecheck because IO.getWeekNumber has type IO Nat, not Nat. The correct way to write a function of type Nat -> IO Nat there is

def bar : Nat -> IO Nat := fun n => do
  let w <- IO.getWeekNumber
  return n + w

where do is sugar for a usage of the bind function, which is used to compose IO actions together

[Mario Carneiro]

A "pure function" is one whose type is not a monad thing like A -> IO B, it's just A -> B

[Filippo A. E. Nuccio]

Mario Carneiro said:

You also have to use bind in order to "sequence" IO actions, unlike pure functions. n + IO.getWeekNumber does not typecheck because IO.getWeekNumber has type IO Nat, not Nat. The correct way to write a function of type Nat -> IO Nat there is

def bar : Nat -> IO Nat := fun n => do
  let w <- IO.getWeekNumber
  return n + w

where do is sugar for a usage of the bind function, which is used to compose IO actions together

Wow, this is enlightening. Thanks!

[Filippo A. E. Nuccio]

Mario Carneiro said:

A "pure function" is one whose type is not a monad thing like A -> IO B, it's just A -> B

But then the term you constructed above of type Nat -> IO Nat is what? Not a function?

[Mario Carneiro]

You can think of A -> IO B as a pure function, but it is a pure function for producing an "IO action" of type IO B, it doesn't actually do the thing that this action describes. So for the same input it's always the same IO action output, but the resulting IO action may have different results when actually performing its effect using #eval or similar

[Filippo A. E. Nuccio]

Ah! Got it!

[Mario Carneiro]

an IO Nat is not a number, it is instructions for how you might get a number if you ask the universe to help

[Filippo A. E. Nuccio]

Yes, I see now. You are saying that from the lean-theoretic point of view it is a honest function assigning to every input the same output, but this output is the action, not the result of the action. And the same action can yield different results when performed at different moments, for instance. Right?

[Filippo A. E. Nuccio]

Thanks! I can dive back in some exercice and try not to drown... :sea_lion:

[Filippo A. E. Nuccio]

(As an aside: is IO short for Input-Output, or completely unrelated?)

[Mario Carneiro]

it is indeed input/output

[Kevin Buzzard]

Filippo A. E. Nuccio said:

Oh, I see. So

def foo : fun n => n+1

has type Nat -> Nat while

def bar : fun n => n + IO.getWeekNumber

(supposing that IO.getWeekNumber exists, for the sake of this example) is of type Nat -> IO Nat?

Filippo -- did you know that WithBot is a monad? You can think of WithBot Nat as "naturals + $-\infty$", but you can also think of them as "a Nat, or perhaps a failure" and then you can just add these things up, but failure + x = failure. But there's a coercion from Nat to WithBot Nat and in the context of monads I think this is function is called pure. WithBot (which is really Option) is a great beginner example of a monad. It also shows that you can't get out of the monad: if you have a term of type WithBot Natyou can't just say "OK but what is the actual Nat?" because the answer might be "oh we failed in the calculation 10 lines up, so there is no Nat any more"

[Filippo A. E. Nuccio]

Oh, never though at WithBot as a monad! Thanks for the insight.

[Agnishom Chattopadhyay]

Out of curiosity, how ready is Lean for general purpose programming? (i.e, writing executable programs and not just proving theorems)

[Matthew Ballard]

Multiple people have done Advent of Code with it, for example.

[Matthew Ballard]

I would say very ready

[Jireh Loreaux]

Indeed, very ready, as it is now being used even by AWS for the Cedar model.

[Agnishom Chattopadhyay]

That's really cool. I am very happy to see a general purpose programming language and a very competent theorem proving environment in one ecosystem. I googled and found this and this

[Agnishom Chattopadhyay]

Jireh Loreaux said:

Indeed, very ready, as it is now being used even by AWS for the Cedar model.

It seems that they are proving theorems about Cedar, rather than implement Cedar itself in Lean. GitHub Link

[Daniil Kisel]

There is an article describing building of a simple web API for a competition.

[Jireh Loreaux]

Right, I said it was used for the Cedar model. But of course that model includes the full specification of Cedar. See the cedar-spec/cedar-lean/Cedar/Spec directory.

[Patrick Massot]

Agnishom Chattopadhyay said:

Out of curiosity, how ready is Lean for general purpose programming? (i.e, writing executable programs and not just proving theorems)

Lean as a programming language is already really nice, but don't expect that libraries exists. You can currently use it if you have no dependency at all (or use it to create a basic library). For instance you won't have regular expressions or http requests. So you need to think carefully before starting a project.

[Adam Topaz]

Right. The main thing missing is libraries. Also, it's a bit dangerous to program in Lean4... once you do it for a while, you realize how much better it is than any other programming language.

[Filippo A. E. Nuccio]

Mario Carneiro said:

IO actions are the elements of type IO A, they represent instructions to do a thing in the real world (an effect) and then report a result back (of type A)

@Mario Carneiro Retrieving this discussion, I have been thinking about this and I still don't understand well when reading FPIL: the definition there is

IO α is the type of a program that, when executed, will either throw an exception or return a value of type α

and I do not understand the role of the "exception" when comparing with your definition. For instance, IO Unit should either throw an exception or a term of type Unit. Now, looking at

def main : IO Unit := IO.println "Hello, world!"

how should I interpret the role of the "exception"?

[Mario Carneiro]

IO A is actually defined as BaseIO (Except IO.Error A), where BaseIO is what I described and Except is another monad (it's equivalent to Sum but with constructors named .ok and .error instead of the more generic .inl and .inr) which expresses the possibility of failure. So an IO action can perform an effect and then return a failure of type IO.Error instead of an actual value of type A

[Filippo A. E. Nuccio]

And in the above case with main, when would this failure be returned?

[Mario Carneiro]

It would be produced by main when you execute it

[Mario Carneiro]

println might throw an error if the underlying stream is closed, for example

[Mario Carneiro]

or if you are piping the output to a file and you run out of disk space

[Mario Carneiro]

the lean runtime, which is the one responsible for running main, checks if this IO action returned an error and if so it prints some information about it to the console and exits with an error code

[Mario Carneiro]

or if you run main by just using #eval main, the lean server is the one that catches this error and draws a red squiggle over the command and shows the error message in the infoview

[Filippo A. E. Nuccio]

Oh I see.

[Filippo A. E. Nuccio]

On the other hand, your example

def foo : IO Nat := IO.getNumHeartbeats

certainly produces a Nat, but does it also have a side effect?

[Mario Carneiro]

It actually does, since if you run it twice you get different numbers

[Mario Carneiro]

it has the effect of increasing the number of heartbeats by 1 :)

[Filippo A. E. Nuccio]

Well, but this is the same for everything I do, even if it is not a IO action, no?

[Mario Carneiro]

But in general IO actions aren't required to have an effect. In particular pure x is an IO action that has no effect and returns x

[Mario Carneiro]

Filippo A. E. Nuccio said:

Well, but this is the same for everything I do, even if it is not a IO action, no?

This is a bit complicated. For things that aren't IO actions, any effects they have in reality (like allocations or consuming CPU cycles) are not observable from the lean type system

[Mario Carneiro]

this is actually more a statement about what lean can (or cannot) express than it is about what effects programs have

[Filippo A. E. Nuccio]

Oh, I see, very clear. Thanks again, I'll go back to the book!

[Mario Carneiro]

for example pointer equality is not observable as far as lean is concerned, because if you could observe it you can prove false

[Filippo A. E. Nuccio]

Wow, now you made me curious... why?

[Mario Carneiro]

Because you can create the same object twice in different locations, and lean will say that these objects are equal but the "address of" operation applied to them results in different values, which violates the congruence property of equality: applying a function to equal things yields equal results

[Filippo A. E. Nuccio]

Nice!

[Mario Carneiro]

Nevertheless, observing addresses and pointer equality is sometimes useful or necessary, so lean has these functions anyway... but they are marked as unsafe: docs#ptrAddrUnsafe

[Filippo A. E. Nuccio]

I see, but we are steadily climbing beyond my paygrade now! :sweat_smile:

[Siddhartha Gadgil]

A simple case one gets IO Nat is in generating a random number. In my course I first grumbled about this and then realized that it was for a very good reason, since we want:

• different invocations to give different values.
• A function applied to equal arguments give equal results.

One can "run" to a Nat but then it is clear that we have a state argument which is different for different invocations.

Personally (as a mathematician) I found this example useful for understanding as there is no need for a real world :smile: to justify needing state. Indeed, in my course I made a simple example separating only the relevant part of IO: https://github.com/siddhartha-gadgil/proofs-and-programs-2023/blob/2d3312143811f0679175c2614e454ad6d163608f/PnP2023/Lec_03_24/Sampling.lean#L100

[Filippo A. E. Nuccio]

And this example is the rand or the run function? Do you happen to have recorded your course?

[Siddhartha Gadgil]

Filippo A. E. Nuccio said:

And this example is the rand or the run function? Do you happen to have recorded your course?

This example is to show state being used. The rand function is like Lean's built in one, in that it gives a monadic value. Here it is RandomM Nat instead of IO Nat of Lean. The run is one that can get us out of the Monad, or in general to one level below (TermElabM to MetaM to CoreM ...). Because the Monad here is a simple one the result of running is the pure value, without having to fall back to error.

I haven't recorded my course, though I did use Docgen4 to create docs: https://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html with many details.

[Filippo A. E. Nuccio]

Thanks!

[David Thrane Christiansen]

I'm catching up a bit on Zulip after a week of heads-down concentrated coding - thank you all for taking such good care of @Filippo A. E. Nuccio 's questions!

@Filippo A. E. Nuccio - thank you for reading the book carefully, and for showing up here with questions. It makes me very happy that you're getting value out of it, and that you're putting as much work into reading it as went into writing it. You've basically skipped ahead to chapter 5 in this discussion session :-)

Thanks again!

[Filippo A. E. Nuccio]

Thank you for writing it (and to all the people who helped me, of course)! I am now trying to attack your cat/feline/(will there be tigers? lions? :tiger: ) example, with some struggle and much fun. You'll certainly see more questions.