Functional Programming in Lean 日本語訳

伝統によれば、プログラミング言語は、コンソールに "Hello, world!" と表示するプログラムをコンパイルし、実行することで導入されるべきです。この単純なプログラムは、言語ツールが正しくインストールされ、プログラマがコンパイルされたコードを実行できることを保証します。

しかし、1970年代以降、プログラミングは変わりました。今日、コンパイラは一般的にテキストエディタに統合されており、プログラミング環境はプログラムを書いている最中にフィードバックを提供してくれます。Lean も例外ではありません：Lean は言語サーバープロトコル（LSP：Language Server Protocol）の拡張版を実装していて、テキストエディタと情報交換し、ユーザが入力するたびにフィードバックを提供することができます。

Python・Haskell・JavaScript などのさまざまな言語が、REPL（read-eval-print-loop）を提供しています。REPL は対話的なトップレベル、あるいはブラウザコンソールとしても知られています。REPL 環境内では、ユーザが式や文を入力することができます。そして、プログラミング言語はユーザの入力に基づき計算を実行し、結果を表示します。一方 Lean は、これらの機能をエディタとの対話機能に統合し、プログラムテキスト自体に統合されたフィードバックをテキストエディタ上に表示させるコマンドを提供します。この章では、エディタ内で Lean を操作する方法を簡単に紹介します。次章 Hello, World! ではコマンドラインからバッチモードで Lean を使用する伝統的な方法を説明します。

この本は、Lean をエディタで開きながら、コード例に沿って、そして実際にコード例を入力しながら読むのがベストです。コード例で遊びましょう！そして、何が起こるか見てみましょう！