Haskell の `Int` は『空間』でもある — プログラミング言語のデータ型が持つもうひとつの顔

前回、「空間を連続変形しても、変わらずに残る本質的な構造（不変量）を取り出す数学—「数学のホモトピー理論」は「定理証明言語の型理論」につながる」という記事を公開しました。

そこでは、数学のホモトピー理論の世界観 ── 対象を空間の中の点として置き、2つの対象が等しいことを、2点をつなぐ道として描く見方 ── を紹介しました。

池のある広場では、2点をつなぐ道が何種類にも枝分かれすること、そして、空間を連続変形して残る骨組みが、その道の一覧表から読み取れることを見ました。

今回の記事は、その 空間的な眼差し を、プログラミング言語のデータ型 に当てはめます。

前回が 数学の側の景色 だったのに対して、今回は、皆様がふだん書き慣れている Haskell のコードを入り口にして、同じ景色を眺め直します。

想定読者と、この記事のねらい

• Haskell を触り始めて3ヶ月ほどの機械学習エンジニア
   
• 高校の理系数学は履修したが、細かい内容はほぼ忘れている
   
• 型理論は未学習。「依存型」については「要素の数を指定した List 型を定義できる、興味深い言語機能」という程度の認識
   
• 「圏論」「ホモトピー理論」「Martin-Löf 型理論」は、名前だけ耳にしたことがある、または全く知らない

この記事は、そういう皆様に 「Haskell の Int 型は、実は幾何学の対象でもある」 という視点を持ってもらうことをねらいとしています。

いつも書いている Int、String、[a] といった データ型 が、数学者の言う「空間」でもある 、と言われても最初はピンとこないと思います。

しかし、この記事を読み終えたとき、皆様はたぶん次のように思われるはずです。

Haskell で data Foo = Bar | Baz と書くとき、私は幾何学の対象を書いていたのか。

専門用語は最小限に抑え、必要なものだけ順序立てて導入します。

数学の教科書のような厳密な定義（開集合を使った位相空間の定義など）は使いません。

かわりに、「点と道」というごく素朴な言葉 だけで説明します。

---

1. Haskell で [Int] を書くとき、皆様は幾何学の対象を書いていた

いきなり結論めいたことを書きます。

Haskell で次のようなコードを書いたことがあると思います。

xs :: [Int]
xs = [1, 2, 3]

これはリスト型 [Int] の値 [1, 2, 3] を定義しているだけの、ごく普通の Haskell コードです。

このとき、皆様はたぶん [Int] を 「Int の並び」 という程度に思っています。
それで日常のプログラミングには何の問題もありません。

ところが、現代の型理論の一分野である ホモトピー型理論（Homotopy Type Theory、以下 HoTT ¹）の視点から見ると、[Int] は 一種の「空間」 として読むことができます。

しかも、その空間の中には 「点」だけでなく「道」がある という、数学者にとって自然な構造 を持っています。

この記事では、この主張の意味を、Haskell を書いてこられた皆様の視点から丁寧に解きほぐしていきます。

---

2. 「空間」って、開集合とかの話ですか？

大学の教養課程で位相空間論を学ばれたことがある方であれば、「空間」と聞くと 開集合の族が定義された集合 を思い浮かべるかもしれません。

そういう厳密な話は、この記事ではしません。

ここで採用するのは、次のような素朴な見方です。

空間とは、点と、点どうしを結ぶ道が集まったもの。

これだけです。以下、この一行を頼りに話を進めます。

• 点: 空間の中に住む要素
• 道: ある点から別の点まで、空間の中を切れ目なく移動する経路

数学者は「道」のことを path（パス）と呼びます。

以降、日本語で「道」と書きますが、頭の中で「path」と読み替えてもらってかまいません。

そして、この視点にひとつだけ、大事な追加ルールがあります。

「動かない道」も 1 つの道として数える。

つまり、点 x から x 自身への「その場に留まる」経路も、正当な 1 本の道です。これを refl（reflexivity、反射律）と呼びます²。

---

3. Int を空間として見る

上の見方を、Haskell の Int に当てはめてみます。

Int には、整数を表す値が入ります。

ここでは簡単のため、..., -2, -1, 0, 1, 2, ... と並べて考えてみましょう。

これらを 空間の点 として見ます。

では、点と点を結ぶ 道 はどうなっているのでしょうか？

ルールはこうです。

• 同じ値の間: 「動かない道」が 1 本だけある
• 異なる値の間: 道はない（0 本）

たとえば、3 から 3 への道は、「動かない道」1 本だけ。
3 から 4 への道は、存在しない。

図示すると以下のようになります。

各整数の上にある小さな緑色のアーチが「動かない道」を表しています。
異なる整数の間には、何も描かれていません（道がないから）。

Haskell で 3 == 3 と書けば True が返ります。
この True は、「3 と 3 を結ぶ道が 1 本ある」ということの Haskell における表明です。

一方、3 == 4 は False を返します。
これは「3 と 4 を結ぶ道は存在しない」ということです。

この見方の下では、Haskell の == は 「2 つの値を結ぶ道が存在するかどうか」を判定するもの と読み直せます。

📌 中上級者向け補足：厳密性を担保した説明をすると ── `==` と恒等型は同じものなのか

ここで本文では、Haskell の == と、HoTT における「道」を対応づけて説明しました。ただし、== と HoTT の恒等型（identity type）は、まったく同じ仕組みではありません。

Haskell の == は Eq 型クラスによる比較演算です。一方、HoTT では x ≡ y のような恒等型そのものが「x と y の等しさの証拠」を表します。

したがって、本文の説明は、Haskell の等値比較を HoTT 的な空間の見方に対応づけて理解するための比喩です。

そして、これが Int を空間として見る第一歩です。Int は、点が縦横無尽に並んでいるけれど、それらの間には道がほとんどない、退屈な空間 なのです。

---

4. String, List, Tuple も同じ「退屈な空間」

Int と同じ見方が、String、[Int]、(Int, Bool) などにもそのまま当てはまります。

String は [Char] と同じで、文字の並びです。"hello" と "hello" の間には道が 1 本（動かない道）、"hello" と "world" の間には道はありません。

[Int] も同様です。[1, 2, 3] と [1, 2, 3] の間には道が 1 本、[1, 2, 3] と [1, 2, 4] の間には道はありません。

やや意外に思えるかもしれませんが、リスト同士の「等しさの根拠」も 1 本だけです。

なぜでしょうか？

リスト [1, 2, 3] と [1, 2, 3] を比べるとき、各位置ごとに 1 == 1, 2 == 2, 3 == 3 を確かめます。

各位置での道は 1 本ずつ。それを 3 つ束ねると、全体としても 1 本の道になります。

(Int, Bool) のようなタプル型も同じです。

(3, True) と (3, True) の間には、成分ごとの道 1 本ずつを束ねた道が全体として 1本あります。

こういう 「同じ値の間には道が1本、異なる値の間には道がない」型 を、HoTT では h-set（h-集合、または h-level 2 の型）と呼びます³。

Haskell で日常的に扱う多くのデータ型は、この h-set の世界をイメージするのに向いています。

📌 中上級者向け補足：厳密性を担保した説明をすると ── h-set と Haskell の型は本当に同じなのか

HoTT でいう h-set は、ざっくり言えば「任意の2点の間の恒等型が命題となる型」です。
直感的には、各 x, y について x = y の証拠が高々1つ、というイメージです。

一方、Haskell の実行時の値には、非停止計算や未定義値など、純粋な型理論にはそのまま存在しない意味論上の事情があります。

そのため、この記事では「Haskell の通常のデータ型を h-set 的な空間として眺めるモデル」を採用しています。

---

5. 関数型 — 「等しさの根拠」は何本あるか

ここで、関数型 A -> B を考えます。

関数型を 空間として見る と、少し面白いことが起こります。

for ループ版と再帰版の階乗を、Haskell で並べてみます。

factLoop :: Int -> Int
factLoop n = foldl (*) 1 [1..n]

factRec :: Int -> Int
factRec 0 = 1
factRec n = n * factRec (n - 1)

それでは、次の問いの答えを問われたとき、皆様はどのように回答されますか？

factLoop == factRec と書けますか？

書けません。Haskell は関数の等しさを == で判定しません。

しかし、どんな n を入れても両者は同じ値を返します。

ここで数学の側の答えを紹介します。

数学（および Agda や Rocq のような証明支援系）の側では、「どんな入力に対しても同じ結果を返すなら、2 つの関数は等しい」というルールを認めることができます。関数外延性（function extensionality）と呼びます⁴。

📌 中上級者向け補足：厳密性を担保した説明をすると ── 関数外延性とは何を言っているのか

関数外延性（function extensionality）は、関数 f と g について、

(∀ x, f x = g x) → f = g

という形の原理です。

つまり、「すべての入力 x について値が等しい」ことから、「関数そのものが等しい」ことを導きます。

ただし、これは Haskell の == が関数に使える、という意味ではありません。
Haskell では通常、関数に Eq インスタンスはありません。

また、本文の factLoop / factRec は数学的な関数の等しさを直感的に説明するための例です。
実際の Haskell では停止性などの事情があります。

Cubical Agda では、関数外延性を公理として追加するのではなく、型理論の構成の中で 扱える形になっています。

ここが本記事のちょっとした山場です。

factLoop と factRec の間に道は何本あるか

第 4 節までで見てきたように、「2つの値の間の道」とは「等しいことの根拠」のことでした。
では、factLoop と factRec の場合、その根拠はいくつあるでしょうか。

関数外延性について、もう少し掘り下げて見ていきましょう。

関数外延性は、次のような形をしています。

各入力 n について、factLoop n と factRec n の間の道 を集めれば、
それを束ねて factLoop と factRec の間の道 を 1 本作れる。

入力ごとの道を「集めて束ねたもの」が、関数どうしの道になる のです。

では、各入力 n について、factLoop n と factRec n の間には道は何本あるでしょうか。

• factLoop 0 も factRec 0 も 1 を返します。両者は Int の値として同じ 1。第 3 節で見たとおり、Int の同じ値の間には 道は 1 本だけ（動かない道）。
• factLoop 1 も factRec 1 も 1。やはり道は 1 本。
• factLoop 2 も factRec 2 も 2。道は 1 本。
• 以下同様、どの n についても道はちょうど 1 本ずつ。

各入力について 1本ずつの道を、すべての入力にわたって束ねたもの。
これが、関数外延性が与える「factLoop と factRec の道」の正体です。

結論として、factLoop と factRec の間の道は、実質的に1本 です。

これは、第 4 節で見た [1,2,3] と [1,2,3] の道が 1 本だったのと同じ理由です。

各位置での道が1本ずつ、それを束ねると全体として1本になる。
関数の場合も、各入力での道が1本ずつ、それを束ねて全体として1本になる。

なぜ「引数の型は道の本数に影響しない」のか

ここで、次の主張が具体的な意味を帯びてきます。

関数型 A -> B を空間として見ると、その豊かさは実は 戻り値の型 B の豊かさ だけで決まります。引数の型 A は、道の本数には影響しません。

factLoop と factRec の例で確かめると、以下のようになります。

• 引数の型は Int。入力の値としては 0, 1, 2, ... と無限にあります。
• しかし、各入力について集める道は、戻り値の型 Int の中の道 です。
• Int は退屈な空間で、同じ値の間の道は 1 本しかありません。
• したがって、各入力について 1 本、束ねても全体として 1 本、という結論になります。

もし戻り値の型が Int ではなく、もっと道の豊かな型（第 6 節で出てくる円周 S¹ のような）だったら、話は変わります。

各入力について複数本の道があり、それを束ねると関数どうしの間にも複数の道が生じます。

引数の型 A は、「何個の入力について道を集めるか」を決めるだけで、「各入力について何本道があるか」には関わらない。

だから、関数型 A -> B の道の豊かさは、戻り値の型 B だけで決まる、というわけです。

Int -> Int はやはり h-set です。
Nat -> Bool も h-set。

実用上使う関数型はほとんど h-set の仲間、ということになります。

📌 中上級者向け補足：厳密性を担保した説明をすると ── 関数型 `A -> B` の「豊かさ」は B だけで決まるのか

HoTT では、関数 f, g : A → B の恒等型について、関数外延性により、各 x : A における f x と g x の恒等型の族との対応が得られます。直感的には、

(f = g) ≃ ∀ x : A, f x = g x

という関係です。

そのため、各入力について現れる「値の等しさ」を束ねて関数の等しさを考える、という本文の説明ができます。

ただし、これは「A が完全に無関係」という意味ではありません。
A は、どの入力について等しさを集めるかを決めます。

---

6. 退屈じゃない空間 — 円周をデータ型で書く

ここまでの型は、すべて h-set（退屈な空間）でした。

世の中には、もう少し豊かな空間もあります。

Haskell では書けませんが、後で紹介する Cubical Agda という言語では書ける、そんなデータ型の例を紹介します。

まず、円周を数学の側で復習する

「円周」と聞いて、皆様は「半径1の丸」を思い浮かべられると思います。

ここでいう円周も、まさにその丸のことです。
数学者はこれを S¹（エスワン、1次元球面）と書きます。

円周というのは、丸の輪郭そのもの です。
中身の円盤は含みません。線だけです。

そして、S¹ の輪郭上に 1 点を選び、その点に名前をつけて base と呼ぶ ことにします。
日本語で「基点」と訳します。

「どこでもいいから 1 点、目印になる場所」と思ってください。
地図で言えば、旅の出発地点を「ここ」と決めるようなものです。

図の中で、輪郭上の黒丸が base です。
ここでは輪郭の一番上に選びましたが、右でも下でも、選ぶ場所はどこでも構いません。

base を 1 つ決めたら、次のような問いが立ちます。

base から出発して、円周に沿って歩き、base に戻ってくる道は何通りあるか？

• 動かないでその場にいる ── これも 1 つの道（動かない道）
• 1 周して戻る ── これは動かない道とは違う道
• 2 周して戻る ── これもまた違う道
• 逆向きに 1 周 ── これもまた違う道

こうして、base から base への道は、「何周したか」で無限に区別できます。

左回りをプラス、右回りをマイナスと数えると、道の種類は 整数全体 ℤ と 1 対 1 に対応 します。

これが、代数トポロジーで 19 世紀末から知られている 「円周の基本群は ℤ である」 という古典的な事実です⁵。

📌 中上級者向け補足：厳密性を担保した説明をすると ── 円周の道は本当に整数本なのか

「円周の基本群が ℤ である」というとき、整数と対応しているのは、円周上のループそのものを1本ずつ数えた集合ではありません。

円周上には、同じ「1周」を少しずつ違う形で描いた連続経路が無数にあります。
これらを、端点を固定した連続変形（ホモトピー）で同じものとしてまとめます 。

その結果得られる ループのホモトピー類 が、整数 ℤ で分類されます。

この「base から出発して、円周に沿って左回りに1周し、base に戻ってくる道」を、loop と呼ぶことにします。

この円周を、データ型として書く

さて、上で説明した円周を、そのままデータ型として書くとどうなるでしょうか？

円周というデータ型は、「base という点」と「base から base への 1 周の道 loop」の 2 つから組み立てられます。

Cubical Agda では次のように書けます。

data S¹ : Type where
  base : S¹
  loop : base ≡ base

1 行目、2 行目、3 行目の読み方は、以下の通りです。

• 1 行目 data S¹ : Type where は、Haskell でいう data S1 = ... にあたります。「S¹ という新しいデータ型を定義するよ」という宣言です。
   
• 2 行目 base : S¹ は、Haskell でいう Base :: S1 にあたります。「S¹ の値として base というものがある」というコンストラクタです。ここまでは Haskell と同じ発想です。
   
• 3 行目 loop : base ≡ base が、Haskell では絶対に書けないものです。base から base への道 loop を、コンストラクタとして直接定義している のです。
  Haskell では「データ型の値」を作るコンストラクタしか書けませんが、Cubical Agda では、「値と値の間の道」を作るコンストラクタも 書けます。

つまり S¹ は「値 base がひとつあるだけの型」ではありません。

値 base と、base から base への道 loop の両方を含むデータ型 なのです。

そして、loop を 2 回続ければ 2 周、逆向きに 1 回で −1 周、と重ねていけるので、base ≡ base の中には、動かない道と loop と loop・loop と … と、整数の本数だけ道があります。

第4節までに見てきた Int や [Int] は、「値（点）しかコンストラクタで作れない、退屈な空間」 でした。

S¹ は、「値（点）と 道の両方を コンストラクタで作る、退屈じゃない空間」の最初の例です。

こういう「経路もコンストラクタで定義できるデータ型」を 高次帰納型（ Higher Inductive Type 、以下 HIT ）と呼びます。

ここが、関数型プログラミングとホモトピー理論が実際に出会う場所 です。

📌 中上級者向け補足：厳密性を担保した説明をすると ── HIT の `loop : base ≡ base` は何を意味するのか

loop : base ≡ base は、単なる Haskell の関数や普通のデータ値ではなく、恒等型 base ≡ base の要素です。

HIT は、点だけでなく、点の間の等しさの証拠を生成規則として持つ型 を記述できます。

さらに 恒等型そのものが型 なので、その中にも高次の等しさを考えられます 。

本文では、この構造を、「値と道を同じデータ型の中で生成できる」 と直感化しています。

もうひとつの例 ── 風船の表面 S² も書ける

前回の記事の第4節で、「1階は空き部屋なのに、2階に住人がいる建物」のような空間として、風船の表面を紹介しました。

数学者はこれを S²（エスツー、2 次元球面）と書きます。
この S² も、*Cubical Agda では データ型として コードに記述することができます。

data S² : Type where
  base : S²
  surf : refl ≡ refl

• 2 行目までは S¹ と同じで、点 base をひとつ作ります。
• 3 行目の refl は、base から base への「動かない道」のことです。つまり surf : refl ≡ refl は、「動かない道」から「動かない道」への変形を、コンストラクタとして直接作っています。S¹ の loop が「道のコンストラクタ」だったのに対して、surf は 「道と道をつなぐ変形（2 段目）のコンストラクタ」 です。風船の表面という 2 次元の面を、この 1 個の変形として貼りつけている、と読めます。

コンストラクタの置き場所が1段違うだけですが、この違いが、空間の性格の違いにそのまま現れます。

• S¹ は、1 段目（道の段）で豊かになります。base ≡ base には整数の本数だけ道がある一方、その上の段（道と道の等しさ、さらにその上……）は、すべて実質1通りに潰れます。
  それゆえ、S¹ の階段は、下から 3段目にあたる高さ（h-level 3）で止まります。
• S² は、1 段目は静かです。どのループも 1 点に縮められて、道は実質 1 本しかありません。ところが 2 段目 で、しぼんだ風船をボールに何回かぶせ直すか、という整数の違いが現れます（数学の記号では π₂(S²) ≅ ℤ）。しかも話はそこで終わらず、3 段目より上にも非自明な構造が現れ続けることが知られています。S² の階段は、どの有限の高さでも止まりません。

「どの段で豊かさが現れるか」「階段が有限で止まるか」は、型ごとの個性 です。

次の第7節の表では、S¹ と S² の2つの型を並べて整理します。

---

6.5 豊かな空間は、円周だけではない — 毛色の違う 3 つの例

第6節では、道をコンストラクタで作る円周 S¹ を見ました。

「豊かな空間の例は、幾何学の図形だけなのか？」と思われたかもしれません。

実は、まったく違う出どころからも、道が複数ある型は現れます。

ここでは、円周とは毛色の違う例を3つ、紹介だけしておきます。

いずれも、HoTT の標準的な教科書や査読つき論文で扱われている、確立した例です。

例 A：型そのものを並べた空間の中の Bool

ここまでは、Int や S¹ という「ひとつの型の内側」を空間として見てきました。

今度は視点を一段階 引き上げて、型そのものを点として並べた空間 を考えることもできます。

Int も Bool も S¹ も、それぞれがこの大きな空間の中の1個の点になります（この特別な空間を、型理論では 宇宙 と呼びます）。

この空間の中で、点 Bool から点 Bool 自身への道は、何本あるでしょうか？

答えは 2 本 です。

Bool の値を Bool の値へ、情報を失わずに対応させる方法が2通りあるから です。

ひとつは「True は True へ、False は False へ」というそのままの対応。

もうひとつは「True と False を入れ替える」対応（Haskell の not にあたります）。

HoTT には、この2通りの対応を、そのまま2本の別々の道として空間に登録する仕組みが備わっています（Univalence と呼ばれる原理で、後続の記事で正面から向き合います）。

3 と 3 の間の道は 1 本きりでした。

ところが Bool と Bool の間の道は 2 本ある。

同じ「自分自身と等しい」でも、階が違えば本数が違う
── これが、型そのものを点として眺めたときに見える景色です。

📌 中上級者向け補足：厳密性を担保した説明をすると ── `Bool` と `Bool` の間の「2 本の道」の正体

本文では、Bool から Bool への道が「恒等対応」と「True / False の交換」の2通りある、と説明しました。これは Univalence の考え方を直感化したものです。

HoTT では、Univalence により、型の同値（equivalence）から型の等しさを構成できます。

Bool の場合は、Bool から Bool への同値がちょうど2つあり、それに対応して等しさの証拠もちょうど2つになる、というところまで正確に言えます。

ただし、一般の型では、等しさの型はこのような単純な数えあげでは済まず、それ自体が高次の構造を持ちえます。

「道が2本」という数え方がそのまま通用するのは、Bool のような素朴な型（h-set）どうしの場合です。

例 B：重複のない有限集合 ── 並べ替えの数だけ道がある

次は、組合せの世界からの例です。

トランプのカードを 3 枚、{A, B, C} という重複のない集まりとして持っているとします。

この集まりを、例 A と同じように「集まりそのものを点として並べた空間」の中の 1 点として見ると、点 {A, B, C} から自分自身への道は何本あるでしょうか。

こちらの答えは 6 本 です。

3枚のカードを 3枚のカードへ、過不足なく対応させる方法（つまり並べ替え）が、3 × 2 × 1 = 6 通りあるからです。

カードが 4 枚なら 24 本、
5枚なら 120 本。

要素の個数の階乗のぶんだけ、「自分自身と等しい」ことの道が並びます。

シャッフルの1回1回が、それぞれ別の「等しさの証拠」として空間に記録されている
── そんなイメージです。

円周の道が「何周したか」という幾何学の量で数えられたのに対して、こちらの道は「どう並べ替えたか」という組合せの量で数えられます。

出自はまるで違う のに、「道が複数ある空間」という 同じ現象が起きている のです。

例 C：バージョン管理 ── リポジトリを点、パッチを道として見る

最後は、皆様の日常業務にいちばん近い例です。

Git のようなバージョン管理システムを思い浮かべてください。

リポジトリの各状態を空間の点、コミット（パッチ）を、状態から状態への道 として見る、という研究があります。

Angiuli、Morehouse、Licata、Harper による "Homotopical Patch Theory"（ICFP 2014）という査読つき論文で、バージョン管理の理論が、実際に HoTT の型として書き下されました。

この見方の面白さは、2段目にあります。

たとえば、別々のファイルに触る2つのパッチは、どちらを先に適用しても同じ結果になります。

「p を当ててから q を当てる」道と、「q を当ててから p を当てる」道
── この2本の道が同じ結果に至ることの証拠は、まさに前回の記事で見た 道と道をつなぐ変形（2 段目の等しさ）として表現されるのです。

merge や 履歴の入れ替えといった、バージョン管理の日常的な操作の背後に、等しさの階層構造が横たわっていた ことになります。

📌 中上級者向け補足：厳密性を担保した説明をすると ── Git のパッチと HoTT の「道」は数学的に同じなのか

Homotopical Patch Theory は、バージョン管理におけるパッチを数学的な構造として扱い、パッチの合成や交換に現れる等しさを高次の構造として捉える研究です。

ただし、実際の Git のコミットやパッチが、そのまま HoTT の恒等型になるという意味ではありません。

研究上のモデルとして、バージョン管理の操作を HoTT 的な構造に対応づけています。

3つの例に共通するのは、道が複数ある空間は、幾何学の教室の外にもふつうに転がっている ということです。

型の宇宙、カードの束、Git のリポジトリ。

皆様の身の回りは、思ったより退屈ではないのかもしれません。

---

7. まとめの表 — h-level で並べる

ここまで見てきたデータ型を、「同じ2点の間に 道が何本あるか 」を基準にして並べてます。
この本数の指標を、HoTT では h-level（h-層、または h-レベル）と呼びます。

📌 中上級者向け補足：厳密性を担保した説明をすると ── h-level の数字には注意が必要

HoTT の h-level は、単純に「道の本数を数える番号」ではありません。

h-level は、恒等型がどこまで単純になるかを帰納的に測る概念です。
たとえば h-set は、任意の2点の間の恒等型が命題となる型と捉えられます。

そのため、「h-level 2 ＝ 道が1本」「h-level 3 ＝ 同型が何本」といった単純な対応表は、誤解を生みやすいところです。

下の表は、この記事の範囲で直感をつかむための整理であり、正確な定義は h-level の帰納的な定義に譲ります。

データ型・比較対象	道の本数	名前（HoTT の言葉で）
Unit（値 1 つ）	点も道もほぼない	h-level 0（可縮）
Bool, Int, String, [Int] の同じ値どうし	道は 1 本のみ	h-level 2（h-set）
factLoop と factRec（Int -> Int の要素どうし）	各入力で 1 本ずつ、束ねて 1 本	h-level 2（h-set）
群、ベクトル空間などの数学的構造	道は同型の本数だけ（有限または無限）	h-level 3
円周 S¹ の base から base へ	道は整数の本数だけ	h-level 3（道の段で豊かさが現れる）
風船の表面 S²（前回の記事に登場）	1 段目は実質 1 本、2 段目で整数の本数だけ	有限の h-level を持たない

📌 中上級者向け補足：厳密性を担保した説明をすると ── 群・ベクトル空間の「道＝同型」はどういう意味か

型として扱った数学的構造では、構造を保つ同型や自己同型が、Univalence を通して等しさの構造として現れます。

ただし、「道の本数＝自己同型の個数」と単純に言うだけでは、高次の構造を省略しています。無限個の自己同型を持つ構造もあります。

本文では、自己同型が等しさの構造として現れる、という入口だけを示しています。

Haskell で普段扱う型は、この表のうち上から3段目までにほぼ収まります。
要するに h-set の世界です。

そして、円周 S¹ や球面 S² のような、点だけでなく、道や変形までコンストラクタで作る型 を書けるのは、Haskell ではなく、Cubical Agda のような HIT を持つ言語 の役割です。

---

8. なぜこの視点が嬉しいのか

「Haskell の Int を空間として見て、何が嬉しいのか？」という問いに答えて、この記事を締めます。

第 1 に、== の意味が広がる。Haskell の == は True か False を返すだけですが、HoTTの視点 では、「等しさ」には 何本の根拠があるか という豊かさがあります。

日常のプログラミングでは、0本か1本かしか意識しませんが、円周のような型では2本、3本、無限本の根拠が区別されます。

この視点は、証明支援系（Agda、Rocq、Lean）で数学の定理を形式化するときに、大きな威力を発揮します 。

第 2 に、data 宣言と幾何学がつながります。

Haskell で data Foo = Bar | Baz と書くとき、皆様は「Bar と Baz という 2 つの点を持つ、退屈な空間」を定義していたことになります。

この視点を持つと、Cubical Agda の HIT のような 「経路も定義できるデータ型」 が、Haskell の data の自然な拡張として理解できます。

第3に、型理論の家系図の中で、Haskell の立ち位置を認識できます。

Haskell は、単純型付きラムダ計算に多相型を加えた辺りの型理論 を実装しています。
依存型 は持ちませんし、恒等型（identity type、「等しさそのものを型として扱う」型）も持ちません。（このあたりの議論は、次回公開予定の記事で、主題として取り上げる予定です）

HoTT や Cubical Agda は、その先の景色 を示してくれます。

「Haskell の通常のデータ型は、この記事でいう h-set の世界を中心に捉えられる」と、自分の使っている言語の特徴と守備範囲を認識できることは、他の言語や理論への橋を架ける第一歩です。

---

9. 次に読むもの

この記事は、数珠つなぎの単独記事の2本目にあたります。
以下は後続の記事で扱う予定のテーマです。

• 型理論の家系図 — 単純型付きラムダ計算から始めて、多相型（System F）、依存型（Martin-Löf 型理論）、CoC/CIC、そして HoTT まで、家系図を段階的にたどる
   
• 立方体型理論（Cubical Type Theory） — HoTT の中の等しさ（恒等型）を「実際に計算できる形」で扱うための型理論。De Morgan立方体 、Cartesian立方体 という 2つの流派 がある

また、Rocq、Agda、Idris 2、Isabelle、Arend など、実際の証明支援系での書き方については、別の連載記事で個別に扱っています。

---

今後のロードマップ

数珠つなぎの単独記事の全体像は、次のとおりです。

---

補足：本文で省略した用語について

• 本文中の「恒等型」「Martin-Löf 型理論」「∞-亜群」といった専門用語は、意図的に本文からは外しました。この記事の目的は「Haskell 使いに空間としてのデータ型の見方を伝える」ことであり、専門用語の網羅ではないからです。より正確な学習は、続編や下記の参考文献をご参照ください。
   
• 「関数外延性が使える」というのは、Haskell ではなく Cubical Agda や、公理として仮定した Agda/Rocq の話です。Haskell では、factLoop == factRec は書けないままです。本文で紹介した「関数外延性」は、あくまで数学の側で認められているルールであり、Haskell で直接使えるものではない点はご注意ください。
   
• S¹ の base ≡ base の中に「整数の本数だけ道がある」ことは、代数トポロジーの古典的事実「π₁(S¹) = ℤ」として知られています。HoTT の枠組みでこれを形式的に証明した最初の仕事のひとつが、Licata-Shulman による Calculating the Fundamental Group of the Circle in Homotopy Type Theory (LICS 2013) です。

---

参考文献・リンク

• HoTT の体系書: Homotopy Type Theory: Univalent Foundations of Mathematics (HoTT Book, 2013)（PDF が無料公開されています）
• Cubical Agda の公式ドキュメント: Cubical Agda — Agda 2 documentation
• Cubical Agda の標準ライブラリ: agda/cubical (GitHub)
• Curry-Howard 対応の入門: Wadler, "Propositions as Types" (2015)
• 円周の基本群を HoTT で計算した論文: Licata-Shulman 2013
• バージョン管理を HoTT で定式化した論文: Angiuli, Morehouse, Licata, Harper, "Homotopical Patch Theory" (ICFP 2014)

以上、Haskell の Int が持つ「もうひとつの顔」を見ていただきました。

皆様が次に data Foo = Bar | Baz と書くとき、頭の片隅に「Bar と Baz、2つの点を持つ、退屈だけど確かに空間」というイメージ が浮かびましたら、この記事の目的は果たされたことになります。

1. HoTT は 2010 年代前半に体系化された比較的新しい型理論で、2013 年に体系書『Homotopy Type Theory: Univalent Foundations of Mathematics』が出ました。今後、HoTTそのものの入門記事も書く予定です。 ↩

2. refl は HoTT や Agda/Rocq でよく出てくる用語ですが、この記事の本文では「動かない道」という日本語で通します。 ↩

3. 「h-level」は HoTT で登場する用語で、型の「豊かさの層」を階段状に測る指標です。この記事の最後の表で、他の h-level も並べて紹介します。 ↩

4. 関数外延性は、Haskell のような通常のプログラミング言語には備わっていないルールですが、Cubical Agda や、公理として仮定した Agda/Rocq では扱えます。この記事の後続として書く HoTT 入門記事で詳しく触れます。 ↩

5. 「基本群」というのは、base を固定したときに base から base への道全体を、「合成」と「反転」という操作のもとで代数的に整理した構造です。この記事では立ち入りません。 ↩