構造体の定義の曖昧さ問題

[Seasawher]

問題の概要

構造体の定義として以下の４つがありえる。

1. コンストラクタの数が一つであるような、非再帰的な帰納型（TPiL 日本語版で採用されている）
2. コンストラクタの数が一つであるような帰納型
3. structure コマンドで定義できる型
4. structure コマンドで定義できる型と、class コマンドで定義できる型

Lean by Example ではこの問題にいままで気づいていなかった。どの定義を採用するか？

各定義が同値ではないこと

• 1 と 2 は明らかに同じではない。

• 1 と 3 も同じではない。structure コマンドは再帰的な定義を受け入れるからである。

structure Foo where
  name : String
  children : List Foo

• 1 と 4 が同じでないは明らか。

• 2 と 3 が同じでないのは、structure コマンドは Prop 型から Prop ではないフィールドを持たせることを許可しないからである。Lean の標準ライブラリの Exists が inductive で定義されているのはこのため。

structure Exists'.{v} {α : Sort v} (p : α → Prop) : Prop where
  intro ::
  /-
  failed to generate projections for 'Prop' structure, field 'w' is not a proof
  -/
  w : α
  h : p w

• 2 と 4 が同じでないのは明らか。
• 3 と 4 が同じでないのも明らか。

各定義を推す理由

ここでは便宜上、「コンストラクタの数が一つであるような帰納型」を前構造体(prestructure)と呼ぶことにする。これはここだけの用語である。

1. TPiL にそう書かれているし、前構造体であれば無名コンストラクタが使用できる。それに昔は structure で再帰的な定義はできなかった。
2. 再帰的な定義を許可するようになったのは最近の Lean の更新によるものなので、それを取り入れればよいという考え方。
3. それはそう。
4. structure に [class] 属性を付与したものは、#print すると class 扱いになる。また、#synth コマンドにも反応するようになる。したがって、class は structure のサブセットだと見なせるという考え方。なお class inductive で定義した型は、#print すると inductive と表示されるので狭義の型クラスではない、と見做す。

[Seasawher]

Lean by Example で採用する解釈

4 を採用する。根拠として、isStructure という関数があることが挙げられる。

import Lean

open Lean Elab Term

/-- 与えられた型が構造体(structure)であるか判定する -/
def isStructure' (type : Name) : TermElabM Bool := do
  return isStructure (← getEnv) type

#eval isStructure' `And
#eval isStructure' `Exists
#eval isStructure' `Or
#eval isStructure' `Iff
#eval isStructure' `Decidable

これは、#print して class または structure と表示される型を構造体だと定義しているのにおそらく等しい。

この問題が波及する箇所

• TPiL と矛盾する記述があるのであれば、混乱を生むので注釈が必要。
• 無名コンストラクタに関する記述。現在は「構造体に対して使える」という記述になっているが、実際は前構造体に対して利用可能である。
• structure のページの「構造体は、帰納型の特別な場合であり、コンストラクタが一つしかないケースに対応します。」という記述。前構造体と構造体は異なるので、区別が必要。
• class inductive のページに、こうして定義された型クラスは、型クラスではあるが他の型クラスとはちょっと異なるという注釈を入れる必要が生じる。
• [class] 属性( 属性紹介: @[class] 属性 #309 )について解説が必要になる。また、[class] 属性が付与された構造体を「広義の型クラス」と呼ぶなどのわかりやすい名称が必要かもしれない。

[Seasawher]

@aconite-ac さんのご意見により、TPiL 日本語版と合わせて Lean by Example では「構造体とは、単一のコンストラクタを持ち、添字を持たない帰納型」という定義を採用することにします。

この場合 Lean の既存関数で構造体かどうかを判定する方法はなくなり、#print コマンドの出力結果とも矛盾することになる。読者が「構造体とは何か？」という面倒くさい問題を考えずに済むようにしたい。以下の２つが重要そうに思える。

• 読者がある程度自分で判断できるように、この issue で指摘した反例のコードは掲載する。
• 読者に疑問を抱かせないように上手にお茶を濁しつつ、反例の存在を踏まえてうっかり間違った内容を書かない。断定を避けたり、「構造体」という型の話と Lean の実装の話を区別するなど、上手な回避方法をケースバイケースで考えたい。