🦆

Lean 入門 (9)

2026/01/03に公開

Lean

Lean 4

tech

Functional Programming in Lean を読みます。

2. Hello, World!

この章は Lean 4 で実際のプログラムを実行・ビルドする方法を解説した実践的な章です。

ここでは純粋関数型言語であるLeanがどのように入出力（I/O）などの副作用を扱い、スタンドアロンなプログラムを作成するかを焦点に当てています。Lean のツールチェーン（lake ビルドシステムなど）の使い方を学び、簡単なコマンドラインツールを作成します。

2.1. Running a Program

ここでは実行可能なプログラムを書く方法を学びます。Hello.lean を実行します。

Hello.lean

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

$ lean --run Hello.lean
Hello, world!

Leanは純粋関数型言語なので、すべての式は数学的な値として評価され、通常の手続き型言語の様には副作用（標準出力への書き込み、ファイル操作など）を扱えません。そこで Lean は IO モナドを使って副作用を安全にカプセル化します（この辺は Haskell とかと良く似てます）。

main : IO Unit という型の関数を定義すると、それがプログラムのエントリポイントになります。例として、シンプルなHello Worldプログラム：

2.2 Step By Step

もうちょっと複雑な、入力と出力を伴うコードはこんな感じになります。

これは標準入力から1行読み、標準出力にエコーします。do 記法で IO アクションを逐次的に記述可能です。

HelloName.lean

def main : IO Unit := do
  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}!"

$ lean --run HelloName.lean
How would you like to be addressed?
tmiya
Hello, tmiya!

2.3. Starting a Project

まず lake new {project名} でプロジェクトを作ります。以下のファイルが自動生成されます。

$ lake new greeting
$ tree greeting/
greeting/
├── Greeting
│   └── Basic.lean
├── Greeting.lean
├── Main.lean
├── README.md
├── lakefile.toml
└── lean-toolchain

lean-toolchain には使用してるヴァージョン情報とかが書かれます。

$ cat lean-toolchain 
leanprover/lean4:v4.26.0

lakefile.toml はビルドに必要な情報です。

$ cat lakefile.toml 
name = "greeting"
version = "0.1.0"
defaultTargets = ["greeting"]

[[lean_lib]]
name = "Greeting"

[[lean_exe]]
name = "greeting"
root = "Main"

Greeting.lean は Greeting ライブラリのルートになります。実装とかは Greeting/ 下のファイルに書きます。

$ cat Greeting.lean 
-- This module serves as the root of the `Greeting` library.
-- Import modules here that should be built as part of the library.
import Greeting.Basic
$ cat Greeting/Basic.lean 
def hello := "world"
$

Main.lean はプログラムのルートになります(と、toml ファイルに書かれてる)。

Main.lean

import Greeting

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

とりあえずビルドして実行します。ビルドすると、C のコードを経て実行ファイルが作られている様です。

$ lake build
$ lake exe greeting
Hello, world!
$ tree .lake/build
.lake/build
├── bin
│   ├── greeting
│   ├── greeting.hash
│   └── greeting.trace
├── ir
│   ├── Greeting
│   │   ├── Basic.c
│   │   ├── Basic.c.hash
│   │   ├── Basic.c.o.export
│   │   ├── Basic.c.o.export.hash
│   │   ├── Basic.c.o.export.trace
│   │   └── Basic.setup.json
│   ├── Greeting.c
│   ├── Greeting.c.hash
│   ├── Greeting.c.o.export
│   ├── Greeting.c.o.export.hash
│   ├── Greeting.c.o.export.trace
│   ├── Greeting.setup.json
│   ├── Main.c
│   ├── Main.c.hash
│   ├── Main.c.o.export
│   ├── Main.c.o.export.hash
│   ├── Main.c.o.export.trace
│   └── Main.setup.json
└── lib
    └── lean
        ├── Greeting
        │   ├── Basic.ilean
        │   ├── Basic.ilean.hash
        │   ├── Basic.olean
        │   ├── Basic.olean.hash
        │   └── Basic.trace
        ├── Greeting.ilean
        ├── Greeting.ilean.hash
        ├── Greeting.olean
        ├── Greeting.olean.hash
        ├── Greeting.trace
        ├── Main.ilean
        ├── Main.ilean.hash
        ├── Main.olean
        ├── Main.olean.hash
        └── Main.trace

次に、Greeting ライブラリに、Greeting/Smile.lean を追加します。

Greeting/Smile.lean

def Expression.happy : String := "a big smile"

この happy 関数を使うように Main.lean を修正します。

Main.lean

import Greeting
import Greeting.Smile

open Expression

def main : IO Unit :=
  IO.println s!"Hello, {hello}, with {happy}!"

特に toml ファイルは修正の必要はなく、ビルド出来ます。

$ lake build
$ lake exe greeting
Hello, world, with a big smile!
$

2.4. Worked Example: cat

ここでは cat コマンドに似た feline コマンドを作ります。

まずプロジェクトを作成。

$ lake new feline
$ lake build
$ lake exe feline

Main.lean を修正します。

dump 関数は再帰関数ですが、停止性が保証されません（stream が終わる保証がない）ので、partial を付ける必要があります。
その他はテキストを読んで下さい。基本的には I/O 関係やシステム関係のライブラリの使い方を調べれば納得いくと思います。

Main.lean

def bufsize : USize := 20 * 1024

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf <- stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout <- IO.getStdout
    stdout.write buf
    dump stream

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists <- filename.pathExists
  if not fileExists then
    let stderr <- IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle <- IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "-" :: args =>
    let stdin <- IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream <- fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ =>  process 0 args

2.5. Additional Conveniences

多くの IO 関数で、結果を一時的に変数に束縛してすぐに使用するパターンが繰り返されます。このセクションでは、そんな冗長さを避けるための「nested actions」を紹介します。これは、括弧内の ← を使った式を、外側のdoブロックに自動的に持ち上げ、ユニークな名前で束縛します。

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  if not (← filename.pathExists) then
    (← IO.getStderr).putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read

Lean の do ブロックは通常、ホワイトスペース依存（新しい行でインデント一致）ですが、まれにレイアウトを柔軟にしたい場合があります。このセクションでは、セミコロン（;）と中括弧（{}）を使った代替記法もあります。
#evalコマンドは通常、式を評価して文字列表現を表示しますが、IOアクションに対してはアクションを実行し、副作用を発生させます。

2.6. Summary

評価と実行の違い、do 記法、プログラムをコンパイルして実行すること、停止性が保証されない関数には partial を付ける必要があること、を学びました。

開発をさらに快適にする機能の紹介：IO.appPath で実行ファイルパス取得。
環境変数アクセス。
プロセス実行（IO.Process.run）。
lakeのキャッシュやインクリメンタルビルド。
テストフレームワークの簡単な使い方。

また、partial def で部分関数を安全に定義する方法や、コマンドラインオプション解析ライブラリの言及も。実践的なTipsが多く、プロジェクトをスケールさせるための準備を整えます。

2. Hello, World!

2.1. Running a Program

2.2 Step By Step

2.3. Starting a Project

2.4. Worked Example: cat

2.5. Additional Conveniences

2.6. Summary

Discussion