Asta Halkjær From @ahfrom@types.pl

_Functional Programming in Lean_ is now done and out the door!

It's a free online book that describes using the interactive theorem prover Lean 4 as a programming language, without assuming any background in functional programming. You don't need to already know Haskell, OCaml, Rust, Scala, or Racket to read this book.

You can read it at https://leanprover.github.io/functional_programming_in_lean/ .

Thank you to everyone who's carefully read prereleases - it's much, much better than it otherwise would have been. The Lean Zulip is a great place to hang out.

Also, thanks to MSR for supporting this project, and to Leonardo de Moura for initiating it. It's been a lot of fun!

@JadeMasterMath @mc

It's subtler than that. Each type has its own identity type.

But the identity type is defined in a uniform way for all types, by the data (Id, refl, J, +conversion rules).

But then, you can *prove* characterizations of the identity types for different types.

For the type of natural numbers, for example, the identity type gives the notion of equality you would expect, which you can define by induction on natural numbers.

For a type universe (a larger type of small types), univalence says that identifications are in 1-1 correspondence with bijections.

For the type of groups, you can prove that identifications are in 1-1 correspondence with group isomorphisms.

For the type of subgroups of a given ambient group, you can prove that equality of two subgroups is "having the same elements of the ambient group" (not isomorphism!).

Now what is common about *all* identity types of any type, is that you can "transport".

Let's write Id x y for the type of identifications of x and y (rather than x=y). Then the transport theorem is that

Id x y and P x together imply P y.

Here P x can be a property of x, but it can also be data on x.

So, for example, if you have two types X and Y and P X is "group structure on X", then, because of the above characterization of identities in the type of types, the transport theorem says that from a group structure on X you get a group structure on Y.

But the point is that transport can be applied not only to isomorphism, but to any kind of identification.

​