ForIn 型クラスを紹介する

以下、公式資料ベースの要点です。なお、公式 Zulip は Web 検索経由では ForIn 自体を解説する有用スレッドを確認できず、実質的な根拠は Functional Programming in Lean と Lean 公式リファレンス です。

結論

ForIn は、Lean の

for x in xs do
...

を動かすための型クラスです。List、Array、Range などの「走査できるもの」に対し、do ブロック内でモナド的に反復する方法を与えます。

公式リファレンス上の本体はこれです。 

class ForIn (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v)) where
forIn :
{β : Type u₁} →
ρ →
β →
(α → β → m (ForInStep β)) →
m β

読み方は次の通りです。

ForIn m ρ α

は、

「モナド m の中で、コレクション型 ρ を、要素型 α として走査できる」

という意味です。

forIn の引数は：

ρ -- 走査対象
β -- ループ内部状態の型
β -- 初期状態
α → β → m (ForInStep β) -- 各要素に対する本体
m β -- 最終状態

ForInStep β は「続けるか、止めるか」を表します。公式リファレンスでは、done は break / return に対応し、yield は通常継続または continue に対応すると説明されています。 

inductive ForInStep (β : Type u) where
| done : β → ForInStep β
| yield : β → ForInStep β

典型例：for は ForIn に脱糖される

Functional Programming in Lean は、for ... in ... do が ForIn に脱糖され、ForIn は ForM より複雑で「状態」と「早期終了」を扱う、と説明しています。 

def sumList (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
acc := acc + x
return acc
#eval sumList [1, 2, 3, 4]
-- 10

これは概念的には次のような状態渡しです。

def sumListExplicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
pure <| ForInStep.yield (acc + x)
#eval sumListExplicit [1, 2, 3, 4]
-- 10

break：ForInStep.done

def sumUntilGreaterThan10 (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x > 10 then
break
acc := acc + x
return acc
#eval sumUntilGreaterThan10 [1, 2, 20, 3]
-- 3

対応するイメージは：

def sumUntilGreaterThan10Explicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
if x > 10 then
pure <| ForInStep.done acc
else
pure <| ForInStep.yield (acc + x)

return：ループだけでなく do ブロック全体から戻る

Functional Programming in Lean では、for ループ内の早期 return を使った List.find? の例が出ています。 

def find? (p : α → Bool) (xs : List α) : Option α := do
for x in xs do
if p x then
return x
failure

例：

#eval find? (fun n => n > 5) [1, 3, 8, 2]
-- some 8
#eval find? (fun n => n > 5) [1, 3, 4]
-- none

continue：今回の反復だけスキップ

同じく公式本では、continue によってループ本体の残りを飛ばせることが説明されています。 

def sumOdds (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x % 2 == 0 then
continue
acc := acc + x
return acc
#eval sumOdds [1, 2, 3, 4, 5]
-- 9

ForM から ForIn を作る

Functional Programming in Lean では、ForM インスタンスから ForM.forIn によって ForIn インスタンスを作れると説明されています。ただし、そのアダプタは内部で StateT と ExceptT を使うため、モナドを一般化している ForM に対して使うものです。 

structure AllLessThan where
num : Nat
def AllLessThan.forM [Monad m]
(coll : AllLessThan)
(action : Nat → m PUnit) : m PUnit := do
let rec countdown : Nat → m PUnit
| 0 => pure ⟨⟩
| n + 1 => do
action n
countdown n
countdown coll.num
instance [Monad m] : ForM m AllLessThan Nat where
forM := AllLessThan.forM
instance [Monad m] : ForIn m AllLessThan Nat where
forIn := ForM.forIn

使用例：

def printLessThanFive : IO Unit := do
for i in ({ num := 5 } : AllLessThan) do
IO.println i
#eval printLessThanFive
-- 4
-- 3
-- 2
-- 1
-- 0

ForIn'：要素がコレクションに属する証拠つきループ

ForIn' は、各反復で a ∈ x の証明も本体に渡す強化版です。公式リファレンスでは、for h : x in xs do ... 形式で使うと説明されています。 

class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v))
(d : outParam (Membership α ρ)) where
forIn' :
{β : Type u₁} →
(x : ρ) →
β →
((a : α) → a ∈ x → β → m (ForInStep β)) →
m β

公式本の例では、範囲 [0:xs.size] を証拠つきで回すことで、xs[i] が安全なアクセスだと Lean に分からせています。 

def printArray [ToString α] (xs : Array α) : IO Unit := do
for h : i in [0:xs.size] do
IO.println s!"{i}:\t{xs[i]}"

ここで h は概念的に：

h : i ∈ [0:xs.size]

であり、Lean はそこから i < xs.size を導けます。

複数コレクションの並列ループ

Functional Programming in Lean は、複数の in 節をカンマで並べると並列に反復し、どれかが尽きた時点で停止すると説明しています。 

def parallelLoop : IO Unit := do
for x in ["currant", "gooseberry", "rowan"], y in [4:8] do
IO.println (x, y)
#eval parallelLoop
-- ("currant", 4)
-- ("gooseberry", 5)
-- ("rowan", 6)

注意：Lean 4.27 以降の変更

Lean 4.27.0 のリリースノートでは、ForIn、ForIn'、ForM のインターフェースが変更され、型クラス自体は Monad m パラメータを取らなくなり、下流の instance 側で [Monad m] を仮定する必要がある、と説明されています。 

したがって、古い記事やコードでは：

instance : ForIn m MyCollection α where
...

の周辺で Monad m の置き方が現在の Lean と合わない場合があります。現在は概ね：

instance [Monad m] : ForIn m MyCollection α where
...

の形に寄せるのが安全です。

まとめ

ForIn は「for x in xs do を使えるようにする型クラス」です。ForM が単純な全要素走査を表すのに対し、ForIn は let mut、break、continue、return を支えるために、内部状態 β と ForInStep β を扱います。証明つきの反復が必要なら ForIn' を使います。

The issue names no target file or test; first locate the repository's existing documentation or example structure and check the proposed snippets against the current Lean 4.27 interfaces. Done means adding a ForIn explanation that covers ForInStep, break, return, continue, ForIn', parallel loops, and the ForIn/ForM changes with working examples.