構造体

プログラムを書く最初のステップは、通常、問題領域の概念を確認し、それをコードで適切に表現することです。ドメイン概念は、他のもっと単純な概念の集まりであることがあります。そういったとき、単純な構成要素をひとつの「パッケージ」にまとめ、意味のある名前をつけると便利でしょう。Lean では、それは構造体(structure)によって実現できます。これは Rust や C の struct、C# でいう record に対応するものです。

構造体を定義すると、Lean は他のどの型にも簡約できない、全く新しい型を導入します。構造体は、同じデータを含んでいても異なる概念を表している可能性があるため、他の型に簡約できない必要があります。例えば、点はデカルト座標か極座標のどちらかを使って表現しても、それぞれ浮動小数点数の組であることは同じです。別々の構造体を定義することで、APIの使用者が混同しにくくなります。

Lean の浮動小数点数型は Float と呼ばれます。浮動小数点数は一般的な記法で記述されます。

#check 1.2

1.2 : Float

#check -454.2123215

-454.2123215 : Float

#check 0.0

0.0 : Float

浮動小数点数が小数点付きで記述されている場合、Lean は Float 型だと推論します。小数点なしで書かれた場合は、型注釈が必要になることがあります。

#check 0

0 : Nat

#check (0 : Float)

0 : Float

デカルト点(Cartesian point)は、x と y という2つの Float 型のフィールドを持つ構造体です。これは structure キーワードを使って宣言されます。

structure Point where
  x : Float
  y : Float
deriving Repr

この宣言の後、Point は新しい構造体型になります。最後の行には deriving Repr と書かれていますが、これは Lean に Point 型の値を表示するコードを生成するよう指示しています。このコードは #eval で使用され、プログラマに評価結果を表示します。 Python での repr 関数と同様のものです。コンパイラが生成した表示コードを上書きすることも可能です。

構造体型の値を作る典型的な方法は、中括弧の中にすべてのフィールドの値を指定することです。デカルト平面(Cartesian plane)の原点とは、x と y がともにゼロとなる場所です：

def origin : Point := { x := 0.0, y := 0.0 }

Point の定義で deriving Repr の行を省略すると、#eval origin を実行しようとしたとき、関数の引数を省略したときと同様のエラーが発生します：

expression
  origin
has type
  Point
but instance
  Lean.MetaEval Point
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

このメッセージは、評価マシンが評価結果をユーザに伝える方法を知らないという意味です。

喜ばしいことに deriving Repr を付け加えれば評価することができ、origin の定義とよく似た結果が #eval origin から出力されます。

{ x := 0.000000, y := 0.000000 }

構造体はデータの集まりを「束ね」、名前を付けて一つの単位として扱うために存在するため、構造体の個々のフィールドを抽出できることも重要です。C 言語や Python, Rust のようにドット記法を用いてこれを行うことができます。

#eval origin.x

0.000000

#eval origin.y

0.000000

ドット記法は、構造体を引数に取る関数を定義するために使用できます。例えば、各座標の値を加算することによって、点の加算を行うことを考えます。#eval addPoints { x := 1.5, y := 32 } { x := -8, y := 0.2 } の評価結果は次のようになるべきです:

{ x := -6.500000, y := 32.200000 }

この addPoints 関数は、p1 と p2 と呼ばれる2つの Point 型の項を引数に取ります。そして返される点は、p1 と p2 の両方の x、y 成分に依存しています:

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

同様に、2点間の距離は、x 成分と y 成分の差の二乗和の平方根であり、次のように書くことができます：

def distance (p1 : Point) (p2 : Point) : Float :=
  Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))

たとえば、(1, 2) と (5, -1) の距離は 5 です。

#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := -1.0 }

5.000000

複数の構造体に同じ名前のフィールドが存在することもありえます。例えば、3次元の点のデータ型を考えます。フィールド x と y は2次元のものと同じ名前にできます。更に同じフィールド名でインスタンス化することができます：

structure Point3D where
  x : Float
  y : Float
  z : Float
deriving Repr

def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }

つまり、中括弧構文を使うためには、構造体に期待される型がわかっていなければなりません。型がわからない場合、Lean は構造体をインスタンス化することができません。たとえば

#check { x := 0.0, y := 0.0 }

は次のようなエラーになります:

invalid {...} notation, expected type is not known

いつものように、型注釈をつけることでこの状況を改善することができます。

#check ({ x := 0.0, y := 0.0 } : Point)

{ x := 0.0, y := 0.0 } : Point

より簡潔な書き方として、Lean では中括弧の中に構造型の注釈を入れることもできます。

#check { x := 0.0, y := 0.0 : Point}

{ x := 0.0, y := 0.0 } : Point

構造体の更新

Point のフィールド x を 0.0 に置き換える関数 zeroX を考えてみてください。だいたいのプログラミング言語では、この操作は x が指すメモリロケーションを新しい値で上書きすることを意味します。しかし、Lean は可変(mutable)な状態を持たないのでした。関数型プログラミングの界隈では、ほとんどの場合この種の文が意味するのは、「x フィールドが新しい値を指し、他のすべてのフィールドが元の値を指す、新しい Point を割り当てる」ということです。zeroX の実装法のひとつは、上記の記述に忠実に、x に新しい値を入れて、y を手動で移すことです：

def zeroX (p : Point) : Point :=
  { x := 0, y := p.y }

しかし、この実装の仕方には欠点があります。まず、構造体に新しいフィールドを追加するとき、フィールドを更新しているすべての個所を修正しなければならず、保守が困難になります。第2に、構造体に同じ型のフィールドが複数含まれている場合、コピー&ペーストのコーディングによってフィールドの内容を重複させてしまったり、入れ替えてしまったりする現実的なリスクがあります。最後に、定型文を書かなければならないのでプログラムが長くなってしまいます。

Lean には、構造体の一部のフィールドだけを置換し、他はそのままにするための便利な構文があります。構造体を初期化する際に with キーワードを付けることです。with の後に現れるフィールドだけが更新されます。例えば zeroX を更新対象の x の値だけで書くことができます:

def zeroX (p : Point) : Point :=
  { p with x := 0 }

この with による構造体を更新する構文は、既存の値は変更しておらず、既存の値とフィールドの一部を共有する新しい値を生成しているということに注意してください。たとえば、fourAndThree という点を考えます:

def fourAndThree : Point :=
  { x := 4.3, y := 3.4 }

fourAndThree を評価し、zeroX を使って更新された値を評価し、再び fourAndThree を評価してみると、元の値が得られます:

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

#eval zeroX fourAndThree

{ x := 0.000000, y := 3.400000 }

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

構造体を更新しても元の値は変更されないので、新しい値を計算することによりコードの理解が難しくなることはありません。古い構造体への参照はすべて、変わらず同じフィールド値を参照し続けます。

舞台裏

すべての構造体には コンストラクタ(constructor) があります。ここで、「コンストラクタ」という用語は混乱を生むかもしれません。Java や Python におけるコンストラクタとは異なり、Lean のコンストラクタは「データ型の初期化時に実行される任意のコード」ではありません。Lean におけるコンストラクタは、新しく割り当てられたデータ構造にデータを集めて格納するだけです。データを前処理したり、無効な引数を拒否したりするカスタムコンストラクタを作ることはできません。このように「コンストラクタ」という言葉の意味は2つの文脈で異なるのですが、しかし関連はあります。

デフォルトでは S という名前の構造体のコンストラクタは S.mk という名前になります。ここで、S は名前空間修飾子、mk はコンストラクタそのものの名前です。中括弧による初期化構文を使う代わりに、コンストラクタを直接使うことができます。

#check Point.mk 1.5 2.8

しかし、一般的にこれは Lean のスタイルとして良いものと考えられていません。Lean は標準的な（中括弧を使った）構文でフィードバックを返します。

{ x := 1.5, y := 2.8 } : Point

コンストラクタは関数型を持っているため、関数が期待される場所であればどこでも使用できます。例えば、Point.mk は2つの Float の項（それぞれ x と y）を受け取り、新しい Point を返す関数です。

#check (Point.mk)

Point.mk : Float → Float → Point

構造体のコンストラクタ名を上書きするには、先頭にコロン2つを付けて書きます。例えば、Point.mk の代わりに Point.point を使うには、次のように書きます：

structure Point where
  point ::
  x : Float
  y : Float
deriving Repr

コンストラクタに加えて、構造体の各フィールドに対してアクセサ関数が定義されます。アクセサ関数は構造体の名前空間でフィールドと同じ名前を持っています。Point については、アクセサ関数 Point.x と Point.y が生成されます。

#check (Point.x)

Point.x : Point → Float

#check (Point.y)

Point.y : Point → Float

実際、構造体を作る中括弧による構文が舞台裏で構造体のコンストラクタを呼ぶように、戦術の addPoints の定義における p1.x は変換されてアクセサ Point.x を呼び出します。つまり、#eval origin.x と #eval Point.x origin の結果は等しく、次が得られます。

0.000000

アクセサドット記法は、構造体のフィールド以外にも使えます。任意の数の引数を取る関数にも使用できます。より一般的に、アクセサ記法は TARGET.f ARG1 ARG2 ... という形をしています。このとき TARGET の型が T であれば、T.f という関数が呼び出されます。TARGET は関数 T.f の型 T を持つ最初の引数になります。多くの場合これは最初の引数ですが、常にではありません。ARG1 ARG2 ... は順に残りの引数として与えられます。例えば String.append は、String が append フィールドを持つ構造体ではないにもかかわらず、アクセサ記法を使って文字列から呼び出すことができます。

#eval "one string".append " and another"

"one string and another"

上記の例では TARGET が "one string" に当たり、ARG1 が " and another" に当たります。

関数 Point.modifyBoth (つまり、Point 名前空間で定義された modifyBoth) は、Point の全てのフィールドに関数を適用します：

def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
  { x := f p.x, y := f p.y }

Point 型の引数は関数型の引数の後に来ていますが、ドット記法でも問題なく使用できます：

#eval fourAndThree.modifyBoth Float.floor

{ x := 4.000000, y := 3.000000 }

この例では TARGET は fourAndThree に当たり、ARG1 は Float.floor に当たります。これは、アクセサ記法のターゲットが、型が一致する最初の引数として使われ、必ずしも最初の引数として使われるとは限らないことによるものです。

演習問題

RectangularPrism(角柱) という名前で、height, width, depth の3つの Float 型のフィールドを持つ構造体を定義してください。

角柱の体積を計算する関数 volume : RectangularPrism → Float を定義してください。

端点をフィールドとして、線分を表す構造体 Segment を定義してください。そして線分の長さを計算する関数 length : Segment → Float を定義してください。なお Segment のフィールドは2つ以下としてください。

RectangularPrism の宣言により、どういう名前が導入されましたか?

以下の Hamster と Book の宣言により、どういう名前が導入されましたか? またその型はどうなっていますか。

structure Hamster where
  name : String
  fluffy : Bool

structure Book where
  makeBook ::
  title : String
  author : String
  price : Float

Functional Programming in Lean 日本語訳

構造体

構造体の更新

舞台裏

演習問題