多相性

ほとんどの言語と同じように、Leanの型も引数を取ることができます。例えば、List Nat 型は自然数のリストを意味し、List String 型は文字列のリストを、List (List Point) 型は点のリストのリストを意味します。これはC#やJavaのような言語における型の書き方である List<Nat> 、List<String> 、List<List<Point>> に非常に似ています。Leanが関数に引数を渡すときにスペースを使うように、型に引数を渡すときにもスペースを使います。

関数型プログラミングでは、多相性 （polymorphism）という用語は通常、引数に型をとるデータ型や定義を指します。これはスーパークラスのふるまいをオーバーライドするサブクラスのことを多相性とするオブジェクト指向プログラミングのコミュニティとは異なる点です。本書では、「多相性」は常に最初の意味を指します。これらの型引数はデータ型や定義で使用することができ、引数の名前をほかの型に置き換えることで、同じデータ型や定義を任意の型で使用できるようになります。

Point 構造体は x と y フィールドの両方が Float 型である必要があります。しかし、点は各座標の表現に特化している必要はありません。Point の多相バージョン PPoint は、型を引数として受け取り、その型を両方のフィールドに使用することができます：

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

関数定義の引数が定義された関数名の直後に書かれるように、構造体の引数も構造体名の直後に書かれます。引数自体から示唆される具体的な名前がない場合には、Leanの型引数名にはギリシャ文字を使うのが通例です。型 Type はほかの型を記述する型であるため、Nat や List String 、Point Int はすべて Type 型を持ちます。

List 型のように、PPoint も引数に特定の型を指定することで使用できます：

def natOrigin : PPoint Nat :=
  { x := Nat.zero, y := Nat.zero }

この例では、両方のフィールドが Nat であることが期待されます。関数が引数の変数を引数の値に置き換えて呼び出されるのと同じように、PPoint に Nat 型を引数として与えると、引数名 α が引数の型 Nat に置き換えられることでフィールド x と y が Nat 型を持つ構造体が生成されます。型はLeanでは普通の式であるため、（ PPoint 型のような）多相型に引数を渡すときに特別な構文は必要ありません。

定義は引数として型を取ることもでき、それによって多相なものになります。replaceX は PPoint の x フィールドを新しい値に置き換える関数です。replaceX が 任意の 多相な点で動作するようにするには、replaceX 自身が多相でなければなりません。これは、最初の引数をポイントのフィールドの型とし、それ以降の引数は最初の引数の名前を参照することで実現されます。

def replaceX (α : Type) (point : PPoint α) (newX : α) : PPoint α :=
  { point with x := newX }

言い換えると、引数 point と newX の型が α を参照している場合、それらは 最初の引数として提供されたいずれかの型 を参照していることになります。これは、関数の引数名が関数内に現れたときに、提供された値を参照する方法と似ています。

この事実は replaceX の型をチェックし、次に replaceX Nat の型をチェックすることで確認できます。

#check (replaceX)

replaceX : (α : Type) → PPoint α → α → PPoint α

この関数型には最初の引数の 名前 が含まれ、その後に続く引数ではこの名前を参照します。関数適用の値が関数本体の引数名を提供された引数の値に置き換えることで導出されるのと同じように、関数適用の型は、引数名を関数の戻り値の型で与えられる値に置き換えることで導かれます。最初の引数に Nat を指定すると、残りの型に含まれるすべての α が Nat に置き換えられます：

#check replaceX Nat

replaceX Nat : PPoint Nat → Nat → PPoint Nat

α 以降の残りの引数には明示的に名前が付けられていないため、引数が増えてもそれ以上の置換は起きません：

#check replaceX Nat natOrigin

replaceX Nat natOrigin : Nat → PPoint Nat

#check replaceX Nat natOrigin 5

replaceX Nat natOrigin 5 : PPoint Nat

関数適用の式全体の型が引数に型を渡すことによって決定されるという事実は、その式を評価する機能には関係がありません。

#eval replaceX Nat natOrigin 5

{ x := 5, y := 0 }

多相関数は名前付きの型引数を取り、その後の引数の型が当該の引数の名前を参照することで機能します。しかし、型引数について名前を付けられたことによる特別なことは何もありません。例えば正負の符号を表すデータ型が与えられたとします：

inductive Sign where
  | pos
  | neg

ここで引数が符号である関数を書くことができます。もし引数が正なら、この関数は Nat を返し、負なら Int を返します：

def posOrNegThree (s : Sign) : match s with | Sign.pos => Nat | Sign.neg => Int :=
  match s with
  | Sign.pos => (3 : Nat)
  | Sign.neg => (-3 : Int)

型は第一級であり、Leanの言語として通常のルールで計算することができるため、データ型に対するパターンマッチで計算することができます。Leanがこの関数をチェックするとき、関数本体の match 式がデータ型の match 式に対応することを利用して、pos の場合は Nat を、neg の場合は Int を期待される型にします。

posOrNegThree を Sign.pos に適用すると、関数本体と戻り値の型の両方の引数名 s が Sign.pos に置き換えられます。評価は式と型の両方で行われます：

(posOrNegThree Sign.pos : match Sign.pos with | Sign.pos => Nat | Sign.neg => Int)
===>
((match Sign.pos with
  | Sign.pos => (3 : Nat)
  | Sign.neg => (-3 : Int)) :
 match Sign.pos with | Sign.pos => Nat | Sign.neg => Int)
===>
((3 : Nat) : Nat)
===>
3

連結リスト

Leanの標準ライブラリには、List と呼ばれる標準的な連結リストのデータ型と、それをより便利に使うための特別な構文が含まれています。リストを記述するには角括弧を使います。例えば10未満の素数が格納されたリストは次のように書くことができます：

def primesUnder10 : List Nat := [2, 3, 5, 7]

この裏側では、List は帰納的データ型として次のような感じで定義されています：

inductive List (α : Type) where
  | nil : List α
  | cons : α → List α → List α

標準ライブラリでの実際の定義は、まだ発表されていない機能を使用しているため若干異なりますが、実質的には似たものになっています。この定義によると、List は PPoint と同様に引数として型を1つ取ります。この型はリストに格納される要素の型です。コンストラクタによれば、List α は nil または cons のどちらかで構築することができます。コンストラクタ nil は空のリストを、コンストラクタ cons は空でないリストを表します。cons の第1引数はリストの先頭で、第2引数はその後ろに連なるリストです。 \( n \) 個の要素を含むリストには \( n \) 個の cons コンストラクタが含まれ、最後の cons コンストラクタの後ろには nil が続きます。

primesUnder10 の例は、List のコンストラクタを直接使うことでより明示的に書くことができます。

def explicitPrimesUnder10 : List Nat :=
  List.cons 2 (List.cons 3 (List.cons 5 (List.cons 7 List.nil)))

これら2つの定義は完全に等価ですが、explicitPrimesUnder10 よりも primesUnder10 の方がはるかに読みやすいでしょう。

List を受け付けるような関数は Nat を取る関数と同じように定義することができます。実際、連結リストは、各 succ コンストラクタに余分なデータフィールドがぶら下がったような Nat と考えることもできます。この観点からすると、リストの長さを計算することは、各 cons を succ に置き換え、最後の nil を zero に置き換える処理です。replaceX が点のフィールドの型を引数に取ったように、length はリストの要素の型を引数に取ります。例えば、リストに文字列が含まれている場合、最初の引数は String ：length String ["Sourdough", "bread"] です。これは次のように計算されます：

length String ["Sourdough", "bread"]
===>
length String (List.cons "Sourdough" (List.cons "bread" List.nil))
===>
Nat.succ (length String (List.cons "bread" List.nil))
===>
Nat.succ (Nat.succ (length String List.nil))
===>
Nat.succ (Nat.succ Nat.zero)
===>
2

length の定義は多相的であり（リストの要素の型を引数にとるため）、また再帰的です（自分自身を参照するため）。一般的に、関数はデータの形に従います：再帰的なデータ型は再帰的な関数を導き、多相的なデータ型は多相的な関数を導きます。

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length α ys)

xs や ys といった名前は、未知の値のリストを表すために慣例的に使用されます。名前の中の s は複数形であることを示すため、「x s(エックスス)」や「y s(ワイス)」ではなく、「エクセズ(exes)」や「ワイズ(whys)」と発音されます。

リスト上の関数を読みやすくするために、[] という括弧記法を使って nil に対してパターンマッチを行うことができ、cons の代わりに :: という中置記法を使うことができます。

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length α ys)

暗黙の引数

replaceX と length はどちらも使うにはややお役所的です、というのも型引数は一般的にその後の引数の値で一意に決まるからです。実際、たいていの言語では、コンパイラが型引数を自分で決定する完璧な能力を備えており、ユーザの助けが必要になることはまれです。これはLeanでも同様です。関数を定義するときに、丸括弧の代わりに波括弧で囲むことで引数を 暗黙的に （implicit）宣言することができます。例えば、暗黙の型引数を持つバージョンの replaceX は次のようになります：

def replaceX {α : Type} (point : PPoint α) (newX : α) : PPoint α :=
  { point with x := newX }

この関数は natOrigin に用いる際に Nat を明示的に渡すことなく使えます、なぜならLeanは後の引数から α の値を 推測 することができるからです：

#eval replaceX natOrigin 5

{ x := 5, y := 0 }

同様に、length も暗黙的に要素の型を取るように再定義できます：

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

この length 関数は primesUnder10 に直接適用できます：

#eval length primesUnder10

4

標準ライブラリにて、この関数は List.length と呼ばれています。つまり、構造体フィールドへのアクセスに使われるドット構文がリストの長さを求めるのにも使えるということです：

#eval primesUnder10.length

4

C#やJavaなどにおいて時折、型引数を明示的に提供することを要求するように、Leanが暗黙の引数がなんであるか常にわかるとは限りません。このような場合、引数をその名前を使って指定することができます。例えば、List.length を整数のリストに対してのみ動作するようにするには、α に Int を設定します：

#check List.length (α := Int)

List.length : List Int → Nat

その他の組み込みのデータ型

リストに加えて、Leanの標準ライブラリには、様々なコンテキストで使用できる構造や帰納的データ型が数多く含まれています。

Option

すべてのリストに先頭の要素があるとは限りません。空のリストも存在します。データのコレクションに対する操作においては探しているものが見つけられないことが多々あります。例えば、リストの先頭の要素を見つける関数は、該当する要素を見つけられないかもしれません。そのため、先頭の要素がないことを知らせる方法が必要です。

多くの言語には、値がないことを表す null という値があります。既存の型に特別な null 値を持たせる代わりに、Leanでは Option と呼ばれる何かしらの型に値がないことを示すものを合わせた型が提供されています。例えば、nullを許容する Int は Option Int で、nullを許容する文字列のリストは Option (List String) 型で表現されます。nullの許容を表すために新しい型を導入するということは、型システムが null のチェックを忘れえないことを意味します。なぜなら Option Int は Int が期待されるコンテキストで使うことができないからです。

Option には some と none という2つのコンストラクタがあり、それぞれベースとなる型の非null版とnull版を表します。非null版のコンストラクタ some にはベースとなる値が格納され、none には引数は渡されません：

inductive Option (α : Type) : Type where
  | none : Option α
  | some (val : α) : Option α

Option 型はC#やKotlinなどの言語のnullable型に非常に似ていますが、同じではありません。これらの言語では、ある型（例えば Boolean ）が常にその型の実際の値（ true と false ）を参照する場合、Boolean? 型または Nullable<Boolean> 型は null 値を元の型に追加する形で許容します。それらの型システムにおいてこの型をなぞるのは非常に有用です: 型チェッカやそのほかのツールはプログラマがnullのチェックを忘れないようにするのに役立ちますし、型シグネチャで明示的にnull許容性を記述しているAPIはそうでないAPIよりも有益です。しかし、これらのnull許容な型はLeanの Option とは非常に重要な点で異なります。Option (Option Int) は none か some none 、some (some 360) で構築できます。一方でC#はnull許容ではない型に対して ? を1つだけつけることを許容しており、複数層のnull許容型を禁じています。またKotlinでは T?? は T? と同じものとして取り扱われます。この微妙な違いは実際にはほとんど関係ありませんが、時折問題になることがあります。

リストの先頭の要素を探すには、もし存在するなら List.head? を使用します。はてなマークは名前の一部であり、C#やKotlinでnull可能な型を示すためにはてなマークを使用することとは無関係です。List.head? の定義では、リストの後続を表すためにアンダースコアが使われています。この場合、アンダースコアはあらゆるものにマッチしますが、マッチしたデータを参照する変数を導入することはできません。名前の代わりにアンダースコアを使うことで、読者に入力の一部が無視されることを明確に伝えることができます。

def List.head? {α : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | y :: _ => some y

Leanの命名規則として失敗する可能性のある操作について、Option を返すものには ? を、無効な入力が渡されたらクラッシュするものには ! を、失敗するときにデフォルト値を返すものには D を接尾辞としてそれぞれ定義します。例えば、head は呼び出し元に対して、渡されたリストが空でないという数学的な根拠の提示を要求します。head? は Option を返し、head! は空のリストを渡されたときにプログラムをクラッシュさせ、headD はリストが空の場合に返すデフォルト値を取ります。はてなマークとビックリマークは名前の一部であり、特別な構文ではありません。このようにLeanの命名規則は多くの言語に比べて自由です。

head? は List 名前空間で定義されているため、アクセサ記法を使うことができます：

#eval primesUnder10.head?

some 2

しかし、これを空リストで試そうとすると、以下の2つのエラーを出します：

#eval [].head?

don't know how to synthesize implicit argument
  @List.nil ?m.20264
context:
⊢ Type ?u.20261

don't know how to synthesize implicit argument
  @_root_.List.head? ?m.20264 []
context:
⊢ Type ?u.20261

これはLeanが式の型を完全に決定できなかったためです。特に、List.head? の暗黙の型引数だけでなく、List.nil の暗黙の型引数も見つけることができていません。Leanの出力での ?m.XYZ は推論できなかったプログラムの一部を表しています。これらの未知の部分は メタ変数 （metavariables）と呼ばれ、エラーメッセージに時折現れます。式を評価するために、Leanはその型を見つけられる必要がありますが、空リストは1つも要素を持たないことから型が見つからないため、上記の式の型を得ることができません。型を明示的に指定することで、Leanは処理を進めることができます：

#eval [].head? (α := Int)

none

この型は型注釈で与えることも可能です：

#eval ([] : List Int).head?

none

エラーメッセージは有用な手がかりを与えてくれます。どちらのメッセージも、足りない暗黙の引数を記述するために、 同じ メタ変数を使用しています。これはLeanが解の実際の値を決定できなかったにもかかわらず、2つの足りない部分が解を共有するだろうと判断したことを意味します。

Prod

Prod 構造体は「Product」の略で、2つの値を結合する一般的な方法です。例えば、Prod Nat String は Nat と String を含みます。つまり、PPoint Nat は Prod Nat Nat に置き換えることができます。Prod はC#のタプル、Kotlinの Pair 型と Triple 型、C++の tuple によく似ています。実用に際しては、Point のような単純な場合であってももっぱら独自の構造体を定義することが最善です。というのもこのような固有の用語によってコードが読みやすくなるからです。さらに、構造体型を定義することで、異なるドメイン概念に異なる型を割り当て、それらが混在することを防ぐことでより多くのエラーを検出できます。

一方、新しい型を定義するオーバーヘッドに見合わないケースもあります。加えて、いくつかのライブラリは「ペア」以上の具体的な概念がないほど十分汎用的です。そして最後に、標準ライブラリには様々な便利関数が含まれており、組み込みのペア型をより簡単に扱うことができます。

標準的なペアの構造体は Prod と呼ばれます。

structure Prod (α : Type) (β : Type) : Type where
  fst : α
  snd : β

リストは頻繁に使われるため、読みやすくなる特別な構文があります。同じ理由で、積の型とコンストラクタも特別な構文を持っています。Prod α β 型は通常 α × β と表記されます。これは集合のデカルト積の通常の表記を反映したものです。同様に、ペアを表す通常の数学的記法が Prod でも利用できます。つまり、以下のように書く代わりに：

def fives : String × Int := { fst := "five", snd := 5 }

次のように書けます:

def fives : String × Int := ("five", 5)

どちらの記法も右結合です。つまり、以下の定義は等価です:

def sevens : String × Int × Nat := ("VII", 7, 4 + 3)

def sevens : String × (Int × Nat) := ("VII", (7, 4 + 3))

言い換えれば、2つ以上の型を持つすべての積とそれに対応するコンストラクタは、実際には裏でネストされた積とネストされたペアなのです。

Sum

Sum データ型は、2つの異なる型の値を選択できるようにする汎用的な方法です。例えば、Sum String Int は String か Int のどちらかです。Prod と同様に、Sum は非常に汎用的なコードを書く時や、ドメイン固有の型が無いような非常に小さなコードで使用するか、標準ライブラリに便利な関数があるときに使用します。たいていの場合、カスタムの帰納型を使用する方が読みやすく、保守性も高くなります。

Sum α β 型の値は、コンストラクタ inl を α 型の値に適用したものか、コンストラクタ inr を β 型の値に適用したかのどちらかです：

inductive Sum (α : Type) (β : Type) : Type where
  | inl : α → Sum α β
  | inr : β → Sum α β

これらの名前はそれぞれ「左埋め込み(left injection)」と「右埋め込み(right injection)」の略です。Prod にデカルト積の記法が使われるように、Sum には「丸で囲んだプラス」記法が使われ、Sum α β は α ⊕ β とも書き表されます。Sum.inl と Sum.inr には特別な構文はありません。

例えば、ペットの名前に犬の名前と猫の名前のどちらもあり得る場合、それらを表す型を文字列の和として導入することができます。

def PetName : Type := String ⊕ String

実際のプログラムでは通常、このような目的のためには情報量の多いコンストラクタ名でカスタムの帰納的データ型を定義する方がよいでしょう。ここでは犬の名前には Sum.inl を、猫の名前には Sum.inr を使用します。これらのコンストラクタを使用して、動物の名前のリストを書くことができます：

def animals : List PetName :=
  [Sum.inl "Spot", Sum.inr "Tiger", Sum.inl "Fifi", Sum.inl "Rex", Sum.inr "Floof"]

2つのコンストラクタを区別するために、パターンマッチを使うことができます。例えば、動物の名前のリストに含まれる犬の数（つまり、Sum.inl コンストラクタの数）を数える関数は次のようになります：

def howManyDogs (pets : List PetName) : Nat :=
  match pets with
  | [] => 0
  | Sum.inl _ :: morePets => howManyDogs morePets + 1
  | Sum.inr _ :: morePets => howManyDogs morePets

関数呼び出しは中置演算子より前に評価されるため、howManyDogs morePets + 1 は (howManyDogs morePets) + 1 と同じです。予想通り、#eval howManyDogs animals は 3 を返します。

Unit

Unit は unit と呼ばれる引数のないコンストラクタを1つだけもつ型です。つまり、引数のないコンストラクタを適用した単一の値のみを記述します。Unit は以下のように定義されます：

inductive Unit : Type where
  | unit : Unit

単体では Unit は特に役に立ちません。しかし、多相なプログラムでは、足りないデータのプレースホルダとして使用することができます。例えば、以下の帰納的データ型は算術式を表します：

inductive ArithExpr (ann : Type) : Type where
  | int : ann → Int → ArithExpr ann
  | plus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | minus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | times : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann

型引数の ann は注釈を表し、各コンストラクタは注釈されています。パースされた結果の式はソース中の位置を注釈しているかもしれないため、ArithExpr SourcePos の戻り値の型はパーサがそれぞれの部分式に SourcePos を置くことを保証します。しかし、パーサから来ない式はソース中の位置を持たないため、その型は ArithExpr Unit となります。

さらに、すべてのLeanでの関数は引数を持つため、ほかの言語での引数が無い関数は、Leanでは Unit 引数を取る関数として表すことができます。戻り値の観点では、Unit 型はC言語から派生した言語での void 型に似ています。C言語ファミリーでは、void を返す関数は呼び出し元に制御を返すが、興味深い値を返すことはありません。Unit は意図的に興味のない値であることで、型システムの中に特別な目的の void 機能を必要とすることなく、これを表現することができます。Unit のコンストラクタは空の括弧で書くことができます：() : Unit

Empty

Empty データ型はコンストラクタを一切持ちません。よってこれは到達不可能なコードを意味します。なぜなら、どんな関数呼び出しの列も Empty 型の値で終了することは無いからです。

Empty は Unit ほど頻繁には使われません。しかし、特殊なコンテキストでは役に立ちます。多くの多相データ型では、すべてのコンストラクタですべての型引数を使用するわけではありません。たとえば、Sum.inl と Sum.inr はそれぞれ Sum の型引数を1つしか使用しません。Empty を Sum の型引数の1つとして使用することで、プログラムの特定の時点でコンストラクタの1つを除外することができます。これにより、追加の制限があるコンテキストでジェネリックなコードを使用することができます。

名前について: 和(Sum)、積(Product)、単位(Unit)

一般的に、複数のコンストラクタを持つ型は 直和型 （sum type）と呼ばれ、単一のコンストラクタが複数の引数を取る型は 直積型 （product type）と呼ばれます。これらの用語は、通常の算術で使われる和と積に関連しています。この関係は、関係する型が有限個の値を含む場合に最もわかりやすいでしょう。α と β がそれぞれ \( n \) 個と \( k \) 個の異なる値を含む型だとすると、α ⊕ β は \( n + k \) 個の異なる値を含み、α × β は \( n \times k \) 個の異なる値を含みます。たとえば Bool は true と false の2つの値を持ち、Unit には Unit.unit という1つの値があります。積 Bool × Unit は2つの値 (true, Unit.unit) と (false, Unit.unit) を持ち、和 Bool ⊕ Unit は3つの値 Sum.inl true と Sum.inl false 、Sum.inr unit を持ちます。これと同様に、 \( 2 \times 1 = 2 \) と \( 2 + 1 = 3 \) となります。

見るかもしれないメッセージ

すべての定義可能な構造体や帰納型が Type 型を持つわけではありません。特に、コンストラクタが引数として任意の型を取る場合、帰納型は異なる型を持たなければなりません。これらのエラーは通常、「宇宙レベル」について述べています。例えば、この帰納型について：

inductive MyType : Type where
  | ctor : (α : Type) → α → MyType

Leanは以下のエラーを出します：

invalid universe level in constructor 'MyType.ctor', parameter 'α' has type
  Type
at universe level
  2
it must be smaller than or equal to the inductive datatype universe level
  1

後の章では、なぜそうなるか、どのように定義を修正すればうまくいくのかを説明します。今の時点では、型をコンストラクタの引数ではなく、帰納型全体の引数にしてみてください。

同様に、コンストラクタの引数が定義されているデータ型を引数とする関数である場合、その定義は却下されます。例えば以下の定義について：

inductive MyType : Type where
  | ctor : (MyType → Int) → MyType

このようなメッセージが出力されます：

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared

技術的な理由から、このようなデータ型を許可すると、Leanの内部論理が損なわれる可能性があり、定理証明として使用するのに適さなくなります。

帰納的な型の引数を忘れると、混乱を招くメッセージになることもあります。例えば、ctor の型の MyType に引数 α が渡されていない場合です：

inductive MyType (α : Type) : Type where
  | ctor : α → MyType

Leanはこれに対して以下のエラーを返します:

type expected, got
  (MyType : Type → Type)

このエラーメッセージは MyType の型は Type → Type であり、型そのものを記述していないと言っています。MyType が実際の正真正銘の型になるためには、引数を必要とします。

定義の型シグネチャなど、ほかのコンテキストで型引数が省略された場合にも、同じメッセージが表示されることがあります：

inductive MyType (α : Type) : Type where
  | ctor : α → MyType α

def ofFive : MyType := ctor 5

演習問題

• リストの最後の要素を探す関数を書いてください。これは Option を返すべきです。

• リストの中で与えられた述語を満たす最初の要素を探す関数を書いてください。定義は def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α := から始めてください。

• ペアの2つのフィールドを入れ替える関数 Prod.swap を書いてください。定義は def Prod.swap {α β : Type} (pair : α × β) : β × α := から始めてください。

• カスタムのデータ型を使って PetName の例を書き換えて、Sum のバージョンを比較してください。

• 2つのリストのペアを紐づける関数 zip を書いてください。出力されるリストは入力のリストのうち短い方と同じ長さにしてください。定義は def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) := から始めてください。

• リストの先頭から \( n \) 個の要素を返す多相関数 take を書いてください。ここで \( n \) は Nat です。もしリストの要素が n 個未満の場合、出力のリストは入力のリストにしてください。また #eval take 3 ["bolete", "oyster"] は ["bolete", "oyster"] を出力し、#eval take 1 ["bolete", "oyster"] は ["bolete"] を出力させてください。

• 型と算術の間の類似を使って、直積を直和に分配する関数を書いてください。言い換えると、この型は α × (β ⊕ γ) → (α × β) ⊕ (α × γ) になります。

• 型と算術の間の類似を使って、2倍が和になる関数を書いてください。言い換えると、この方は Bool × α → α ⊕ α になります。