Haskellのbaseには群も環も体もない ── 代数構造を型クラスでどこまで表現できるか

はじめに

Haskell の 標準ライブラリ ── base と呼ばれる、処理系に最初から付いてくる部分です ── には、群 はありません。

環 もありません。体 もありません。半環 すらありません。

本記事全体に関する注意書き

これは「Haskell で代数を扱えない」という意味ではありません。

外部のライブラリ を導入すれば、群 も 環 も 体 も使えます。
行列 も、テンソル も、ベクトル空間 も扱えます。

algebra、numeric-prelude、linear、hmatrix といった ライブラリ が公開されており、実際に数値計算や記号計算に使われています。

本記事が問うのは、なぜそれらが base に入らなかったのか です。

ここで、以下の点を最初にお伝えさせてください。

「base に存在しない」ことと、「Haskellの型システム で 自然に表現できない」ことは、同じではありません。

前者は 設計上の判断 であり、後者は 言語の性質 です。

本記事は、後者が前者の背景にあると考えて論を進めますが、Haskell 委員会がこの理由で Group を入れなかったと証明するものではありません。

• 型クラスの設計
• コヒーレンス
• 法則の扱い
• 代数階層の設計

これらの観点から考察したもの、とお読みください。

数学の代数構造 を 型クラス で表現できる言語として紹介されることの多い Haskell が、最も基本的な構造さえ標準では持っていない。

そこには、理由 があります。

本記事では、その理由を見ていきます。

この記事の問い

問いは、次の２つです。

• ① なぜ、base に群も環も体も入らなかったのか。

• ② 外部ライブラリを使えば解決するのか。それとも、Haskell の型システムそのものに限界があるのか。

答えを先に述べます。

Haskellの型クラス が宣言できるのは、演算の名前と型 だけです。

その演算が満たすべき法則 ── 順番を変えても答えが同じか、といった性質 ── を、インスタンスの条件 として要求することはできません。

演算が満たすべき法則とは何か

具体例を挙げます。

足し算 という 演算 を考えます。
この演算には、名前 と 型 があります。

(+) :: a -> a -> a

「a を２つ受け取って、a を返す」という型です。

ここまでは、型クラスに書くことができます。

しかし、足し算 には、これ以上の性質 があります。

性質	式で書くと
順番を変えても同じ	a + b = b + a
どこから計算しても同じ	(a + b) + c = a + (b + c)
０を足しても変わらない	a + 0 = a

上の表に掲げた 演算が常に満たすべき条件 を、代数学 では 公理 と呼びます。

Haskell では 法則（law）と呼び、Functor や Monad のドキュメントにも "should satisfy the following laws" と記されています。

本記事でも、以降は 「法則」 という文言で記載することにします。

これらは、型クラスの宣言 に書き加えることはできません。

なお、ここで述べているのは、通常の型クラスの宣言についてです。

Haskell にも、型クラスの外側で法則を扱う仕組みは用意されています。

発展 ── Haskell で法則を扱う４つの仕組み（クリックで展開）

型クラスの宣言に法則を含められないことは、Haskell が法則を扱えないことを意味しません。

型クラスの外側に、いくつもの仕組みが用意されています。代表的なものを４つ紹介します。

１. 反例を探す ── QuickCheck と quickcheck-classes

実用上、最も手軽に利用できる方法の１つです。

QuickCheck は、ランダムな値を大量に生成して、指定した性質が成り立つかを試すライブラリです。

そして quickcheck-classes は、標準的な型クラスの法則を、あらかじめ用意してくれます。

import Data.Proxy (Proxy(..))
import Test.QuickCheck.Classes

main :: IO ()
main = lawsCheck (monoidLaws (Proxy :: Proxy Ordering))

実行すると、次のような出力が得られます。

Monoid: Associative +++ OK, passed 100 tests.
Monoid: Left Identity +++ OK, passed 100 tests.
Monoid: Right Identity +++ OK, passed 100 tests.

semigroupLaws、functorLaws、monadLaws、ordLaws など、代表的な型クラスについて法則の組が用意されています。

なお、検査される項目や必要な制約は、ライブラリの版によって変わります。実際の出力は、お使いの環境でご確認ください。

出典
quickcheck-classes, Hackage

ただし、これはテストであって、数学的な証明ではありません。

有限個のテストケースで法則を評価しているだけで、すべての値について法則が成り立つことを証明するものではありません。

２. 型の等式を表す ── Data.Type.Equality

base に含まれる仕組みです。

data a :~: b where
  Refl :: a :~: a

a :~: b は、「型 a と型 b が等しい」ことを表す型です。
構成子は Refl の１つだけで、両辺が同じときにしか作れません。

これは、Agda や Lean の等式型と同じ発想です。

Data.Type.Equality が直接表すのは、型どうしの等しさです。
「$a + b = b + a$」のような値についての等式を、そのまま :~: に書くことはできません。

出典
Data.Type.Equality, base, Hackage

３. 型に「検査済み」の印を付ける ── Ghosts of Departed Proofs

Matt Noonan が2018年に発表した Ghosts of Departed Proofs（GDP、去りし証明の亡霊）という設計手法があります。

荷札のようなもの、と考えてください。

たとえば「０より大きいと確かめた整数」を考えます。中身はただの整数です。

しかし、「検査済み」という札が付いているものと、付いていないものを、型として区別する。

newtype Checked p a = Checked a

p に注目してください。
左側にありますが、右側の Checked a には現れません。

このように、型の引数として現れるが値としては使われないものを、ファントム型引数と呼びます。
実行時には何のデータも持ちません。

p の役割は、どの種類の検査を通ったかを型として区別することです。

Checked IsPositive Int と Checked IsSorted [Int] は、p の部分が違うので、別の型になります。「正であることを確かめた整数」と「並べ替え済みであることを確かめたリスト」を、混同せずに扱えます。

実際に書くと、こうなります

{-# LANGUAGE RoleAnnotations #-}

module Positive (Checked, IsPositive, checkPositive) where

type role Checked nominal

newtype Checked p a = Checked a

data IsPositive

checkPositive :: Int -> Maybe (Checked IsPositive Int)
checkPositive x
  | x > 0     = Just (Checked x)
  | otherwise = Nothing

３行目が、この仕組みの要です。

module Positive (...) where は、「このまとまりから、外へ何を見せるか」を書く宣言です。

括弧の中に並べたものだけが、外から使えます。

ここでは、型名 Checked、札の種類を表す IsPositive、そして関数 checkPositive だけを見せています。

タロウくん：
newtype の宣言は、その下に書いてありますね。

専任講師：
宣言そのものは、このまとまりの内部にあります。

外へ公開しているのは型名だけです。

タロウくん：
つまり、Checked という値の作り方は、外から見えない。

専任講師：
そこが肝心です。外から Checked 5 と書くことはできません。

構成子を外へ公開しなければ、このまとまりの利用者は札を直接付けられません。

札を付ける責務を、checkPositive のような検査関数へ集中させられます。

type role は何をしているのか

タロウくん：
type role Checked nominal という行が気になります。

専任講師：
これがないと、抜け道が残ります。

タロウくん：
抜け道。

専任講師：
coerce という関数があります。

実行時の表現が同じ型どうしを、無コストで変換するものです。

Checked IsPositive Int と Checked IsSorted Int は、実行時には どちらもただの整数 です。
表現が同じ。

タロウくん：
だから、変換できてしまう。

専任講師：
札を勝手に付け替えられます。

nominal は、「p が違う型どうしを、同じ中身だからといって coerce で付け替えることはできない」と指定するものです。

タロウくん：
構成子を隠すだけでは足りない。

専任講師：
足りません。そこまで揃えて、初めて札が意味を持ちます。

だから、検査済みとして扱える

この型を外から勝手に作れないようにしておけば、この型の値を持っていることを「検査を通ったもの」として扱えます。

受け取った側は、もう調べ直す必要がありません。

そして、札は実行時に消えます。
残るのは中身の整数だけ。
性能の代償もありません。

「去りし証明の亡霊」 という名前は、そこから来ています。

何が保証されて、何が保証されないのか

ここは、正確に述べておきます。

タロウくん：
先生、checkPositive の中身が間違っていたら、どうなりますか。

専任講師：
よい問いです。

たとえば、こう書いたとします。

checkPositive x = Just (Checked x)

検査をしていません。

しかし、これはコンパイルを通ります。

タロウくん：
札は付くけれど、確かめていない。

専任講師：
そのとおりです。

型が保証するのは、「公開された関数を経て IsPositive の札が付いた」という履歴です。

x > 0 を正しく検査していること自体は、checkPositive の実装、レビュー、テスト、あるいは別の検証手段に依存します。

タロウくん：
本記事の主題と、同じ構図ですね。

専任講師：
同じです。
型は、経路を保証します。中身の正しさは、別の手段で確かめることになります。

論文の記述

（原文引用）

sophisticated preconditions can be encoded in Haskell's type system with no run-time overhead, by using proofs that inhabit phantom type parameters attached to newtype wrappers

（筆者による日本語訳）

洗練された事前条件を、実行時のオーバーヘッドなしに Haskell の型システムへ符号化できる。newtype の包みに付けたファントム型引数に、証明を住まわせることによって。

出典
Matt Noonan, "Ghosts of Departed Proofs (Functional Pearl)", Haskell Symposium, 2018年

なお、GDP では、値ごとに一意な名前を型として与える仕組みも用います。上の例は、発想の骨格だけを示したものです。

４. 仕様付きコードを静的に検証する ── LiquidHaskell

型に述語を添えることで、値が満たすべき条件を書けます。

{-@ type Pos = {v:Int | v > 0} @-}

{-@ ... @-} という特別な注釈の中に、「０より大きい整数」という条件を書いています。

このように述語を添えた型を 篩型（refinement type）と呼びます。そして、条件が成り立つかどうかを SMT ソルバ が検証します。

そして、代数の法則も書けます。

{-@ assocPlus :: x:Int -> y:Int -> z:Int
              -> { (x + y) + z == x + (y + z) } @-}

実際に、Monoid、Functor、Applicative、Monad の法則が、この方法で証明されています。

（原文引用）

We used Liquid Haskell to prove the Monoid, Functor, Applicative and Monad Laws [...] for various user-defined instances

（筆者による日本語訳）

我々は Liquid Haskell を用いて、さまざまな利用者定義のインスタンスについて、Monoid、Functor、Applicative、Monad の法則を証明した。

出典
N. Vazou, R. Jhala, "Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)", arXiv:1610.04641, 2016年、§6.3

４つに共通すること

手法	何をするか	保証の根拠
quickcheck-classes	法則の反例を探す	有限回の試行で反例が出ないこと
Data.Type.Equality	型どうしの等しさを表す	型レベルの等式の証拠
GDP	API の境界で不変条件を保つ	抽象化した構成子と、必要に応じたファントム型の証拠
LiquidHaskell	仕様付きコードを静的に検証する	篩型と SMT ソルバ

反例を探すこと、API の設計で不変条件を守ること、静的に検証すること ── どれも「法則を扱う」と言えますが、保証できる範囲と保証の仕組みは同じではありません。

そして、いずれも型クラスの宣言に法則を含めるものではありません。

Monoid のインスタンスを書くときに、結合律の証明を求められることはありません。書き手が別途、これらの仕組みを使って確かめる ── そういう構造になっています。

「法則を守る設計を、使う側が組み立てる」 手法であって、「法則を守ることを、型クラスが求める」 仕組みではないのです。

この違いが、次に見る言語との分かれ目になります。

演算の性質 を 型クラスの宣言 で表現できないと、どのような事態が生じるのでしょうか？

例えば、「引き算」を「足し算」として登録するコード が、コンパイルを通って しまいます。

引き算 は $(5-3)-1 = 1$ と $5-(3-1) = 3$ で、どこから計算するかによって答えが変わる のにもかかわらず、です。

型クラスの宣言に記述できるのは、演算の名前と型までです。

その演算がどう振る舞うべきかを記述する場所 は、用意されていません。

これが、本記事を貫く問題です。

なお、Haskell でも 型クラスの外側であれば、法則を型として扱う手法が存在 します。
それについては、第４部で扱います。

なお、いま挙げた ３つの性質 には、それぞれ名前が付いています。

第２部で正式に扱います。

演算の性質も『型』として表現できる言語がある

同じことを、Lean 4 という言語で書いてみます。

class MyMonoid (α : Type) where
  op    : α → α → α
  unit  : α
  assoc : ∀ a b c : α, op (op a b) c = op a (op b c)

上３行は、Haskell と同じです。演算 op と、単位元 unit を要求しています。

単位元 とは、何と組み合わせても相手を変えない値のことです。

足し算 における $0$、掛け算 における $1$ がそれにあたります。
第２部で改めて扱います。

４行目が違います。

assoc という名前で、「どこから計算しても同じ」という主張そのものを要求しています。

そして、この主張を 証明しなければ、インスタンスを作れません。

引き算で登録しようとすると、どうなるか。

instance : MyMonoid Int where
  op    := fun a b => a - b
  unit  := 0
  assoc := by
    intro a b c
    -- (a - b) - c = a - (b - c) を証明しようとする
    -- 証明できないので、ここでエラーになる
    sorry

sorry は「ここは未証明です」と処理系に伝える印です。
これを書くと警告が出ます。

証明を書こうとしても、書けません。
成り立たないからです。

sorry を使わない、検証済みのコードとしては完成できません。

Haskell では通り、Lean では完成できない。

この違いが、本記事の主題の１つです。

詳しくは第７部で扱います。

なお、これは base に限った話ではありません。

外部ライブラリも、GHC の通常の型クラス解決を使う限り、同じ制約の下にあります。

演算が満たすべき法則を表現できないことが、代数構造の階層を設計するうえでの障害になっています。

なぜ 障害 になるのでしょうか？

代数構造は、法則によって定義されている からです。

半群 と モノイド と 群 の 違い は、演算の数ではなく、どの法則を満たすか にあります。

その法則を型に表せないと、３つの違いは宣言されたメソッドの有無だけになり、「演算が法則を満たす構造」として区別することができません。

メソッドとは、型クラスが「この操作を備えていること」として要求する関数や値のことです。

Semigroup なら演算 <>、Monoid ならそれに加えて単位元 mempty。仮に Group を作るなら、さらに逆元を返す関数が加わります。

つまり、区別の手がかりは「どのメソッドが宣言されているか」だけになります。

その関数が本当に 単位元 や 逆元として振る舞うかどうか は、型からは分かりません。

上の画像解説

①ラベルは鮮明、中身は見えない ── 型クラスが検査するのは「その名前の関数が宣言されているか」だけです。中身が法則を満たすかは検査されません。

この非対称性を、印刷されたラベルと不透明な瓶で表しています。

②虫眼鏡が壁で止まる ── 調べようとしても届かない。破線が瓶の壁で切れ、疑問符で終わる形にしました。

③下部の一文 ── the label is checked — the contents are not。記事の主張そのものです。

この点は、第５部で詳しく扱います。

予備知識は要りません

群、環、体、行列、可換性 ── これらの数学用語は、すべて本文中で説明します。

高校数学の詳細や、抽象代数を学んだ経験は前提にしません。

Haskell の記法も、必要な箇所で説明します。

ただし、型システム や複数の言語の設計比較を扱うため、プログラミングの経験はあったほうが読みやすいはずです。

---

この記事のメッセージ

５行にまとめます。

1. Haskell の base には Semigroup と Monoid はあるが、Group、Ring、Field はない
2. その背景に、複数構造・法則・階層設計という３つの問題がある
3. newtype は１つ目を回避できるが、構造どうしの関係が失われる
4. 法則をコンパイル時に検証させることは、型クラスの仕組みではできない
5. Lean や Rocq では、法則そのものを型クラスの公理として要求できる

以下は、より詳しい要約です。

TL;DR

• Haskell の base に、群・環・体・半環はない。 Monoid と Semigroup はある
   
• ただし、外部ライブラリを使えば代数も行列もテンソルも扱える。 本記事が問うのは、なぜ base に入らなかったのか、である
   
• Num は環ではない。 加算・乗算・符号反転・絶対値を１つのクラスに詰め込んだもので、代数構造と対応してはいない
   
• 代数構造を使いたい場合は、外部ライブラリを使う。 algebra、numeric-prelude など複数あり、階層の切り方がそれぞれ違う
   
• 障害は３つある。 １つの型に１つの実装しか書けないこと（コヒーレンス）、法則を検査できないこと、階層の設計が一意でないこと。このうち前２つは、通常の型クラス機構を使う限り制約として残る
   
• 整数は加法について群、乗法についてモノイドをなす。 しかし、型クラス は１つの型に１つの実装しか許さないので、両方を同時に書けない
   
• Monoid は結合律を要求するが、GHC は確かめない。 嘘 の実装を書いても コンパイルは通る
   
• Num は、言語仕様としては法則を定めていない。 ドキュメントには「慣習的に期待される」環の性質として明記されているが、要求ではない。そして Double は 結合律を満たさないまま Num のインスタンスになっている。
   
• Idris では法則を型で要求できる。 ただし、標準ライブラリ ではなく 外部ライブラリ の機能であり、演算と法則を分けた設計のために階層の構築が難しい
   
• Lean の Mathlib では、群の公理を証明として提出する必要がある。 演算と法則を同じクラスに入れる ことで、Idris の 困難を回避 している
   
• 「逆行列を持つ」という性質は、Haskell の型では表せない。 行列の大きさは型に書けるが、正則性 は中身によって決まる。しかも浮動小数点数では、値としても確実に判定できない
   
• Haskell の強みは、記述の軽さと型クラス解決の一意性。 弱みは、法則の保証がない こと。この２つは交換関係 にある

想定読者

• Haskell の Num や Monoid を使ったことはあるが、その設計理由を考えたことがない方
   
• 抽象代数を学んだことがない方。群も環も体も、本文で説明します。高校数学の詳細も前提にしません
   
• 型クラスやトレイトを設計する立場にある方。抽象化の階層をどう切るかという問題は、代数に限りません
   
• Lean や Rocq に関心がある方。Mathlib との比較を第７部で扱います
   
• 「型で保証する」という言葉の中身を知りたい方

この記事を読む価値

1. Num が何であって何でないか が分かる。そして、なぜ base に代数構造が入らなかったのかが分かる
    
2. 群・環・体を、記号ではなく具体例で理解できる
    
3. 型クラスのコヒーレンスという制約 が、実際に何を妨げるかが分かる。これは base の問題ではなく、言語の設計である
    
4. Sum と Product という newtype が、なぜ存在するのか が分かる
    
5. 法則を検査する仕組みと、しない仕組みの違い が具体的に分かる
    
6. Double が代数の公理を満たさないこと と、それが型に現れない理由が分かる
    
7. 代数構造のライブラリを選ぶとき、何を見ればよいか が分かる
    
8. Haskell、Rust、Idris、Lean 4 の型システム を、同じ軸で比較できる
    
9. Haskell以外の別の言語に乗り換えるべきか、Haskellを使い続けるべきか を、ユースケース別に判断できる

この記事の全体像

赤い枠 が３つあります。

これらは、標準ライブラリ に 代数階層 を採用しようとすると直面する、構造的な設計上の難所 です。

歴史的な経緯を断定するものではありません。 その点は「はじめに」で述べたとおりです。

そして、そのうち第３部と第４部の障害は、通常の型クラス機構を使う限り制約として残ります。 外部ライブラリを導入しても、この点は変わりません。

青い枠が、それを解決した別の体系との比較です。

---

第１部 ── Haskell には、何があるのか

まず、事実を確認します。

対話の形で進めます。話し手は２人です。

• タロウくん ── Haskell を書いたことがある。数学は高校で止まっている。

• 専任講師 ── 型システムと代数を扱う。

---

タロウくん：
先生、Haskell って数学的な言語だと聞きました。群とか環とか、そういうものが型クラスで表現されているんですよね。

専任講師：
そう思われていることが多いですね。

しかし、標準ライブラリを開いてみると、群はありません。

タロウくん：
ない、というのは？

専任講師：
Group という名前の型クラスが、base に存在しないということです。

環もありません。体もありません。

タロウくん：
えっ。じゃあ、何があるんですか。

専任講師：
代数構造に関係するもので base にあるのは、Semigroup と Monoid の２つです。

タロウくん：
２つだけ。

専任講師：
２つだけです。

そこから先はありません。群も、環も、体も、半環も。

タロウくん：
半環というのは？

専任講師：
後で説明します。
ここでは、「環より少し弱い構造」とだけ申し上げておきます。

タロウくん：
でも先生、Haskell で行列計算をしている人がいますよね？

専任講師：
います。
外部のライブラリを使えば、行列もテンソルも扱えます。

群や環の型クラスを提供するライブラリも、複数あります。

タロウくん：
じゃあ、困らないんじゃないですか。

専任講師：
数値計算や線形代数であれば、既存のライブラリで事足ります。

ただし、どの代数階層を採用するか、法則をどう試験するか、既存の Num 系の API とどう共存させるか ── そうした判断は、別途必要になります。

タロウくん：
先生、いま３つ言われましたが、どれも意味が分かりません。

専任講師：
順に説明しましょう。

タロウくん：
まず、「代数階層」とは、何ですか？

専任講師：
半群、モノイド、群、環 ── そういう構造を、どういう順序で積み上げるかという設計です。

タロウくん：
順序に、選択の余地があるんですか？

専任講師：
あります。ライブラリごとに違います。

algebra というライブラリと numeric-prelude というライブラリでは、切り方が異なります。
片方を選ぶと、もう片方とはつながりません。

タロウくん：
どう違うんですか。

専任講師：
algebra は、演算ごとにクラスを分けます。

足し算のためのクラス、掛け算のためのクラス。
整数は、その両方に属させることができます。

タロウくん：
なるほど。

numeric-prelude は？

専任講師：
標準の Num を作り直します。

Additive、Ring、Absolute に分け、Ring の中に足し算と掛け算の両方を置く。

タロウくん：
それぞれ、何を担うんですか？

専任講師：
Additive が足し算と引き算。

Ring が、そこに掛け算を加えたもの。第２部で扱う環にあたります。

Absolute が、絶対値と符号です。

タロウくん：
Num に詰め込まれていた６つが、３つに振り分けられている。

専任講師：
そして、絶対値と符号が別のクラスになった。

タロウくん：
行列やガウス整数でも、Ring には属せるわけですね？

専任講師：
そこが、この分割の狙いです。

タロウくん：
同じ「環」を表すのに、形が違うと？

専任講師：
そうです。
そして、一方の型クラスのインスタンスが、もう一方でそのまま使えるわけではありません。

タロウくん：
最初に決めなければならない、のですね？

専任講師：
後から変えるのは大変です。

タロウくん：
次に「法則をどう試験するか」。

専任講師：
結合律や単位元の性質が、実際に守られているかを確かめる作業です。

タロウくん：
コンパイラが確かめてくれないんでしたね。

専任講師：
だから、テストを書くことになります。

そのテストを誰が書くか、どこまで書くか。
それを決める必要があります。

タロウくん：
テストをするために、Haskell とは別に、Rocq や Lean などの定理証明支援系を使うということですか。

専任講師：
いいえ。別の言語へ移る必要はありません。

タロウくん：
Haskell のまま、できるのですね？

専任講師：
できます。
QuickCheckというライブラリ を使います。

ランダムな値を大量に作って、法則が成り立つかを試す。
Haskell のテストとして書けます。

タロウくん：
では、Lean や Rocq を使う場面は？

専任講師：
目的が違います。

QuickCheck は、反例を探す道具です。有限個の値で試して、破れなければそれでよしとする。

タロウくん：
すべての値では確かめていない。

専任講師：
確かめていません。そこが限界です。

Lean や Rocq は、すべての値について成り立つことを証明します。

タロウくん：
Haskell のコードを、そのまま検証できるわけではない。

専任講師：
証明支援系へ持ち込むには、書き直しが要ります。

タロウくん：
それは、大変ですね。

専任講師：
だから実務では、QuickCheck で足りることが多い。

証明の負担と、得られる保証。 その釣り合いで決まります。

なお、Haskell のコードのまま、より強い保証を得る道もあります。

第４部で触れた LiquidHaskell がそれです。
書き直さずに、述語 を添えて性質を確かめることができます。

タロウくん：
選択肢は、２つに限らないんですね。

専任講師：
保証の強さは、段階的です。

タロウくん：
最後に「Num 系の API との共存」。

専任講師：
Num は、Haskell の標準にある型クラスでした。

タロウくん：
足し算や掛け算ができる、というものですね。

専任講師：
そうです。そして既存のライブラリの多くが、Num を前提に書かれています。

タロウくん：
そこに、別の代数ライブラリを持ち込むと。

専任講師：
衝突します。

numeric-prelude は、標準の Prelude を隠して自前のものに置き換えます。
すると、Num を前提とする他のライブラリと組み合わせにくくなる。

タロウくん：
どちらかを選ばなければならない。

専任講師：
あるいは、変換の層を自分で書くことになります。

タロウくん：
なるほど。「ライブラリを入れれば終わり」ではないんですね。

専任講師：
そこが要点です。

タロウくん：
先生、それでも私は、こう思うんです。

専任講師：
どうぞ。

タロウくん：
外部ライブラリを使えば、代数構造を型として宣言できるんですよね。
群や環のクラスも用意されている。

専任講師：
用意されています。

タロウくん：
だとすると、それで問題解決ということになりませんか？

Python だって、可視化には matplotlib、機械学習には scikit-learn を使います。
標準ライブラリだけでできることは、どの言語でも限られています。

専任講師：
鋭い問いです。そして、半分は正しい。

タロウくん：
半分だけ、ですか？

専任講師：
クラスを用意することは、できます。
Group や Ring という名前の型クラスを作ることはできる。

そこは Python と同じです。

タロウくん：
では、何が違うんですか。

専任講師：
そのクラスに属する型が、群や環の条件を満たしているかどうか。
それを Haskell が確かめてくれるかという問題です。

タロウくん：
Haskellは、確かめてくれないということですか？

専任講師：
確かめません。
外部ライブラリを使っても、この点は変わりません。

タロウくん：
なぜですか？
ライブラリの作り方の問題では？

専任講師：
違います。
Haskell の型クラスという仕組みに、条件を書き込む場所がないからです。

タロウくん：
たとえば、どんな条件ですか？

専任講師：
群であれば、演算について次のことが要求されます。

「どこから計算しても同じ」

「mempty と組み合わせても、相手が変わらない」

「inverse で得たものと組み合わせると、mempty になる」

タロウくん：
Haskellでは、それを書く場所がないと？

専任講師：
class Group a where と書いたあと、そこに並べられるのは操作の名前と型だけです。

inverse :: a -> a とは書けます。
しかし「これが本当に逆元を返す」とは書けません。

タロウくん：
逆元を返さない関数を登録しても、通ってしまうのですね？

専任講師：
通ってしまいます。

タロウくん：
ライブラリを工夫しても、どうにもならない。

専任講師：
なりません。

タロウくん：
それは、Python の matplotlib とは話が違いますね。

専任講師：
違います。
matplotlib は「標準にない機能を足す」ものです。

いま問題にしているのは、「言語の仕組みとして、そもそも表現できないもの」です。

タロウくん：
足りないのではなく、書けない。

専任講師：
そこが要点です。

タロウくん：
では、代数階層のライブラリを使う意味は？

専任講師：
ライブラリを使う意味はちゃんとあります。
名前が付くことです。

Group という型クラスがあれば、「この型は群として扱う」という意図が伝わります。抽象化もできる。

タロウくん：
ただし、その型が本当に群であることは、保証されない。

専任講師：
されません。

結合律を満たすか。
mempty が単位元として振る舞うか。
inverse が逆元を返すか。
そのどれも、確かめられていません。

ドキュメントに「群の公理を満たすこと」と書いてあるだけです。

タロウくん：
つまり、こういうことですか。

その約束を守るかどうかは、型クラスの仕組みの側では検査されない。
守ることを強制もしてくれない。

専任講師：
そのとおりです。

ただし、一点だけ正確に申し上げておきます。

いま「型クラスの仕組み」と限定しました。「Haskell の型システム」とは言っていません。

タロウくん：
違いがあるんですか。

専任講師：
あります。

Haskell にも、条件を型で扱う仕組みはあるのです。冒頭の発展コラムで触れました。

Data.Type.Equality の :~: は、型どうしの等しさを型として表します。

GDP ── Ghosts of Departed Proofs ── は、ファントム型引数に証明を住まわせる設計手法です。

これらは、Haskell の型システムの一部です。

タロウくん：
ファントム型引数。住まわせる。どちらも意味が分かりません。

専任講師：
荷札のようなものだと考えてください。

中身は同じ整数です。しかし**「０より大きいことを確かめ済み」という札が付いているもの**と、付いていないものを、別の型として扱う。

タロウくん：
札の有無で、型が変わる。

専任講師：
そうです。そして札を付ける手段を外に公開しない。実際に検査する関数だけが、札を付けられるようにします。

タロウくん：
検査を通らないと、札がもらえない。

専任講師：
すると、札が付いていること自体が、確かめた証拠になります。

タロウくん：
なるほど。では、これを使えばいいじゃないですか。

専任講師：
何にですか。

タロウくん：
mempty です。「本当に単位元として振る舞う」という札を付ければいい。

専任講師：
札を付けること自体は、できます。

タロウくん：
では、解決では。

専任講師：
誰が、その札を付けるのですか。

タロウくん：
えっ。

専任講師：
先ほどの例では、「０より大きいか」を実際に調べる関数が札を付けていました。

タロウくん：
はい。

専任講師：
では、「この mempty は単位元として振る舞う」ことを、どうやって調べますか。

タロウくん：
……すべての値について、確かめる。

専任講師：
**多くの型では、値が無限にあります。**実行時に確かめ切ることはできません。

タロウくん：
では、証明する。

専任講師：
通常の Haskell には、値についての法則を証明として書き、それを型クラスの条件にする仕組みがありません。

札を付ける関数を書けたとしても、その関数が本当に確かめているという保証は、どこにもない。

タロウくん：
待ってください。それはつまり、こういうことですか。

「単位元であることは検証済みです」という札がかけられていても、本当に検証したのかどうかは、札を付けたプログラマに委ねられている。

専任講師：
そのとおりです。

タロウくん：
だとすると、GDP には意味がないんじゃないですか。

結局、プログラマを信じるしかないなら、ドキュメントに書いてある約束と何が違うんですか。

専任講師：
鋭い問いです。そして、扱う性質によって答えが変わります。

タロウくん：
性質によって。

専任講師：
「０より大きい」であれば、検査する関数を実際に書けます。

checkPositive x
  | x > 0     = Just (Checked x)
  | otherwise = Nothing

この関数の中身は、読めば確かめられます。

そして、この関数を通らなければ札は付きません。

タロウくん：
検査が、コードとして存在している。

専任講師：
そこが違いです。

タロウくん：
では、単位元の場合は。

専任講師：
書けません。

すべての値について確かめる関数は、存在しえない。

だから、札を付ける関数は「無条件で札を付ける」ものになります。

タロウくん：
それでは、何も確かめていない。

専任講師：
確かめていません。そのとおり、ドキュメントの約束と変わりません。

タロウくん：
つまり、GDP が意味を持つのは。

専任講師：
実行時に確かめられる性質だけです。

「０より大きい」「並べ替え済みである」「空でない」── こうしたものには、確かに効きます。検査を書き忘れる事故を、型で防げます。

タロウくん：
すべての値について成り立つ法則には、効かない。

専任講師：
効きません。そこが、GDP の射程です。

タロウくん：
なるほど。意味がないのではなく、使える場所が違う。

専任講師：
そういうことです。

タロウくん：
先生、もう一度整理させてください。

専任講師：
どうぞ。

タロウくん：
私が最初に挙げたのは、単位元、逆元、可換性、そして行列の正則性でした。

専任講師：
はい。

タロウくん：
いまの話でいくと、**行列の正則性は GDP で扱えそうです。**実行時に確かめられますから。

専任講師：
そこは、もう一段の注意が要ります。

タロウくん：
まだ何かあるんですか。

専任講師：
正則かどうかは、行列式という量を計算して判定します。その計算に、浮動小数点数の誤差が入ります。

タロウくん：
確かめたつもりで、確かめられていない。

専任講師：
理論上ゼロになるはずの値が、$10^{-18}$ 程度になることがあります。
ゼロでないと判定されてしまう。

タロウくん：
札は付くけれど、当てにならない。

専任講師：
そういう場合があります。
この話は、本記事の第８部で詳しく扱います。

タロウくん：
分かりました。
では、残る３つ ── 単位元、逆元、可換性は？

専任講師：
すべて、演算についての法則です。

タロウくん：
つまり、すべての値について成り立つかどうかの話。

専任講師：
そうです。だから GDP では扱えません。

タロウくん：
整理できました。

私が挙げた４つのうち、３つは演算についての法則で、GDP で守れるものではない。

残る１つ ── 正則性は個々の値の性質ですが、浮動小数点数の誤差という別の問題がある。

専任講師：
よくまとまりました。

タロウくん：
では、結局のところ ── instance Group MyType where と書いたとき、結合律の証明を求められることは。

専任講師：
ありません。

GDP を使っても、:~: を使っても。

そのクラスに属するための条件として、法則の証明を要求する場所がない。

タロウくん：
GDP がしているのは、別のことなんですね。

専任講師：
使う側が、自分で設計を組み立てているのです。

値を作る手段を外に公開せず、検査を通った値だけを返す関数を用意する。
そうして、その型の値が満たすべき条件を守る。

タロウくん：
型クラスが要求しているのではない。

専任講師：
そこが違いです。

「法則を守る設計を、使う側が組み立てる」 手法であって、「法則を守ることを、型クラスが求める」 仕組みではありません。

タロウくん：
だから、外部ライブラリでも変わらない んですね。

専任講師：
変わりません。

タロウくん：
分かってきました。

専任講師：
この違いを詳しく見るのが、本記事の第３部から第５部です。

タロウくん：
では、何が問題なんですか。

専任講師：
問題というより、問いです。

なぜ、それらが base に入らなかったのか。

タロウくん：
誰も必要としなかったから、ではなくて。

専任講師：
必要とされてきました。議論も続いています。

それでも入っていない。そこには、設計上の難所があるわけです。

タロウくん：
その理由が、この記事の主題ということですね。

専任講師：
そうです。

タロウくん：
分かりました。

あ、でも先生。base には Num というのがありますよね。数を扱う型クラスが。

専任講師：
あります。Num はあります。

しかし、Num は数学的な意味での「環」を直接表す型クラスではありません。

タロウくん：
どういうことですか。足し算も掛け算もできるのに。

専任講師：
定義を見てみましょう。

class Num a where
  (+), (-), (*) :: a -> a -> a
  negate        :: a -> a
  abs           :: a -> a
  signum        :: a -> a
  fromInteger   :: Integer -> a

タロウくん：
えっと、読み方が分かりません。

専任講師：
順に説明します。

class Num a where は、「型 a が Num というクラスに属するとは、以下の操作を持つことである」という宣言です。

:: は「〜という型を持つ」を表す記号です。

(+) :: a -> a -> a は、「a を受け取り、a を受け取り、a を返す関数」です。足し算ですね。

タロウくん：
矢印が２つあるのは、引数が２つあるということですか。

専任講師：
そう理解して差し支えありません。

正確には、「a を受け取って、『a を受け取って a を返す関数』を返す関数」です。引数を１つずつ受け取る形になっています。

この流儀を カリー化 と呼びます。関数型言語では標準的な書き方です。

タロウくん：
分かりました。それで、abs と signum は。

専任講師：
abs は絶対値、signum は符号です。

タロウくん：
それが問題なんですか。

専任講師：
問題です。

数学で「環」と呼ばれる構造には、絶対値も符号もありません。

タロウくん：
えっ、じゃあ Num は何なんですか。

専任講師：
「数っぽく振る舞う型」を、実用の都合でまとめたものです。

タロウくん：
実用の都合。

専任講師：
Num は、少なくとも現在の形では、数学でいう環の公理をそのまま写した階層ではありません。

加減乗の演算に加えて、整数からの変換、絶対値、符号を含みます。数値を扱うための入口として設計されており、環の定義には含まれない操作も入っています。

タロウくん：
だから、階層になっていない。

専任講師：
そうです。半群、モノイド、群、環 ── そういう積み上げにはなっていません。

なお、この設計については Haskell Prime という言語仕様の改訂を議論する場でも取り上げられており、代替案が検討されてきました。

タロウくん：
でも、実際に足し算も掛け算もできるじゃないですか。

専任講師：
できます。ただ、それが「環である」ことを意味しません。

具体的な問題を挙げましょう。

行列を Num のインスタンスにしようとすると、abs と signum を実装しなければなりません。

タロウくん：
行列の絶対値。

専任講師：
数学的に、意味のある定義がありません。

タロウくん：
じゃあ、どうするんですか。

専任講師：
エラーを投げる実装を書くか、無理やり何かを返すか。どちらかです。

タロウくん：
他にもありますか。

専任講師：
ガウス整数がそうです。

タロウくん：
それは何ですか。

専任講師：
複素数のうち、実部と虚部がどちらも整数のものです。$3 + 2i$ のような数ですね。

タロウくん：
複素数というのは。

専任講師：
２乗すると $-1$ になる数 $i$ を使って、$a + bi$ の形に書ける数です。
実数だけでは解けない方程式を扱うために導入されました。

タロウくん：
そのガウス整数でも、絶対値が問題になると。

専任講師：
ガウス整数には「大きさ」に相当する量がありますが、それは整数になるとは限りません。

そして符号に至っては、意味のある定義がありません。
実数のように「正か負か」という区別ができないからです。

タロウくん：
なるほど。

タロウくん：
型クラスに属するために、意味のない関数を実装させられる。

専任講師：
そういう構造になっています。

Haskell Prime という、言語仕様の改訂を議論する場でも、この点は指摘されてきました。

タロウくん：
改善されなかったんですか。

専任講師：
議論は続いていますが、base の Num は今も同じ形です。

既存のコードとの互換性が理由です。

---

対話に出てきた事実を整理します

base にある代数関連の型クラス

class Semigroup a where
  (<>)    :: a -> a -> a
  sconcat :: NonEmpty a -> a
  stimes  :: Integral b => b -> a -> a

class Semigroup a => Monoid a where
  mempty  :: a
  mappend :: a -> a -> a
  mconcat :: [a] -> a

Semigroup は、２つの値を組み合わせる演算 <> を持つことを要求します。

sconcat と stimes には既定の実装があるため、インスタンスを書くときに必要なのは <> だけです。

Monoid は、それに加えて mempty という特別な値を持つことを要求します。

mappend は <> と同じもので、既定の実装が mappend = (<>) となっています。歴史的な経緯で残っているメソッドです。

mconcat はリスト全体をまとめる関数で、こちらにも既定の実装があります。

class Semigroup a => Monoid a の => は、「Monoid に属するには、先に Semigroup に属していなければならない」という指定です。

この上位クラス関係は、base-4.11.0.0 で導入されました。それ以前は Monoid が独立していました。

base にない型クラス

• Group（群）
• Ring（環）
• Field（体）
• Semiring（半環）

なお、PureScript という別の言語では、Semiring が標準ライブラリに入っています。Haskell の設計は、この点でも唯一の選択肢ではありません。

---

第２部 ── 群・環・体とは何か

ここまで、「群」「環」「体」 という語を、説明せずに使ってきました。

本節で説明します。

数学の予備知識は仮定しません。具体例から始めます。

出発点 ── 演算とは何か

演算 とは、２つのものから１つのものを作る規則です。

足し算は演算です。$3$ と $5$ から $8$ を作ります。

掛け算も演算です。
文字列の連結も演算です。「abc」と「def」から「abcdef」を作ります。

そして、演算にはさまざまな性質があります。

結合律

$(a + b) + c$ と $a + (b + c)$ が、常に等しい。

この性質を 結合律（associativity）と呼びます。

足し算は結合律を満たします。$(1+2)+3 = 6$ で、$1+(2+3) = 6$ です。

引き算は満たしません。$(5-3)-1 = 1$ ですが、$5-(3-1) = 3$ です。

結合律が成り立つと、括弧を書かずに済みます。
$a + b + c$ と書いて、どちらの順で計算しても同じだからです。

単位元

何と組み合わせても、相手を変えない値。

足し算における $0$ がそれです。$a + 0 = a$ で、$0 + a = a$ です。

掛け算では $1$ がそうです。文字列の連結では、空文字列がそうです。

この値を 単位元（identity element）と呼びます。

逆元

組み合わせると単位元になる相手。

足し算における $-a$ がそれです。$a + (-a) = 0$ になります。

掛け算では $1/a$ がそうです。$a \times (1/a) = 1$ になります。

ただし、$a$ が $0$ の場合は別です。$0$ に何を掛けても $1$ にはなりません。

この値を 逆元（inverse element）と呼びます。

ただし、逆元は常に存在するとは限りません。

整数の掛け算では、$2$ の逆元は $1/2$ ですが、これは整数ではありません。

文字列の連結にも、逆元はありません。「abc」と何かを連結して空文字列にすることはできません。

---

ここまでを組み合わせる

以上の性質を、どこまで持つかで構造の名前が決まります。

名前	演算	結合律	単位元	逆元
半群（semigroup）	１つ	あり	──	──
モノイド（monoid）	１つ	あり	あり	──
群（group）	１つ	あり	あり	あり

半群 は、結合律を満たす演算を１つ持つだけの構造です。

モノイド は、それに単位元が加わったものです。

群 は、さらに逆元が加わったものです。

具体例で確かめます

文字列の連結は、モノイドです。

結合律を満たし、空文字列という単位元を持ちます。しかし逆元がないので、群ではありません。

整数の足し算は、群です。

結合律を満たし、$0$ という単位元を持ち、$-a$ という逆元を持ちます。

整数の掛け算は、モノイドです。

結合律を満たし、$1$ という単位元を持ちます。しかし $2$ の逆元 $1/2$ は整数ではないので、群ではありません。

ここが重要です。

整数は、足し算については群であり、掛け算についてはモノイドである。

同じ「整数」という型が、演算によって異なる構造をなします。

この事実が、第３部で問題を引き起こします。

---

環 ── 演算が２つある構造

ここまでは、演算が１つの場合でした。

環（ring）は、演算を２つ持つ構造です。

足し算と掛け算にあたる２つの演算があり、次を満たします。

なお、**本記事では乗法の単位元 $1$ を持つものを「環」と呼びます。**文献によっては、$1$ を要求しない流儀もあります。その場合、$1$ を持つものを「単位的環」と呼んで区別します。

条件	内容
足し算について	可換群をなす（後述）
掛け算について	モノイドをなす（結合律と単位元 1）
分配律	a × (b + c) = a × b + a × c および (a + b) × c = a × c + b × c

可換群 の「可換」を説明します。

可換性

$a + b$ と $b + a$ が、常に等しい。

この性質を 可換性（commutativity）と呼びます。

足し算は可換です。$3 + 5$ も $5 + 3$ も $8$ です。

引き算は可換ではありません。$5 - 3$ は $2$ ですが、$3 - 5$ は $-2$ です。

可換群 とは、可換性も満たす群のことです。

分配律

$$a \times (b + c) = a \times b + a \times c$$

この式は、２つの演算の関係を定めています。

掛け算が足し算の上に「分配される」という性質です。

なお、条件はこれだけではありません。

$$(a + b) \times c = a \times c + b \times c$$

こちらも必要です。左から掛ける場合と、右から掛ける場合の両方を要求します。

掛け算が 可換 なら、片方から他方が従います。

しかし、この後で見るように、掛け算が 可換でない構造 もあります。

そのため、両方を条件に含めます。

環の定義に分配律が入っているのは、２つの演算が無関係ではないことを要求するためです。

分配律 がなければ、足し算と掛け算という２つの演算が、たまたま同じ対象の上に乗っているだけになってしまいます。

環の例

整数 は 環 です。

足し算 について 可換群、掛け算 について モノイド 、そして 分配律 を満たします。

多項式 も 環 です。

多項式とは、$x^2 + 3x + 1$ のように、文字の累乗と数を組み合わせた式のことです。

足し算ができます。$(x + 1) + (x + 2) = 2x + 3$ です。

掛け算もできます。$(x + 1) \times (x + 2) = x^2 + 3x + 2$ です。

そして、分配律も成り立ちます。だから環になります。

同じ大きさの正方行列も環です。

ここは正確に述べる必要があります。

行列 は、大きさが揃っていなければ足せません。

掛け算 に至っては、行と列の数が噛み合わなければ計算できません 。

しかし、$n$ 行 $n$ 列の行列だけを集めれば、その中で 足し算 も 掛け算 も 閉じます。

これを $M_n(R)$ と書きます（$R$ は成分の属する環）。

そして、次の点が他と違います。

---

非可換 ── 順番を変えると答えが変わる

行列の掛け算は、可換ではありません。

$A \times B$ と $B \times A$ が、一般には異なります。

行列 とは、数を長方形に並べたものです。

$$A = \begin{pmatrix} 1 & 2 \cr 3 & 4 \end{pmatrix}$$

これは２行２列の行列です。

なぜ、こんなものを考えるのか。

行列は、点を別の点へ移す操作を表します。回転、拡大、鏡映といった変換が、行列で書けます。

そして、２つの行列を掛けることが、２つの変換を続けて行うことにあたります。

行列の掛け算の規則は、その意味から導かれます。規則そのものはここでは扱いません。重要なのは、順番を変えると結果が変わるという事実です。

具体例を挙げます。

$$A = \begin{pmatrix} 1 & 1 \cr 0 & 1 \end{pmatrix}, \quad B = \begin{pmatrix} 1 & 0 \cr 1 & 1 \end{pmatrix}$$

$$AB = \begin{pmatrix} 2 & 1 \cr 1 & 1 \end{pmatrix}, \quad BA = \begin{pmatrix} 1 & 1 \cr 1 & 2 \end{pmatrix}$$

違います。

このような環を 非可換環 と呼びます。

そして、これが実世界の構造です。

回転を２つ組み合わせるとき、順番を変えると結果が変わります。
ルービックキューブの操作も同じです。行列は、そういう操作を表すための道具です。

機械学習を扱う方には、より身近な例があります。

深層学習では、層を重ねるごとに行列を掛けていきます。
この順序を入れ替えると、まったく別の変換になります。

画像処理でも同じです。
「回転してから横方向だけ２倍に引き伸ばす」のと、「横方向だけ２倍に引き伸ばしてから回転する」のとでは、結果が違います。

ただし、注意が必要です。

縦横を同じ倍率で拡大する場合は、回転と順序を入れ替えても結果が変わりません。
可換なのです。

順序が問題になるのは、変換が方向によって異なる働きをする場合 です。
片方向だけの引き伸ばしや、傾ける変換がそれにあたります。

非可換性は、抽象的な性質ではありません。
順序が意味を持つ計算では、実際に現れます。

体 ── 割り算ができる環

体（field）は、環のうち、$0$ 以外のすべての要素が掛け算の逆元を持つものです。

先ほど述べたとおり、$0$ には掛け算の逆元がありません。だから $0$ を除きます。

つまり、$0$ で割ること以外は、割り算ができます。

なお、体の定義には「掛け算が可換であること」も含めるのが通例です。
可換でないものは 斜体 または 可除環 と呼び、区別します。

四元数 がその例です。

複素数が実数を２つ組にしたものだとすれば、四元数は４つ組にしたものです。
$0$ 以外のすべての要素が掛け算の逆元を持ちますが、掛け算は可換ではありません。

３次元の回転を表すのに使われ、コンピュータグラフィックスやロボット工学で実用されています。

有理数（分数）は体です。実数 も体です。複素数 も体です。

整数は体ではありません。
$2$ で割ると整数の外に出てしまうからです。

構造の一覧

構造	演算	特徴
半群	１つ	結合律
モノイド	１つ	＋単位元
群	１つ	＋逆元
可換群	１つ	＋可換性
半環	２つ	足し算がモノイド、掛け算がモノイド、分配律
環	２つ	足し算が可換群、掛け算がモノイド、分配律
可換環	２つ	＋掛け算も可換
体	２つ	＋ 0 以外に掛け算の逆元

半環 は、環 から 「足し算の逆元」を外したもの です。

自然数 がその例になります。
$0, 1, 2, \ldots$ という数の集まりです。

$3 - 5$ を計算しようとすると $-2$ になり、自然数の外に出て しまいます。
つまり、引き算 ができません。

足し算と掛け算はできます。

だから、環 にはなりませんが 半環 にはなります。

いちばん単純な代数構造からスタートして、演算が満たすべき法則をひとつひとつ付け加えていくことで、より多くの法則を備えた、複雑な代数構造へと辿ることができます。

順にたどってみましょう。

出発点は マグマ です。演算が１つあるだけで、法則は何もありません。

ここに、法則を１つずつ加えていきます。

まず 結合律 を加えると、半群 になります。
そこへ 単位元 を加えると モノイド、
さらに 逆元 を加えると 群、
そして 可換性 を加えると 可換群 です。

ここまでは、演算が１つでした。

次に、演算を２つに増やします。

足し算 と 掛け算 を用意し、分配律で結ぶ と、 半環 になります。

そこへ 足し算の逆元 を加えると、 環 が得られます。

さらに、掛け算も可換にする と、 可換環 になります。

さらに ０でない場合に、掛け算の逆元 を加えると 体 が得られます。

ここから先は、別の集合が関わってきます。

環の要素を 外から掛ける操作 を加えると、加群 になります。

その環が体であれば、ベクトル空間 です。

そして、ベクトル空間 に 要素どうしの掛け算 を加えると、多元環（たげんかん、algebra）になります。

英語では algebra ですが、日本語で「代数」と訳すと学問分野の名前と紛らわしくなります。
そのため、「多元環」 または 「線型環」 と呼ばれます。

ベクトル空間では、要素を足すことと、体の要素を外から掛けることができました。

そこに、「要素どうしを掛ける」という演算 を加えたものが、多元環 です。

行列がその例です。
行列は足せますし、実数倍もできます。
そして、行列どうしを掛けることもできます。

この「シンプルな代数構造から複雑な代数構造へ」と並べたときに、その並べ方は、一通りに収まらず、複数の並べ方が可能なのです。

たとえば、「順番を変えても同じ」という「可換性」と呼ばれる性質 があります。

整数の足し算 はこの性質を満たしますが、行列の掛け算 は満たしません。

さて。ここで、この性質を持つものと持たないもの を、代数構造の配置図の どの段階で分けるのが適切 でしょうか？

• モノイドの段階 で分けるのか？
• 群の段階 か？
• それとも 環になってから か？

決め手がありません。

このように、代数構造を単純なものから複雑なものへと配置しようとすると、その配置の仕方は１通りに定まらず、複数の設計が成り立ちます。

実際に、Haskell 、Idris 2 、Isabelle/HOL 、Agda 、Rocq
── これらの言語で使われている 代数ライブラリ は、互いに異なる階層を採用しています。

言語の仕様が違うから、というだけではありません。

同じ Haskell の中でも、algebra と numeric-prelude では切り方が異なります。
このことについては、第１部ですでに確認済みです。

個々の代数構造を、どう配置するかは、ライブラリの設計者が決めることなのです。

この問題を、第５部で扱います。

ここまでを並べてみる

いちばん単純な代数構造から始めて、演算が満たすべき法則をひとつずつ加えていくことができます。

まず、演算が１つ の場合から見ていきましょう。

構造	何を加えたか
マグマ	演算が１つあるだけ。法則は何もない
半群	＋結合律
モノイド	＋単位元
群	＋逆元
可換群	＋可換性

次に、演算が２つの代数構造を見てみます。

構造	何を加えたか
半環	足し算と掛け算、そして分配律
環	＋足し算の逆元
可換環	＋掛け算も可換
体	＋０以外に掛け算の逆元

さらに先があります。

環や体の要素を「外から掛ける」という操作を加えると、別の構造が現れます。

構造	何を加えたか
加群	環の要素を、外から掛けられる
ベクトル空間	体の要素を、外から掛けられる
代数	ベクトル空間に、要素どうしの掛け算を加えたもの

このように、単純なものから複雑なものへと辿る ことができますが、その並べ方は、複数の異なる並べ方が可能 なのです。

---

第３部 ── 障害１ コヒーレンス

この部で分かること
整数が加法と乗法の両方でモノイドになるという事実が、Haskell ではなぜ１つの型クラスに共存できないのか。そして、Sum と Product という newtype が、なぜ存在するのか。

第２部の最後で、次の事実を確認しました。

整数は、足し算については群であり、掛け算についてはモノイドである。

この事実を、Haskell の型クラスで表現しようとすると、最初の壁に当たります。

何が問題なのか

型クラスのインスタンスを書いてみます。

instance Semigroup Integer where
  x <> y = x + y

instance Monoid Integer where
  mempty = 0

instance Semigroup Integer where は、「型 Integer は Semigroup に属する」という宣言です。

演算 <> を足し算とし、単位元 mempty を $0$ としました。

演算と単位元を、別のインスタンス宣言に書いている点に注意してください。Monoid は Semigroup を上位クラスに持つので、演算はそちらに書きます。

これで、整数が足し算についてモノイドであることを表現できました。

次に、掛け算についても書きたくなります。

instance Semigroup Integer where
  x <> y = x * y

instance Monoid Integer where
  mempty = 1

これは書けません。

コンパイルエラーになります。「重複したインスタンス宣言である」と言われます。

理由 ── コヒーレンス

Haskell では、同じ型と型クラスの組に対して、競合するインスタンスを複数持たせない設計になっています。

そのため、x <> y という式を書いたとき、どのインスタンスが使われるかが一意に決まります。この性質を コヒーレンス（coherence）と呼びます。

なお、GHC には OverlappingInstances のような拡張があり、重なりのあるインスタンスを許す設定も存在します。しかし標準的な使い方では、重複したインスタンス宣言はエラーになります。

なぜ、そうなっているのか。

x <> y という式を書いたとき、その意味が一意に決まってほしいからです。

もし Integer に対する Monoid のインスタンスが２つあると、3 <> 5 が $8$ なのか $15$ なのか分かりません。

書かれた場所によって意味が変わる、ということになります。

コヒーレンスは、その曖昧さを排除するための制約です。

回避策 ── newtype で包む

この回避策は、公式ドキュメントに明記されています。

Data.Monoid のドキュメントには、次の記述があります。

（原文引用）

Some types can be viewed as a monoid in more than one way, e.g. both addition and multiplication on numbers. In such cases we often define newtypes and make those instances of Monoid, e.g. Sum and Product.

（筆者による日本語訳）

ある型が、複数の仕方でモノイドとみなせることがある。たとえば数における加法と乗法である。そうした場合、我々はしばしば newtype を定義し、それらを Monoid のインスタンスとする。Sum と Product がその例である。

出典
Data.Monoid, base, Hackage

「複数の仕方でモノイドとみなせる」 という問題を、標準ライブラリ自身が認識していることが分かります。

では、その newtype とは何か。

newtype は、既存の型に新しい名前を付ける宣言です。

base には Sum と Product という型が用意されていますが、ここでは仕組みを確かめるために、同じものを自分で書いてみます。

newtype Additive a       = Additive       { getAdditive       :: a }
newtype Multiplicative a = Multiplicative { getMultiplicative :: a }

Additive Int と Multiplicative Int は、中身はどちらも Int ですが、型としては別物です。

したがって、それぞれに Monoid のインスタンスを書けます。

instance Num a => Semigroup (Additive a) where
  Additive x <> Additive y = Additive (x + y)

instance Num a => Monoid (Additive a) where
  mempty = Additive 0

instance Num a => Semigroup (Multiplicative a) where
  Multiplicative x <> Multiplicative y = Multiplicative (x * y)

instance Num a => Monoid (Multiplicative a) where
  mempty = Multiplicative 1

Num a => は、「型 a が Num に属しているなら」という条件です。

演算 <> は Semigroup に、単位元 mempty は Monoid に書きます。

先ほど見たとおり、Monoid は Semigroup を上位クラスに持つためです。

使うときは、こうなります。

getAdditive       (foldMap Additive       [1,2,3,4])   -- 10
getMultiplicative (foldMap Multiplicative [1,2,3,4])   -- 24

なお、base の Sum と Product に対して、上のようなインスタンスを自分で書くことはできません。

既に base が提供しているため、重複したインスタンス宣言になるからです。

そのため、ここでは別の名前を使いました。

foldMap は、リストの各要素を包んでから、すべてを <> でつなげる関数です。

どちらのモノイドを使うかを、型で指定しているわけです。

なぜ、これが根本的な解決ではないのか

newtype で包む ── この方法は、確かに有効です。
base に Sum と Product が用意されており、広く使われています。

しかし、次の課題が残ります。

第１に、包んで外す手間がかかります。

Sum で包み、計算し、getSum で取り出す。この往復が、コードに現れ続けます。

第２に、構造が増えるたびに newtype が増えてしまいます。

base には、Sum、Product のほかに Min、Max、Any、All、First、Last、Dual、Endo などがあります。

いずれも、「同じ型に対する別のモノイド構造」を表すためのもの です。

たとえば Any と All は、どちらも Bool についてのモノイドです。
Any は「または」、All は「かつ」を演算とします。

Bool という１つの型に対して、２つのモノイド構造がある
── それを表すために、２つの newtype が必要になってしまうわけです。

第３に、構造どうしの関係が失われてしまいます。

Sum Integer と Product Integer は、型 としては、互いに無関係 です。

しかし、数学的には、この２つは互いに無関係ではありません。分配律で結ばれている からです。

環という構造は、まさにその関係を表すものでした。

newtype で 分離 すると、その関係を表現する場所がなくなってしまう のです。

他の言語はどうしているか

Rust も 同じ制約 を持ちます。

１つの型に対する１つのトレイトの実装は、１つだけだからです。

しかし、Agda、Lean、Rocq は事情が異なります。

Haskell とは 別の方法 で、同じ対象に複数の数学的構造を関連 づけられるからです。

ただし、その仕組みは三者三様 です。

Lean と Rocq は 型クラスの探索 によって、
Agda は インスタンス引数またはレコードの明示的な受け渡し によって、複数の構造を区別します。

Rocq にはさらに、Mathematical Components が用いる canonical structures という別の仕組みもあります。

ここでは Lean を例にとり、見てみましょう。

Lean 4

先ほど書けなかったものを、Lean で書いてみます。

注意
以下は、インスタンス探索の順序を観察するためだけの最小例です。
実際の Lean や Mathlib では、同一のクラスと型に競合するインスタンスを複数置く設計は、原則として避けます。
加法と乗法は AddMonoid と Monoid のように別のクラスへ分け、必要なら局所的なインスタンスや、構造の明示的な受け渡しを使います。
推奨される設計は、この節の最後で扱います。

class MyMonoid (α : Type) where
  op   : α → α → α
  unit : α

instance addMonoid : MyMonoid Int where
  op   := fun a b => a + b
  unit := 0

instance mulMonoid : MyMonoid Int where
  op   := fun a b => a * b
  unit := 1

Haskell では、整数に対する Monoid の インスタンスを２つ書くと、重複したインスタンス宣言としてコンパイルエラーに なりました。

Lean では、MyMonoid Int の　インスタンスを加法と乗法の２つ書いても、コンパイルエラーになりません。

instance addMonoid のように、インスタンスに名前を付けている点に注目してください。

Haskell では、インスタンスに名前を付けません。付ける必要がないからです。１つしかないので。

Lean では 複数ある ので、区別する手段が必要になります。

では、どちらが使われるのか

#eval MyMonoid.op (3 : Int) 5

#eval は、式を評価して結果を表示する命令です。

この場合、後に書かれた mulMonoid が選ばれ、$15$ が返ります。

ただし、その理由は「後勝ち」という単純なものではありません。正確に説明します。

Lean の 公式リファレンス には、こう記されています。

（原文引用）

There may be multiple possible instances for a given class; in this case, declared priorities and order of declaration are used as tiebreakers, in that order, with more recent instances taking precedence over earlier ones with the same priority.

（筆者による日本語訳）

あるクラスについて、可能なインスタンスが複数存在しうる。その場合、宣言された優先度と宣言の順序が、この順で決着をつけるために使われる。同じ優先度であれば、より新しいインスタンスが、それ以前のものに優先する。

出典
Instance Synthesis, The Lean Language Reference

何が起きているのか

MyMonoid.op 3 5 と書いたとき、Lean は、「 どのインスタンスの op を使うのか」を 自分で判断 します。

Lean は、候補を順に試していきます。

MyMonoid.op (3 : Int) 5 と書いたとき、Lean が探すのは「MyMonoid Int のインスタンス」です。

候補は２つあります。addMonoid と mulMonoid です。

ここで問題になるのは、どちらが適切かではありません。

Lean は「書き手がどちらを意図したか」を判定しません。
そもそも、判定する材料がない のです。

どちらも MyMonoid Int のインスタンスとして成立しています。
型からは区別がつきません 。

では、何で決まるのか。

試す順番です。優先度が指定されていればその順、指定がなければ宣言の順。そして後から宣言されたものほど、先に試されます。

先に試したものが MyMonoid Int のインスタンスとして使えるなら、そこで探索は終わります。

この例では、後に書かれた mulMonoid が先に試され、そのまま採用されます。
だから $15$ が返るのです。

---

タロウくん：
待ってください。

それだと、addMonoid が適切な場面でも、mulMonoid が後に宣言されていたり、優先度が高く指定されていた場合は、mulMonoid が選ばれるということですか？

専任講師：
そのとおりです。

タロウくん：
おかしくないですか。

専任講師：
おかしいですね。
ですから、こういう書き方は実際にはしません。

タロウくん：
では、どう書くんですか。

専任講師：
方法は２つあります。

タロウくん：
２つ。

専任講師：
１つ目は、使うインスタンスをその場で指定する方法です。

#eval @MyMonoid.op Int addMonoid 3 5   -- 8
#eval @MyMonoid.op Int mulMonoid 3 5   -- 15

@ を付けると、Lean が自動で選ぶ部分を、プログラマが自分で書けるようになります。

タロウくん：
addMonoid と直接書いている。

専任講師：
そうなんです。

Lean 4に探索させるのではなく、プログラマが明示的に指定した方のインスタンスが適用されることになります。

タロウくん：
それなら、間違いようがない。

専任講師：
問題解決ですね。
ただし、@以降の文字列を、プログラマが毎回書かなくてはならず、手間になります。

タロウくん：
たしかに、手間ですね。
２つ目の方法についても教えて下さい。

専任講師：
２つ目は、クラスそのものを分けてしまう方法 です。

加法のための AddMonoid、
乗法のための Monoid。

別のクラスなら、互いに競合しません。

タロウくん：
MyMonoid が１つだから、困っていたわけですね。

専任講師：
そこが問題の発端でした。

Mathlib はこの２つ目の方法を採用しています。

Lean は、どちらが適切かを判断するのか

タロウくん：
先生、根本的なことを伺います。

addMonoid と mulMonoid のうち、その計算にどちらがふさわしいか。
Lean はそれを判断してくれるんですか。

専任講師：
判断しません。

判断する材料がないからです。

タロウくん：
材料、ですか？

専任講師：
MyMonoid.op (3 : Int) 5 という式が持っている情報は、「Int の値を２つ受け取る」ということだけです。

足したいのか掛けたいのか ── その意図は、式のどこにも書かれていません。

タロウくん：
書かれていないものを、判断しようがない。

専任講師：
そうなりますね。

タロウくん：
では、Lean は何をしているんですか？

専任講師：
「MyMonoid Int のインスタンスを１つ見つけてくる」 という作業だけです。

見つかれば、それを使います。
それが書き手の意図と合っているかどうかは、確かめません。

タロウくん：
だから、順番で決まってしまう。

専任講師：
Lean が保証するのは「MyMonoid Int のインスタンスである」ことまでです。

「 プログラマが求めていたインスタンスである」こと は、保証してくれない のです。

タロウくん：
分かりました。
だから、そもそも競合させない設計にするんですね？

専任講師：
そうです。
きちんと正しく判断できないものを、あえてLean 4に判断させない。これが賢い選択です。

AddMonoid と Monoid に分けておけば、AddMonoid.op と 書いた時点で候補は１つ です。

Lean 4 は、宣言の順序や優先度といった、書き手の意図とは無関係な規則で選ぶ ことになります。

その状況そのものを、作らずに済むのです。

タロウくん：
Haskell が最初から取っている道と、似ていますね。

専任講師：
たしかに、そうですね。
似ていると思います。

Haskell は、Sum と Product という 型 で分けました。
Mathlib はクラスの名前で分けています。

分ける場所が違うだけで、「区別する手段を用意する」という点は同じです。

タロウくん：
Haskell のほうは、選ぶ余地がなかったわけですね。

専任講師：
そこが違います。

Haskell では、型と型クラスの組に対して、インスタンスは１つしか存在できません。
分けなければ、そもそもコンパイルが通らないのです。

タロウくん：
Mathlib は、分けないこともできた。

専任講師：
できました。分けないと曖昧になると分かっていたから、分けているのです。

タロウくん：
Haskell は、そうするしかなかった。
Mathlib は、そうすることを選んだ。

専任講師：
そこが違いです。

---

Lean 4 は、どう探索しているのか

ここで、Lean 4 の仕組みをもう少し詳しく見ておきます。

先ほど「候補を順に試す」と述べました。

その手順は、こうなります。

1. 候補となるインスタンスを集める
2. 優先度、次に宣言順で並べる
3. その順に試す
4. 最初に成功したものを採用する

ここでいう「成功」と「失敗」は、書き手の意図とは関係ありません。

探しているクラスと型の組に、そのインスタンスが当てはまるかどうか。
それだけです。

MyMonoid Int を探しているとき、addMonoid も mulMonoid も MyMonoid Int のインスタンスです。どちらを試しても成功します。

では、失敗するのは、どういう場合でしょうか？

例として、条件付きのインスタンスがある場合について考えてみましょう。
「型 a が MyMonoid であるなら、List a も MyMonoid である」という宣言があったとします。

MyMonoid (List Bool) を探すとき、Lean 4 はこのインスタンスを試します。
そして、「Bool が MyMonoid であるか」を確かめに行きます。

Bool のインスタンスが見つかれば、成功です。
見つからなければ、失敗して次の候補へ移ります。

これが、成功する、失敗する、という事の意味です。

試した結果が失敗すれば、次の候補へ移るのです。
この後戻りを バックトラッキング と呼びます。

Lean 4 は、この探索を効率よく行うために、途中の結果を記録する仕組みを採用しています。

条件付きのインスタンスがあると、探索が入れ子になります。

「List a が MyMonoid か」を調べるために「a が MyMonoid か」を調べる。
そういう構造です。

このとき、同じ問いに何度も戻ってくることがあります。

「Int が MyMonoid か」を、別々の経路から何度も調べる。
あるいは、調べている途中で同じ問いに戻ってしまい、そこから抜け出せなくなる場合があります。

ここで、一度調べた結果を記録しておけば、２度目からは記録を見るだけで済みます。

同じ調査を繰り返さずに済み、堂々巡りにも陥りません。
この手法は、tabled resolution と呼ばれています。

優先度の指定

優先度 は、宣言時に指定 します。

instance (priority := 1000) addMonoid : MyMonoid Int where
  op   := fun a b => a + b
  unit := 0

数値が大きいほど、優先度が高くなります。
既定値は 1000 です。

候補が複数あっても、Lean はエラーを出しません。
順に試して、最初に成功したものを黙って採用します。

Haskell であれば、重複したインスタンス宣言はコンパイルエラーになります。

Lean では、そもそも重複という概念がありません。

この違い が、次に述べる代償につながります。

明示的に指定することもできます。

#eval @MyMonoid.op Int addMonoid 3 5   -- 8
#eval @MyMonoid.op Int mulMonoid 3 5   -- 15

@ を付けると、暗黙に解決される引数を、自分で書けるようになります。ここでは、どのインスタンスを使うかを指定しています。

代償

便利に見えますが、代償があります。

MyMonoid.op 3 5 と書いたとき、その意味が文脈によって変わります。

ファイルのどこに書いたか、どのインスタンスが先に登録されているかで、結果が $8$ にも $15$ にもなる。

Haskell のコヒーレンスは、この曖昧さを構造的に排除しています。

Mathlib はどうしているか

実際の Mathlib では、この問題に対処するため、演算ごとに別のクラスを用意しています。

class Add (α : Type u) where
  add : α → α → α

class Mul (α : Type u) where
  mul : α → α → α

そして、加法についての群は AddGroup、乗法についての群は Group と、名前で区別します。

同じ Monoid に２つのインスタンスを持たせるのではなく、AddMonoid と Monoid に分けているのです。

Haskell の Sum/Product が値を包むのに対し、Mathlib はクラスの名前を分ける。

アプローチは違いますが、どちらも「区別する手段が要る」という点は同じです。

さらに Mathlib には、to_additive という仕組みがあります。
乗法について定理を証明すると、加法版の定理を自動生成してくれるものです。

同じことを２回書かずに済ませる工夫 が、必要になっているわけです。

コヒーレンスを保つか、複数の構造を許すか。
どちらにも代償があります。

---

ここで分かったのは、複数の演算を１つの型に重ねようとする と、Haskell では区別のための型が必要になる、ということ でした。

次は、その演算が本当に結合的であることを、誰が保証するのかを見ます。

---

第４部 ── 障害２ 法則を検査できない

この部で分かること
Monoid が要求する結合律は、どこに書かれているのか。そして、それが守られていなくてもコンパイルが通る理由。Idris ではどう違うのか。

コヒーレンスの問題は、newtype で回避できました。

しかし、より根本的な問題があります。

Monoid は何を要求しているか

Monoid の定義を、もう一度見ます。

class Semigroup a => Monoid a where
  mempty :: a

インスタンスを書くときに実装が必要なのは、通常 mempty だけです。
mappend と mconcat には既定の実装があります。

演算 <> は、上位クラスである Semigroup から使えます。

そして、結合律も単位元の性質も、クラスのフィールドとしては要求されていません。

では、どこに書かれているか。

ドキュメントの文章として書かれています。

Haskell のドキュメントには、Semigroup のインスタンスが満たすべき条件として、結合律が記されています。

Monoid については、mempty が左右の単位元であることが記されています。

検査されない

問題は、これらが 検査されない ことです。

次のコードを書いてみます。

newtype Broken = Broken Int deriving (Show, Eq)

instance Semigroup Broken where
  Broken x <> Broken y = Broken (x - y)

instance Monoid Broken where
  mempty = Broken 0

newtype Broken = Broken Int は、Int に Broken という別名を与える宣言です。中身は Int ですが、型としては別物になります。

deriving (Show, Eq) は、表示と等値比較の実装を、コンパイラに自動生成させる指定です。後でテストに使います。

そして演算 <> を、引き算にしました。

引き算は結合律を満たしません。第２部で見たとおりです。

そして、単位元の性質も破れています。

mempty は Broken 0 と定義しました。したがって mempty <> Broken 3 は Broken 0 <> Broken 3 です。

そして演算は引き算なので、Broken (0 - 3)、つまり Broken (-3) になります。

単位元は、左から組み合わせても相手を変えないはずでした。
ここでは符号が変わっています。

それでも、このコードはコンパイルを通ります。

GHC は、結合律も単位元の性質も確かめません。

何が起きるか

foldMap のような関数は、結合律を前提として動きます。

計算の順序を自由に変えてよい、という前提です。
並列化のときは特にそうです。

その前提が崩れていても、コンパイラは警告しません。

実行して、答えが合わないという形で現れます。

しかも、順序を変えたときだけ現れるので、再現が難しいことがあります。

実際にどう対処しているか

Haskell のコミュニティでは、テストで確かめるという方法が取られています。

QuickCheck というライブラリが広く使われています。

これは、ランダムな値を大量に生成して、指定した性質が成り立つかを試すものです。

prop_assoc :: Broken -> Broken -> Broken -> Bool
prop_assoc x y z = (x <> y) <> z == x <> (y <> z)

この性質をテストすれば、反例が見つかります。

ただし、これは検査ではなく試験です。

すべての値について確かめたわけではありません。
たまたま反例が見つからなかっただけかもしれません。

発展 ── では、Haskell で法則を扱う方法は本当にないのか（クリックで展開）

「型クラスの宣言では要求できない」 と書きました。
この限定には理由があります。

Haskell でも、法則を型として扱う方法がないわけではないからです。

ここでは、代表的な３つの方法 を紹介します。

いずれも本記事の主題からは外れますが、正確を期すために記しておきます。

方法１ ── 等式を型として表現する

Data.Type.Equality という標準の仕組みがあります。

data a :~: b where
  Refl :: a :~: a

a :~: b は、「型 a と型 b が等しい」ことを表す型です。構成子は Refl の１つだけで、両辺が同じときにしか作れません。

これは、Agda や Lean の等式型と同じ発想です。

ただし、扱えるのは型どうしの等しさです。
「$a + b = b + a$」のような、値についての等式は直接書けません。

型レベルの自然数（GHC.TypeLits）と組み合わせれば、型レベルでの計算については等式を扱えます。
しかし、値についての法則を要求するには足りません。

方法２ ── ファントム型に証明を住まわせる

Matt Noonan が2018年に発表した Ghosts of Departed Proofs（GDP、去りし証明の亡霊）という設計手法があります。

論文の要旨には、こう記されています。

（原文引用）

sophisticated preconditions can be encoded in Haskell's type system with no run-time overhead, by using proofs that inhabit phantom type parameters attached to newtype wrappers

（筆者による日本語訳）

洗練された事前条件を、実行時のオーバーヘッドなしに Haskell の型システムへ符号化できる。newtype の包みに付けたファントム型引数に、証明を住まわせることによって。

出典
Matt Noonan, "Ghosts of Departed Proofs (Functional Pearl)", Haskell Symposium, 2018年

ファントム型（phantom type）とは、型の引数として現れるが、値としては使われない型のことです。

たとえば「並べ替え済みのリスト」という性質を、次のように表せます。

newtype SortedBy comp a = SortedBy [a]

comp は、どの比較関数で並べ替えたかを表します。実行時には何のデータも持ちません。このような、値としては使われない型引数を ファントム型引数 と呼びます。

ただし、この宣言だけでは何も保証されません。

構成子 SortedBy が外から使えるなら、SortedBy [3,1,2] のような、並んでいないリストも作れてしまいます。

GDP の要点は、構成子を隠すことにあります。

モジュールの外へ構成子を公開せず、並べ替えを実際に行う関数だけが値を作れるようにする。すると、この型の値を持っていること自体が、並べ替え済みであることの証拠になります。

module Sorted (SortedBy, sortBy, mergeBy) where

公開するのは型名と、値を作る手段となる関数だけです。構成子は書きません。

「証明を持つ関数だけが、その型の値を作れる」 ── これが、この手法の核心です。

論文は、この手法について次のように述べています。

（原文引用）

The "ghosts of departed proofs" approach to API design can achieve many of the benefits of dependent types and refinement types, yet only requires some minor and well-understood extensions to Haskell 2010.

（筆者による日本語訳）

API 設計に対する「去りし証明の亡霊」の手法は、依存型や篩型の利点の多くを達成できる。しかも、Haskell 2010 に対する、ささやかでよく理解された拡張しか必要としない。

出典
Matt Noonan, "Ghosts of Departed Proofs (Functional Pearl)", Haskell Symposium, 2018年

方法３ ── 篩型で検証する

LiquidHaskell という仕組みがあります。

型に述語を添えることで、値が満たすべき条件を書けます。

{-@ type Pos = {v:Int | v > 0} @-}

{-@ ... @-} という特別な注釈の中に、「０より大きい整数」という条件を書いています。

この条件は、SMT ソルバという外部の道具によって検証されます。

そして、代数の法則も書けます。

{-@ assocPlus :: x:Int -> y:Int -> z:Int
              -> { (x + y) + z == x + (y + z) } @-}

証明を、等式の連鎖として書き下すこともできます。

では、なぜ本記事は「できない」と述べるのか

３つとも、実際に使われている手法です。

しかし、いずれも「型クラスのインスタンス宣言に、法則の証明を要求する」ものではありません。

手法	何ができるか	型クラスとの関係
:~:	型どうしの等しさを扱う	別の仕組み
GDP	値が条件を満たすことを、包みで保証する	型クラスの外側
LiquidHaskell	述語を SMT ソルバで検証する	言語の外側の道具

Monoid のインスタンスを書くときに、結合律の証明を要求する ── これは、これらの手法をもってしても実現できません。

class Monoid a where mempty :: a という宣言に、法則を追加する場所がないからです。

そして本記事が扱っているのは、まさにその点です。

GDP や LiquidHaskell は、「法則を守る設計を、使う側が組み立てる」手法です。

「法則を守ることを、型クラスが要求する」仕組みではありません。

この違いを踏まえたうえで、以降をお読みください。

これは代数に限った話ではありません

同じ構図が、等値性にもあります。

第１部で見た Rust の Eq トレイトは、反射性を要求します。

しかしコンパイラは確かめません。

実装者が「成り立ちます」と宣言するだけ です。

約束の表明であって、証明の提出ではない。

Monoid の結合律も、まったく同じ立場にあります。

Ord の全順序性も、Functor の恒等則も、Monad の結合則も、すべて同じです。

Haskell の型クラスが要求する法則は、すべてドキュメントに書かれた約束です。

Idris では、法則を要求できます

Idris は、Haskell によく似た構文を持つ言語です。ただし依存型を備えています。

法則を要求するインターフェース を、次のように書くことができます。

interface Semigroup a => SemigroupV a where
  semigroupOpIsAssociative : (l, c, r : a) ->
    l <+> (c <+> r) = (l <+> c) <+> r

interface は、Haskell の class にあたる語です。

Semigroup a => は、Haskell と同じく「先に Semigroup を実装していること」を要求します。

そして中身が、Haskell とまったく違います。

semigroupOpIsAssociative : (l, c, r : a) ->
  l <+> (c <+> r) = (l <+> c) <+> r

これは、関数の型です。

(l, c, r : a) -> は、「型 a の値を３つ受け取る」という意味です。

そして返り値の型が l <+> (c <+> r) = (l <+> c) <+> r ── 等式そのものになっています。

等式が、型である

ここが要点です。

Idris では、命題が型です。
そして、その型の値を作ることが、命題を証明することにあたります。

したがって semigroupOpIsAssociative を実装するには、結合律を証明しなければなりません。

実際に書いてみる

自然数の足し算について、実装してみます。

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[PlusNatSemiV] SemigroupV Nat using PlusNatSemi where
  semigroupOpIsAssociative = plusAssociative

角括弧 [PlusNatSemi] は、実装に名前を付ける記法です。Idris 2 では、同じ型に複数の実装を書けるため、名前で区別します。

using PlusNatSemi は、「この Semigroup の実装を前提とする」という指定です。

そして最後の行で、plusAssociative という既存の証明を渡しています。これは標準ライブラリにある、自然数の足し算の結合律の証明です。

引き算で書こうとすると

先ほどの、引き算を登録する例です。

[MinusIntSemi] Semigroup Int where
  (<+>) x y = x - y

[MinusIntSemiV] SemigroupV Int using MinusIntSemi where
  semigroupOpIsAssociative = ?proof

?proof は「ここは未完成です」という印です。

Idris では、 穴（hole）と呼びます。

ここに入れるべき証明が、存在しません。
引き算は結合律を満たさないからです。

穴を残さない、完成したプログラムとしては書けません。

Haskell では通り、Idris では完成できない。

これは標準ライブラリではありません

一点、正確を期します。

この SemigroupV は、Idris の標準ライブラリにあるものではありません。

Idris 1 では contrib という追加パッケージに VerifiedSemigroup という名前で入っていました。

Idris 2 では、idris2-algebra という外部ライブラリが提供しています。

標準の Semigroup には、法則が含まれていません。
この点は Haskell と同じです。

なぜ標準にしないのか

Idris の設計者は、この問いに答えています。

（原文引用）

the language should make it possible to prove things about your programs, but mustn't require you to do so

（筆者による日本語訳）

言語は、プログラムについて証明することを可能にすべきである。しかし、そうすることを要求してはならない。

出典
Edwin Brady による設計方針の表明。Idris 2 Documentation および同氏の講演・議論において、繰り返し述べられているもの

証明を書きたい人は書ける。書きたくない人は書かなくてよい。

その選択を、標準ライブラリが奪うべきではない ── という判断です。

そして、より深い問題があります

法則付きのインターフェースを積み上げようとすると、別の障害に当たります。

idris2-algebra の作者は、次のように記しています。

（原文引用）

Idris will no longer be able to verify that the Monoid and SemigroupV our interface inherits from are using the same version of (<+>) (because Idris - unlike Haskell - has no such thing as typeclass coherence)

（筆者による日本語訳）

Idris は、我々のインターフェースが継承している Monoid と SemigroupV が、同じ版の <+> を使っていることを、もはや検証できない。（Idris には、Haskell と違って、型クラスのコヒーレンスというものが存在しないからである。）

出典
stefan-hoeck/idris2-algebra, GitHub、README

ここで、第３部の話が戻ってきます。

Idris は同じ型に複数の実装を許します。

すると SemigroupV が検証している <+> と、Monoid が使っている <+> が、別物である可能性が生じます。

法則を証明したのに、その証明が何についてのものか分からなくなる。

トレードオフ

整理します。

	Haskell	Idris
同じ型に複数の実装	書けない	書ける
法則を型で要求	できない	できる
法則付き階層の構築	──	困難

Haskell はコヒーレンスを保つ設計を取り、法則の表現は型クラスの外に置きました。

Idris は法則を型として表現できる設計を取り、コヒーレンスは持ちません。
その結果、法則付きの階層を積み上げることが難しくなっています。

両方を同時に得ることは、簡単ではありません。

なお idris2-algebra の作者は、法則付きインターフェースを、検証対象のインターフェースで添字づけるという方法を検討しています。

ただし、それを行うと型推論がほぼ効かなくなり、どの実装を使うかを毎回明示する必要が生じる、とも記しています。

ここまでを整理します

法則が、どこまで強制されるか。

体系	法則の在り処	強制されるか
Haskell	ドキュメントの文章	されない
Idris（標準）	ドキュメント	されない
Idris（外部ライブラリ）	型として表現可能	選んだ場合のみ
Lean / Mathlib	型クラスのフィールド	される

**Idris が中間にあります。**書きたい人は書ける。しかし、書かないこともできる。

この点で、Lean や Rocq がどうしているかを、第７部で見ます。

---

ここで分かったのは、法則が守られていることを、コンパイラが確かめてくれるわけではない、ということでした。

次は、そのことが階層の設計にどう跳ね返るかを見ます。

対話 ── 書かれていないのか、守られていないのか

ここで、２つの話を対話の形で確かめます。

---

タロウくん：
先生、結合律が検査されないという話ですが ── そもそも、どこかに書いてあるんですか。

専任講師：
Semigroup については、ドキュメントに書かれています。

タロウくん：
Num は。

専任講師：
現在のドキュメントには、結合律や分配律への言及があります。

ただし、Semigroup のように、「インスタンスが満たすべき条件」として明示された形ではありません。

タロウくん：
どう違うのですか？

専任講師：
書き方が違います。

原文を見てみましょう。

（原文引用）

The Haskell Report defines no laws for Num. However, (+) and (*) are customarily expected to define a ring and have the following properties:

（筆者による日本語訳）

Haskell Report は Num に対して法則を定めていない。
しかし (+) と (*) は、慣習的に環をなすことが期待されており、以下の性質を持つ。

出典
GHC.Num, base, Hackage

タロウくん：
「法則を定めていない」と書いてありますね。

専任講師：
そうなんです。

そのうえで、環の公理が項目ごとに列挙されている。

加法の結合律、加法の可換律、加法単位元、加法逆元、乗法の結合律、乗法単位元、分配律。

タロウくん：
書いてはあるんですね。

専任講師：
確かに、書いてあることは事実です。

しかし、「法則」として書かれているのではなく、「慣習的な期待」という位置づけです。

Semigroup のドキュメントは「Instances should satisfy the following」── インスタンスが満たすべき条件、という書き方です。

タロウくん：
規範の強さが違う。

専任講師：
そうです。

そこが違いです。

タロウくん：
そうすると、Num は、数学で明確に定義された 「環」 に対応するのでしょうか？

専任講師：
対応しません。

理由を２点挙げます。

１点目は、環の演算でないものが含まれていることです。

abs と signum です。

第１部で見たとおり、環 の定義には、これら２つは含まれていません。

タロウくん：
数学の 「環」 の定義には含まれていないものが、HaskellのNumというクラスには定義されてしまっているのですね。

専任講師：
そうなりますね。

このことが原因となり、実際に障害が発生します。

Haskell Prime の wiki には、次のように記されています。

（原文引用）

abs and signum don't make sense for Complex Integer (Gaussian integers), vectors, matrices, etc.

（筆者による日本語訳）

abs と signum は、ガウス整数、ベクトル、行列などに対して意味を持たない。

出典
numeric classes, Haskell Prime Wiki

タロウくん：
行列やガウス整数は、環 ではあるのに、Haskellの Num としては成立しない。

専任講師：
もしも、Numに含めようとすると、ガウス整数やベクトル、行列などは、意味のない実装を記述することになってしまいます。これはおかしい。

タロウくん：
２点目の理由は？

専任講師：
Num が、数学の構造から出発して設計されたものではないことです。

同じ wiki に、設計の意図が述べられています。

（原文引用）

The Haskell 98 numeric classes were designed to classify the operations supported by the Haskell 98 types, Integer, Int, Float, Double, Complex and Ratio. However they are not suitable for other mathematical objects.

（筆者による日本語訳）

Haskell 98 の数値クラスは、Haskell 98 が持つ型 ── Integer、Int、Float、Double、Complex、Ratio ── が備える操作を分類するために設計された。しかし、それ以外の数学的対象には適していない。

出典
numeric classes, Haskell Prime Wiki

タロウくん：
すでにある型から出発している。

専任講師：
代数構造から出発したのではありません。
そこが Semigroup との違いです。

タロウくん：
だから、絶対値 と 符号 が入っている。

専任講師：
実用主義で作られた定義なんです。

数学的な定義に対応させることが目的ではありませんでした。

タロウくん：
numeric-prelude のドキュメントには、何か書かれていますか？

専任講師：
かつて、次のような指摘がありました。

（原文引用）

The current Prelude defines no semantics for the fundamental operations. For instance, presumably addition should be associative (or come as close as feasible), but this is not mentioned anywhere.

（筆者による日本語訳）

現在の Prelude は、基本的な演算に対して意味論を定義していない。たとえば、加法は結合的であるべきだと思われるが、そのことはどこにも述べられていない。

出典
Numeric Prelude, HaskellWiki（本記事執筆時点の記述）

タロウくん：
「どこにも述べられていない」。

専任講師：
この指摘は、2018年より前の base のドキュメントについてのものです。

base-4.11 までの Num のドキュメントには、「Basic numeric class.」という一行しか書かれていませんでした。結合律も分配律も、どこにも記されていなかったのです。

タロウくん：
本当に、何も書かれていなかった。

専任講師：
そうなんです。

それが、base-4.12 ── 2018年にリリースされた GHC 8.6 に付属する版のドキュメント ── から、環の公理 が追加されました。

出典
GHC.Num, base-4.11.1.0 および GHC.Num, base-4.12.0.0, Hackage

タロウくん：
書かれるようになったのですね。

専任講師：
現在のドキュメントには、いま見たとおり環の性質が列挙されています。
ただし「慣習的に期待される」という位置づけです。

そして、守られているかどうかをコンパイラが検査することはありません。

タロウくん：
Semigroup と同じ立場ですね。

専任講師：
同じです。 書かれていることと、検査されることは別です。

タロウくん：
Semigroup のほうは、規範として書かれているのに。

専任講師：
Semigroup と Monoid は、代数構造を意識して設計されています。名前からして、そうですね。

Semigroup が base に入ったのは base-4.9.0.0、Monoid の上位クラスになったのは base-4.11.0.0 です。比較的新しい整理です。

Num は、Haskell の最初期からあります。目的が違うのです。

タロウくん：
目的が違う。

専任講師：
数値計算を書きやすくすることが目的でした。数学の構造に合わせることではありません。

タロウくん：
先ほどの numeric-prelude は、そのあと何をしたんですか？

専任講師：
公理を QuickCheck の性質として書き、テストで確かめる方式を取りました。

タロウくん：
第４部の話ですね。
テストであって、検査ではない。

専任講師：
そうです。
ただ、何を守るべきかが明示された という点では、前進です。

タロウくん：
書かれていないよりは、書かれているほうがいい。

専任講師：
そして、機械が読める形で書かれているほうがいい。
QuickCheck の性質は、少なくとも実行できます。

---

タロウくん：
先生、もう１つ聞いていいですか？

専任講師：
どうぞ。

タロウくん：
Double は Num のインスタンスですよね。
あれは、結合律を満たすんですか？

専任講師：
満たしません。

タロウくん：
えっ。

専任講師：
浮動小数点数の足し算は、結合的ではありません。

タロウくん：
足し算なのに。

専任講師：
計算のたびに、誤差が生じるからです。

どの順で足すかによって、誤差の積み重なり方が変わります。

タロウくん：
順番で答えが変わる。

専任講師：
極端な例を挙げます。

非常に大きな数と、非常に小さな数を足すと、小さいほうが消えてしまうことがあります。表現できる桁数に限りがあるためです。

タロウくん：
それが、順番によって起きたり起きなかったりする。

専任講師：
そういうことです。

タロウくん：
これは、Haskell の問題ですか。

専任講師：
いいえ。IEEE 754 という規格の性質なので、どの言語でも同じです。

そして、破れているのは結合律だけではありません。

タロウくん：
他にもあるんですか。

専任講師：
NaN があります。

ゼロをゼロで割ったときなどに現れる、「数でない値」です。

タロウくん：
それがどうしたんですか。

専任講師：
NaN は、自分自身と等しくありません。NaN == NaN が偽になります。

タロウくん：
えっ。等しさの、いちばん基本的な条件が破れている。

専任講師：
そうです。どんなものも自分自身とは等しい ── その条件を満たしません。

タロウくん：
足し算だけでなく、等値比較まで。

専任講師：
浮動小数点数を、そのまま代数の階層に収めることが難しい理由です。

タロウくん：
じゃあ、仕方がない。

専任講師：
仕方がないのですが、そのことが型に現れていないのが問題です。

タロウくん：
Double も Integer も、同じ Num に属している。

専任講師：
Haskell Prime という、言語仕様の改訂を議論する場のwikiには、こう記されています。

（原文引用）

Note that the Float and Double instances will not satisfy the usual axioms for these structures.

（筆者による日本語訳）

Float と Double のインスタンスは、これらの構造についての通常の公理を満たさないことに注意せよ。

出典
numeric classes, Haskell Prime Wiki

タロウくん：
公式に認められている、と。

専任講師：
認識はされています。しかし、型では区別されていません。

タロウくん：
先生、これは第４部の話とは、少し違いますね。

専任講師：
違います。よく気づかれました。

第４部で見たのは、実装者が法則を破りうるという話でした。

タロウくん：
今回は。

専任講師：
標準ライブラリ自身が、法則を破っているという話です。

タロウくん：
Double は base に入っている。

専任講師：
入っています。そして Num のインスタンスです。

タロウくん：
法則を書いていないから、破っていることにもならない。

専任講師：
形式的にはそうなります。
Num は法則を要求していないので、Double は何も違反していません。

タロウくん：
なんだか、うまくできていますね。

専任講師：
逆に言えば、法則を書けば Double が入れなくなるわけです。

タロウくん：
だから書かなかった。

専任講師：
そこまで断定はできません。
ただ、法則を明示することと、Double を同じ階層に置くことは、両立しにくい。

タロウくん：
Lean ではどうなっているんですか。

専任講師：
Mathlib の Field に、浮動小数点数は入っていません。

タロウくん：
入れられない。

専任講師：
公理を証明できないからです。

タロウくん：
なるほど。証明を要求すると、入れられないものが出てくる。

専任講師：
そして、それは正しい振る舞いです。
浮動小数点数は体ではないのですから。

タロウくん：
Haskell は、入れてしまっている。

専任講師：
実用のために、そうしています。

どちらが良いという話ではありません。

何を保証したいかによって、適切な設計が変わるのです。

---

第５部 ── 障害３ 階層の設計が一意でない

この部で分かること
法則を書けないことが、なぜ階層の設計を難しくするのか。そして、numeric-prelude が Num を３つに分割した理由。

３つ目の問題は、設計そのものにあります。

なぜ、法則を書けないと階層が難しくなるのか

冒頭で「演算が満たすべき法則を表現できないことが、代数構造の階層を設計するうえでの障害になっている」と述べました。

その理由を、先に説明します。

代数構造は、法則によって定義されているからです。

第２部を思い出してください。半群、モノイド、群 ── これらの違いは、演算の数ではありませんでした。どの法則を満たすかでした。

構造	演算	違いは何か
半群	１つ	結合律を満たす
モノイド	１つ	＋単位元がある
群	１つ	＋逆元がある

演算の型は、３つとも同じです。a -> a -> a です。

つまり、法則を型クラスのフィールドから取り除くと、この３つを「公理を満たす構造」として区別する根拠が失われます。

残る区別は、mempty や inverse といった操作が宣言されているかどうかだけです。
しかし、それらが本当に単位元や逆元として振る舞うことは、型からは分かりません。

法則がないと、階層はどうなるか

Semigroup と Monoid の違いは、Haskell では mempty があるかどうかだけになります。

Group を作るとしても、inverse :: a -> a というメソッドを足すだけです。

そのメソッドが、本当に逆元を返すかどうかは問われません。

すると、次のことが起きます。

第１に、階層に意味がなくなります。

「この型は群である」と宣言できても、群の性質を使う根拠になりません。

第２に、どこで分けるかの根拠が失われます。

法則があれば、「この法則を追加したから、新しいクラスを作る」という基準ができます。

法則がなければ、基準はメソッドの有無だけです。
そして、どのメソッドをどのクラスに置くかは、設計者の判断に委ねられます。

第３に、正しさを確かめる手段がありません。

ある階層の設計が妥当かどうかは、コンパイラは判定してくれません。

実際に使ってみて、不便かどうかで判断することになります。

だから、複数の設計が並立します

以下では、その帰結を見ていきます。

どこで枝分かれさせるか

第２部で見た代数構造の並びを、そのまま型クラスにすることを考えます。

Semigroup → Monoid → Group → Ring → Field

一見、この順に素直に積み上がりそうに見えます。

しかし、実際には枝分かれが生じます。

たとえば、可換性をどこで入れるか。

• 可換モノイドは、モノイドの部分クラスか
• 可換群は、群の部分クラスか
• 可換環は、環の部分クラスか

すべてを部分クラスとして用意すると、クラスの数が急増します。

加法と乗法の扱い

より深刻な問題があります。

環には、演算が２つありました。足し算と掛け算です。

そして、足し算について可換群、掛け算についてモノイドをなします。

この「２つの構造を持つ」ことを、型クラスでどう表現するか。

方法が複数あります。

方法１ ── 演算ごとに別のクラスを作る

AdditiveGroup、MultiplicativeMonoid のように、演算を名前に含めます。

algebra というライブラリが、この方針を取っています。

方法２ ── 環を１つのクラスにまとめる

Ring というクラスに、+ と * の両方を含めます。

numeric-prelude が、この方針に近い形です。

方法３ ── newtype で包む

base の Sum/Product の方式です。

**どれが正しいということはありません。**それぞれ利点と欠点があります。

実際の階層を比べる

numeric-prelude のドキュメントには、既存の型クラスをどう置き換えるかが示されています。

（原文引用）

Num --> Additive, Ring, Absolute
Integral --> ToInteger, IntegralDomain, RealIntegral
Fractional --> Field
Floating --> Algebraic, Transcendental

（筆者による日本語訳）

Num は Additive、Ring、Absolute へ
Integral は ToInteger、IntegralDomain、RealIntegral へ
Fractional は Field へ
Floating は Algebraic、Transcendental へ

出典
Numeric Prelude, HaskellWiki

Num １つが、３つに分割されています。

これが、第１部で見た「詰め込みすぎ」への対処です。

Additive が足し算、Ring が掛け算を含む環、Absolute が絶対値と符号にあたります。

なぜ細かく分けるのか

同ライブラリのドキュメントには、具体例が挙げられています。

（原文引用）

Consider the data type data IntegerFunction a = IF (a -> Integer). One can reasonably define all the methods of Algebra.Ring.C for IntegerFunction a (satisfying good semantics), but it is impossible to define non-bottom instances of Eq and Show.

（筆者による日本語訳）

データ型 data IntegerFunction a = IF (a -> Integer) を考えてみよ。IntegerFunction a について、Algebra.Ring.C のすべてのメソッドを、良い意味論を満たす形で定義できる。しかし Eq と Show の、まともなインスタンスを定義することは不可能である。

出典
Numeric Prelude, HaskellWiki

「整数を返す関数」という型を考えると、これは環をなします。関数どうしを足したり掛けたりできるからです。

しかし、２つの関数が等しいかどうかを判定することはできません。
すべての入力について確かめる必要があるからです。

かつての Haskell では、Eq と Show が Num の上位クラスでした。
つまり Num に属するには、等値判定と文字列化ができなければならなかった。

この型は、環でありながら Num になれませんでした。

なお、この上位クラス関係は2012年のGHC 7.4で解消されています。
ライブラリの問題意識が、標準の側にも反映された形です。

階層の設計は、Lean でも問題だった

これは Haskell 固有の問題ではありません。

Lean の Mathlib でも、代数構造の階層をどう設計するかは長く議論されてきました。

Rocq の Mathematical Components ライブラリも、同じ問題に取り組んでいます。

構造が増えるほど、その組み合わせが爆発的に増えます。

可換性、有限性、順序、位相 ── これらを掛け合わせると、クラスの数が手に負えなくなります。

Mathlib では、extends による継承を基本としつつ、性質ごとの小さなクラスを併用する設計が採られています。

たとえば「左簡約律を満たす乗法」を表す IsLeftCancelMul のようなクラスがあり、必要なものだけを組み合わせられるようになっています。

Rocq の Mathematical Components では、混合（mixin）と呼ばれる仕組みが、より徹底した形で使われています。

**型クラスによる代数構造の階層化は、どの体系でも難問である。**この点は共通しています。

---

ここまでで、３つの障害が出揃いました。

次は、外部のライブラリがこれらにどう対処したかを見ます。

第６部 ── 外部ライブラリはどうしたか

base に代数構造がない以上、必要な人は外部のライブラリを使います。

複数あり、それぞれ設計方針が異なります。

主なライブラリ

ライブラリ	内容
algebra（Edward Kmett）	半群から加群、代数まで階層化
numeric-prelude	Num を置き換える代数階層
constructive-algebra	構成的代数
linear	ベクトル空間、行列
hmatrix	BLAS/LAPACK を利用した数値線形代数
algebraic-structures	マグマから群、環、加群、代数まで

algebra ── 演算ごとに分ける方式

Edward Kmett による algebra は、演算の名前をクラス名に含めます。

階層の一部を示します。

class Additive a where
  (+) :: a -> a -> a

class Additive a => Monoidal a where
  zero :: a

class Monoidal a => Group a where
  negate :: a -> a

第２部で見た階層と、対応しています。

Additive が半群、Monoidal がモノイド、Group が群にあたります。

そして、加法と乗法で別のクラスを用意しています。Multiplicative、MultiplicativeMonoid といった具合です。

利点 ── 整数の加法構造と乗法構造を、newtype なしで両方持てます。

欠点 ── クラスの数が多く、階層の全体像を把握しにくくなります。

そして、法則は要求されません。

ある研究論文は、この点を次のように述べています。

（原文引用）

Note that, none of these requires the "proof" of algebraic axioms. Hence, one can accidentally write a non-associative Additive-instance, or non-distributive Ring-instance.

（筆者による日本語訳）

これらのいずれも、代数的公理の「証明」を要求しないことに注意せよ。したがって、結合的でない Additive のインスタンスや、分配的でない Ring のインスタンスを、うっかり書いてしまうことがありうる。

出典
石井大海, "A Purely Functional Computer Algebra System Embedded in Haskell", arXiv:1807.01456, 2018年

階層を細かく分けても、第４部の問題は残ります。

numeric-prelude ── 標準を置き換える方式

Num の階層そのものを設計し直したものです。

第５部で見たとおり、Num を Additive、Ring、Absolute に分割します。

利点 ── 数学的な階層に忠実です。

欠点 ── 標準の Prelude を隠す必要があり、既存のコードとの併用が面倒になります。

algebraic-structures ── マグマから始める方式

HLinear という線形代数ライブラリのために作られたものです。

論文には、次の記述があります。

（原文引用）

The new package algebraic-structures provides classes for algebraic structures ranging from magmas, groups, and actions, to rings, modules, and algebras. For example, magmas are sets together with a binary operator; no further conditions are imposed.

（筆者による日本語訳）

新しいパッケージ algebraic-structures は、マグマ、群、作用から、環、加群、代数に至る代数構造のクラスを提供する。たとえばマグマは、集合と二項演算の組であり、それ以上の条件は課されない。

出典
A. Ghitza, M. Raum, "HLinear: Exact Dense Linear Algebra in Haskell", arXiv:1605.02532, 2016年、§2.1

マグマ（magma）とは、演算を１つ持つだけで、結合律すら要求しない構造です。

第２部の表でいえば、半群のさらに下にあたります。

構造	要求する法則
マグマ	なし
半群	結合律
モノイド	＋単位元
群	＋逆元

**「２つのものから１つのものを作る規則がある」**というだけの構造です。

なお、引用文中の 加群（module）と 代数（algebra）は、環の上に作られるより複雑な構造です。本記事では踏み込みません。

作用（action）は、ある構造が別の集合に働きかける仕組みのことです。回転が平面上の点を動かす、といった状況を表します。

class MultiplicativeMagma a where
 (*) :: a -> a -> a

なぜ、そこから始めるのか。

結合律を満たさない演算も、実際には存在するからです。たとえば減算や、ある種の平均をとる演算です。

階層の底を低く取れば、それらも扱えます。

法則をどう扱っているか

同じ論文には、法則への対処も記されています。

（原文引用）

There is no general way to establish that such axioms are valid for a given Haskell function. For this reason, the package algebraic-structures provides Tasty-combinators to test that implementations respect relevant mathematical axioms.

（筆者による日本語訳）

ある Haskell の関数について、そうした公理が成り立つことを確かめる一般的な方法は存在しない。そのため algebraic-structures パッケージは、実装が関連する数学的公理を尊重しているかを試験するための Tasty コンビネータを提供している。

出典
A. Ghitza, M. Raum, "HLinear: Exact Dense Linear Algebra in Haskell", arXiv:1605.02532, 2016年、§2.1

「一般的な方法は存在しない」 と明言されています。

Tasty は、Haskell のテスト用の枠組みです。

つまり、この問題への対処は テストによる試験 であり、コンパイル時の検査ではありません 。

第４部で見た QuickCheck の話と同じ構図 です。

ライブラリを選ぶときに見る点

以上を踏まえると、次の観点で比較できます。

観点	問い
階層の底	マグマからか、半群からか、モノイドからか
演算の扱い	演算ごとにクラスを分けるか、まとめるか
標準との関係	Prelude を置き換えるか、共存するか
法則の扱い	ドキュメントに書くだけか、QuickCheck の性質を用意するか
数値計算との接続	抽象構造だけか、実際の行列計算まで扱うか

「どれが正しいか」ではなく、「何をしたいか」で選ぶことになります。

外部ライブラリでも残る制約

ここで、確認しておくべきことがあります。

第３部と第４部で見た障害は、これらのライブラリを使っても完全には取り除けません。

ただし、影響を緩和することはできます。

newtype による包み、明示的な辞書の受け渡し、QuickCheck や Hedgehog による試験、LiquidHaskell のような外部の検証器
── 用途に応じて、これらを組み合わせることになります。

コヒーレンスの制約は、言語の仕様です。

algebra が演算ごとにクラスを分けているのは、その制約の下で工夫した結果であって、制約を取り払ったわけではありません。

法則についても同じです。

少なくとも本記事で取り上げた主要な Haskell 代数ライブラリでは、法則そのものを型検査器に証明させる仕組みにはなっていません。

先ほど引用したとおり、algebra について「代数的公理の証明を要求しない」ことが指摘されています。

algebraic-structures については、作者自身が「公理が成り立つことを確かめる一般的な方法は存在しない」と述べ、テストによる試験を提供しています。

ライブラリの選択によって変えられるのは、主に第５部の問題です。

階層の設計は、ライブラリの側で選び直せます。

残る２つは、通常の型クラス機構そのものに由来します。

対話 ── 関数を、ベクトルとして扱えるか

ここまで、代数構造を中心に見てきました。

では、他の分野ではどうか。

別の題材で、同じ問題が現れるかを確かめます。

---

タロウくん：
先生、少し違う話をしてもいいですか。

専任講師：
どうぞ。

タロウくん：
関数解析という分野では、関数をベクトル空間の中のベクトルとして扱えると兄から聞きました。

専任講師：
扱えます。関数を足したり、定数倍したりできますから。

タロウくん：
これも、Haskell のライブラリを使えば型として宣言できますか。

専任講師：
よい問いです。そして、実際にライブラリがあります。

タロウくん：
あるんですか。

専任講師：
vector-space というライブラリです。実際のソースを見てみましょう。

Data.VectorSpace のソース

タロウくん：
本当に読めるんですね。

専任講師：
ページの中ほどに、こういう記述があります。

instance VectorSpace v => VectorSpace (a -> v) where
  type Scalar (a -> v) = a -> Scalar v
  (*^) = liftA2 (*^)

タロウくん：
本当に書いてある……

専任講師：
a -> v というのは、「a を受け取って v を返す関数」です。それがベクトル空間である、と宣言しています。

タロウくん：
関数型そのものを、ベクトル空間として扱っている。

専任講師：
しています。しかし、ここからが本題です。

タロウくん：
何かあるんですか。

専任講師：
同じソースファイルに、コメントアウトされた別の定義が残っています。

-- instance VectorSpace v => VectorSpace (a -> v) where
--   type Scalar (a -> v) = Scalar v
--   (*^) s = fmap (s *^)

タロウくん：
似ていますが、２行目が違いますね。

専任講師：
そこが要点です。

スカラー ── 定数倍する数 ── を、何と取るか。
上の版は「a を受け取ってスカラーを返す関数」、下の版は「ただのスカラー」です。

タロウくん：
どちらも書けるんですか。

専任講師：
どちらも VectorSpace のインスタンスとして設計することはできます。
しかし、スカラーをどの型にするかが異なります。

タロウくん：
同じ「関数をベクトルとして扱う」でも、形が変わる。

専任講師：
型クラスの設計によって、表現する構造が変わり得るのです。

タロウくん：
第５部の話ですね。設計が一意でない。

専任講師：
そのとおりです。作者は片方を選び、もう片方をコメントとして残しました。

タロウくん：
選ばなければならなかった。

専任講師：
選ばなければ、書けません。

名前と、数学的な定義

専任講師：
ここで、正確を期しておきます。

タロウくん：
何かありますか。

専任講師：
数学でいうベクトル空間は、体の上に作られます。第２部で見た、割り算ができる構造です。

タロウくん：
はい。

専任講師：
しかし、採用されている版がスカラーとして選んでいる a -> Scalar v は、一般には体ではありません。

タロウくん：
えっ。

専任講師：
定義域に少なくとも２つの点があれば、値を取る場所が重ならない２つの非零関数を作れます。その積は零関数になります。

タロウくん：
どちらも、全体としては $0$ ではないのに。

専任講師：
掛け合わせると、全体で $0$ になる。

タロウくん：
ゼロでないもの同士を掛けて、ゼロになる。

専任講師：
体では、そういうことは起きません。これは、体ではないということです。

タロウくん：
では、あの VectorSpace は何なんですか。

専任講師：
数学の言葉でいえば、関数環の上の加群として読むほうが自然です。ベクトル空間より広い概念です。

タロウくん：
VectorSpace という名前なのに。

専任講師：
ライブラリの型クラス名と、数学での用語が完全に一致するとは限りません。

タロウくん：
第１部の Num と同じ話ですね。

専任講師：
まったく同じ構図です。名前は、意図を伝えるためのものです。数学的な定義と一致することを、型が保証しているわけではありません。

内積について

タロウくん：
先生、もう１つ気になることがあります。

専任講師：
どうぞ。

タロウくん：
関数解析では、内積というものが出てくると聞きました。

専任講師：
ベクトルどうしを掛けて、数を返す演算ですね。角度や長さを測るために使います。

タロウくん：
それも、宣言できるんですか。

専任講師：
「内積を持つ」という構造そのものは、型クラスとして表せます。
このライブラリにも InnerSpace というクラスがあります。

タロウくん：
では、関数についても。

専任講師：
同じソースに、こういう注記があります。

-- No 'InnerSpace' instance for @a -> v@.

タロウくん：
「関数については、内積のインスタンスはない」。

専任講師：
コメントアウトされた版のほうには、そう書かれています。

タロウくん：
なぜですか。

専任講師：
理由が２つあります。

タロウくん：
２つ。

専任講師：
１つ目は、定義が一意に決まらないことです。

関数空間では、代表的な内積の１つとして、実数値関数に対する次のような形があります。

$$\langle f, g \rangle = \int f(x)g(x),dx$$

タロウくん：
積分ですか。

専任講師：
２つの関数を掛けて、全体にわたって足し合わせる。

ただし、これは１つの例にすぎません。複素数を扱う場合は共役を取りますし、どの範囲で、どういう重みで積分するかによっても変わります。

タロウくん：
「関数の型」だけでは、どれを採るか決まらない。

専任講師：
そうです。そして２つ目の理由が、より直接的です。

タロウくん：
何ですか。

専任講師：
型が合わないのです。

タロウくん：
型が。

専任講師：
採用されている版では、スカラーが a -> Scalar v でした。

したがって、内積の返り値も a -> Scalar v でなければなりません。

タロウくん：
関数を返す。

専任講師：
しかし、積分で定める内積が返すのは Scalar v ── ただ１つの数です。

-- この VectorSpace が要求する内積の返り値
a -> Scalar v

-- 積分による内積が返すもの
Scalar v

タロウくん：
噛み合わない。

専任講師：
スカラーの取り方を決めた時点で、内積の形も縛られてしまう。

タロウくん：
だから、コメントアウトされた版のほうに注記があったんですね。

専任講師：
そちらはスカラーを Scalar v と取っています。積分による内積とは型が合う。

**それでも「インスタンスはない」と書かれている。**定義が一意に決まらないからです。

タロウくん：
設計の選択が、次の設計を縛る。

専任講師：
そこが要点です。

さらに深い問題

専任講師：
そして、関数解析にはもう１段階あります。

タロウくん：
まだあるんですか。

専任講師：
完備性という条件です。

タロウくん：
完備。

専任講師：
有理数の列を考えます。$1, 1.4, 1.41, 1.414, \ldots$

**項どうしの差が、どんどん小さくなっていきます。**進むほど、互いに近づく。

このような列を コーシー列 と呼びます。

タロウくん：
どこかに落ち着きそうですね。

専任講師：
そう見えます。しかし、その落ち着き先は有理数ではありません。

タロウくん：
$\sqrt{2}$ ですか。

専任講師：
そうです。行き先が、有理数の外にあるのです。

タロウくん：
それを埋めたのが実数、ということですか。

専任講師：
そういう関係です。そして関数の空間でも、同じことを問います。

ベクトルの大きさを測る仕組みを ノルム と呼びます。

それを持ち、かつ完備な空間を バナッハ空間 と呼びます。

そして、内積を持つベクトル空間を 内積空間 と呼びます。

その内積から定まるノルムについて完備な内積空間が、ヒルベルト空間 です。

なお、ヒルベルト空間を論じるときは、通常は実数体または複素数体をスカラーとする内積空間を考えます。先ほど見た、関数をスカラーに取る版とは前提が異なります。

タロウくん：
それは、型で表せますか。

専任講師：
少なくとも、通常の Haskell の型クラス宣言だけでは表せません。

タロウくん：
なぜですか。

専任講師：
完備性は、空間全体についての性質だからです。

個々の値の性質でも、演算の法則でもない。

タロウくん：
「この関数が」という話ではない。

専任講師：
「この空間の中で、コーシー列には必ず行き先がある」── そういう主張です。

すべての列について語る必要があります。

タロウくん：
第４部の話に似ていますね。
すべての値について成り立つかどうか。

専任講師：
似ています。そして、より扱いにくい。

整理すると

専任講師：
関数解析の構造を、層に分けて考えてみましょう。

層	内容	通常の Haskell の型クラスで扱えるか
ベクトル空間／加群の演算	足し算、スカラー倍	クラスとして宣言できる
演算が満たす法則	分配律、結合律など	法則そのものは要求できない
内積	内積を持つという構造	クラスとしては表せるが、型だけでは定義が一意に決まらない
完備性	コーシー列の行き先	通常の型クラスでは表せない

タロウくん：
表の上にあるものほど、型クラスに書きやすい。

専任講師：
そうです。

表の下へ進むほど、法則、追加の構造、空間全体の性質が加わり、通常の型クラスだけでは表現しにくくなります。

タロウくん：
思っていたより、扱える部分が多かったですね。

専任講師：
演算については、そうです。

演算を宣言することは、確かにできました。ライブラリも実在します。

しかし、数学的構造が深くなるほど、「演算を持っている」だけでは足りなくなります。

法則、追加の構造、そして空間全体の性質。

「何を型として表すのか」だけでなく、「何を型によって保証したいのか」まで考えなければならないのです。

出典

• Data.VectorSpace ソース, Hackage
• conal/vector-space, GitHub（開発元のリポジトリ。ソースは src/Data/VectorSpace.hs）

本節で引いた２つの VectorSpace (a -> v) の定義、および a -> v に対する InnerSpace インスタンスが提供されていない旨の注記は、いずれも上記ソースの該当箇所によります。

ライブラリの作者は Conal Elliott 氏です。

他の言語では、どうなのか

タロウくん：
先生、他の言語では、完備性を型として書けるのですか。

専任講師：
書ける体系があります。

実際に、Lean 4 の数学ライブラリ Mathlib には、完備性を表す型クラスがあります。

[RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]

タロウくん：
４つ並んでいますね。

専任講師：
そこが要点です。

Mathlib では、ヒルベルト空間の本体を単一の基本型クラスとして定義するのではなく、NormedAddCommGroup、InnerProductSpace、CompleteSpace などの型クラスを組み合わせて表します。

タロウくん：
CompleteSpace E というのが、完備性ですか。

専任講師：
そうです。

Lean と Mathlib では、空間 E が完備であることを、CompleteSpace E という型クラスの前提として扱えます。

そして、その前提を受け取った定理は、完備性を必要とする議論にだけ適用できます。

タロウくん：
Haskell の型クラスでは書けなかったものが、Lean の型クラスでは前提として書けている。

専任講師：
そこが違いです。

主な体系での状況

専任講師：
関数解析の構造を、各体系がどう扱っているか。簡潔に整理します。

体系	内積・完備性を形式化できるか	主な表現
Haskell	内積構造の API は表せる。通常の型クラスだけでは、完備性の数学的保証はできない	vector-space の VectorSpace と InnerSpace
Lean 4 / Mathlib	できる	InnerProductSpace と CompleteSpace を型クラスの前提として組み合わせる
Isabelle/HOL	できる	chilbert_space を、型クラス階層の一部として定義する
Rocq	できる	ライブラリごとに、レコード・型クラス・命題を組み合わせて表す

タロウくん：
Isabelle は依存型を持たないと、先ほど伺いました。それでも書けるんですか。

専任講師：
別の方法で書いています。

Isabelle/HOL では、型クラス階層を使って、「この型は完備なノルム空間である」といった性質を型へ付与します。

タロウくん：
Lean とは、やり方が違う。

専任講師：
違います。

Lean では、型クラスの仕組みによって、空間そのものに関する性質を型クラスの前提として表現できます。

さらに Lean は依存型を備えるため、型に加えて値へ依存する命題も、型として表現し、その証明をプログラムの一部として扱えます。

Isabelle/HOL の方法は、値に依存する型で性質を表す方法とは異なります。しかし、型そのものに属する構造と公理を階層化するには、十分に強力です。

タロウくん：
どちらが優れている、という話ではない。

専任講師：
**設計の方針が違うだけです。**どちらも、関数解析の主要な部分を形式化しています。

実際に証明されているもの

タロウくん：
それで、何が証明されているんですか。

専任講師：
Mathlib には、関数解析の主要な定理が収められています。

ハーン・バナッハの定理、バナッハ・シュタインハウスの定理、開写像定理。ヒルベルト空間については、コーシー・シュワルツの不等式、直交射影、リース・フレシェの表現定理、ラックス・ミルグラムの定理。

タロウくん：
名前だけ聞いても分かりませんが、多そうですね。

専任講師：
バナッハ空間とヒルベルト空間に関する、大学院初年度相当の主要定理の多くが形式化されています。

タロウくん：
他の体系では。

専任講師：
Isabelle にも、複素ヒルベルト空間と有界作用素の理論が形式化されています。ユニタリ作用素、射影、随伴作用素などが含まれます。

Rocq では、MathComp-Analysis をはじめとするライブラリ群が、ノルム空間、位相、測度論、積分などの基盤を形式化しています。

個別の関数解析の定理がどこまで利用できるかは、採用するライブラリと版によって変わります。

タロウくん：
Haskell では、これらは。

専任講師：
通常の Haskell の型システムには、定理を命題として型に表し、その証明を型検査によって検証するための仕組みがありません。

vector-space にあるのは、主として演算を表すためのクラスです。

ハーン・バナッハの定理のような命題を型として表し、その証明を値として構成する ── 定理証明系で中心的なこの仕組みは、通常の Haskell の型システムにはありません。

タロウくん：
演算は書けるが、定理は書けない。

専任講師：
そこが、本記事を通じて見てきた区別です。

出典

• Mathlib.Analysis.InnerProductSpace.Defs, Mathlib
• Mathematics in mathlib, Lean Community（形式化済みの定理の一覧）
• D. Unruh 他, "Complex Bounded Operators in Isabelle/HOL", arXiv（2025年のプレプリント）
• M. I. de Frutos-Fernández, "Formalizing Norm Extensions and Applications to Number Theory", arXiv:2306.17234（各体系の形式化状況の比較）

なお、Rocq における個別の定理の形式化状況については、採用するライブラリの公式ドキュメントをご確認ください。

---

第７部 ── Lean の Mathlib と比べる

この部で分かること
Mathlib の Group が、群の公理を証明として要求する仕組み。そして、Idris が直面した困難を、Lean がどう避けているか。

ここまで見てきた３つの障害のうち、２つ目 ── 法則を検査できないこと ── は、Haskell に限った話ではありません。

Rust も同じです。前回の記事で見たとおりです。

しかし、そうでない体系があります。

Mathlib の Group

Lean 4 の数学ライブラリ Mathlib には、Group という型クラスがあります。

その定義は、おおよそ次の形をしています。

class Group (G : Type u) extends DivInvMonoid G where
  protected inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1

extends DivInvMonoid G は、「DivInvMonoid を継承する」という指定です。役割としては Haskell の => にあたりますが、仕組みは異なります。

Haskell の => は「先に Semigroup のインスタンスが存在すること」を要求する制約です。Lean の extends は、親の構造のフィールドを、そのまま自分のフィールドとして取り込みます。

DivInvMonoid は、乗法と逆元と除法を持つモノイドです。つまり Group は、その上に条件を１つ加えたものとして定義されています。

注目していただきたいのは、その下の行です。

protected inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1

これは フィールド です。つまり、Group のインスタンスを作るときに、値として提供しなければならないものです。

内容は「すべての a について、a の逆元と a を掛けると単位元になる」という主張です。

主張が、値として要求される

Lean では、命題が型です。そして、その型の値を作ることが、証明を書くことにあたります。

したがって inv_mul_cancel というフィールドに値を入れるには、その主張を証明しなければなりません。

instance : Group MyType where
  -- DivInvMonoid から継承されたフィールド（乗法、単位元、逆元など）
  mul := ...
  one := ...
  inv := ...
  -- 以下、それらが満たすべき性質
  mul_assoc := by ...
  one_mul   := by ...
  mul_one   := by ...
  inv_mul_cancel := by
    intro a
    -- ここに証明を書く

演算だけでなく、それらが満たすべき性質のすべてに、証明を与える必要があります。

証明が書けなければ、インスタンスは作れません。

嘘の宣言はできません。

なお、実際の Mathlib では、既存の構造から作る補助関数が多数用意されているため、すべてを手で書くことは稀です。しかし、どこかで誰かが証明していることに変わりはありません。

対比

Haskell と Lean で、何が違うのか。

	Haskell の Monoid	Lean の Group
演算	クラスのメソッドとして要求	同じく要求
法則	ドキュメントの文章	クラスのフィールド
検査	されない	される
嘘の実装	コンパイルが通る	通らない

約束の表明と、証明の提出。

前回の記事で、Rust の Eq と Lean の LawfulBEq を対比したときと、同じ構図です。

Lean は、第４部の問題をどう避けているか

第４部で、Idris の困難を見ました。コヒーレンスがないため、法則付きのインターフェースが「どの実装を検証しているのか」を追えなくなる、という問題です。

Lean も、同じ型に複数のインスタンスを許します。

では、なぜ同じ問題が起きないのか。

演算と法則を、分けていないからです。

Idris の設計では、Semigroup（演算だけ）と SemigroupV（法則だけ）が別のインターフェースでした。

だから両者が食い違う余地が生まれます。

Mathlib の Group は、そうなっていません。
演算も法則も、同じクラスのフィールドとして持ちます。

class Semigroup (G : Type u) extends Mul G where
  protected mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

Mul G を継承し、その * についての結合律を、同じクラスの中で要求しています。

食い違う余地がありません。mul_assoc が語っている * は、このクラスが継承した Mul の * そのものだからです。

法則を後付けにせず、最初から組み込む。

これが Lean の方針です。

なぜ Haskell はそうしなかったのか

Haskell の型クラスには、法則を書く場所がないからです。

Haskellの型システム では、「すべての a について $a + 0 = a$」という主張を、型クラスのフィールドとして要求できません。値に依存する型を扱えないためです。

これは設計の怠慢ではなく、型システムの表現力の問題です。

では、Lean のほうが優れているのか

そうとは限りません。

証明を書く負担があります。

Haskell で Monoid のインスタンスを書くのは、数行で済みます。

Lean で Group のインスタンスを書くには、公理をすべて証明する必要があります。

そして、Mathlib でも階層の設計は難問のままです。

第５部で述べたとおり、構造の組み合わせが増える問題は、証明ができるからといって消えません。

保証の強さと、書く負担。

この２つ は 交換関係 にあります。

用途によって、どちらを取るかが変わる のです。

---

第８部 ── 逆行列を持つことは、型で表せるか

ここまでの話は、演算と法則についてでした。

第３部では、１つの型に複数の構造を持たせられるか。第４部では、演算が満たすべき法則を要求できるか。

本節では、もう１段深く進みます。

値そのものが満たす性質を、型に入れられるか。

「この行列は正則である」という性質は、演算についてのものではありません。個々の値が持つ性質です。

なぜ、これがさらに難しいのか

第１部で、GDP という設計手法を見ました。値を包んで、性質を型に持たせる手法です。

「０より大きい」という性質であれば、これで守れました。
検査する関数を書き、それを通った値だけに札を付ける。

では、正則性はどうか。

正則かどうかは、行列の中身を計算しなければ分かりません。
そして、その計算は実行時に行われます。

型は、コンパイル時のものです。
実行時にしか分からないことを、そこに書く方法がありません。

GDP を使っても、実行時に確かめる作業そのものは消えません。

そして、確かめる作業そのものにも問題があります。
それを、この部で見ていきます。

対話の形に戻ります。

---

タロウくん：
先生、行列の話が出てきましたが、逆行列というのがありますよね。

専任講師：
あります。

行列 $A$ に対して、掛けると単位行列になる行列を、$A$ の逆行列と呼びます。

タロウくん：
単位行列というのは。

専任講師：
掛けても相手を変えない行列です。数でいう $1$ にあたります。

$$I = \begin{pmatrix} 1 & 0 \cr 0 & 1 \end{pmatrix}$$

対角線に $1$ が並び、それ以外は $0$ です。

タロウくん：
それで、逆行列を持つ行列と持たない行列があるんですか。

専任講師：
あります。

逆行列を持つ行列を 正則行列、持たない行列を 特異行列 と呼びます。

タロウくん：
どういう行列が持たないんですか。

専任講師：
たとえば、これです。

$$\begin{pmatrix} 1 & 2 \cr 2 & 4 \end{pmatrix}$$

２行目が、１行目のちょうど２倍になっています。

タロウくん：
それだと駄目なんですか。

専任講師：
情報が失われているからです。

行列は、ベクトルを別のベクトルへ移す操作だと考えられます。
この行列は、平面全体を１本の直線に潰してしまいます。

タロウくん：
潰したものは、元に戻せない。

専任講師：
そういうことです。

タロウくん：
分かりました。

それで、型の話ですが ──
「逆行列を持つ行列」という型 は作れないんですか？

専任講師：
そこが問題です。

タロウくん：
作れない、と。

専任講師：
Haskell では作れません。

タロウくん：
なぜですか。

専任講師：
正則かどうかは、行列の中身を見ないと分からないから です。

タロウくん：
中身は、型には書けない。

専任講師：
書けないものと、書けるものがあります。

たとえば行列の大きさは、型に書けます。
hmatrix にも、そのための仕組みがあります。

inv :: KnownNat n => L n n -> L n n

タロウくん：
L n n というのは？

専任講師：
$n$ 行 $n$ 列の行列を表す型です。
n が型のレベルに現れています。

タロウくん：
これなら、正方行列でないものを渡せませんね。

専任講師：
渡せません。コンパイルの段階で弾かれます。

タロウくん：
じゃあ、正則性 も同じように。

専任講師：
そこが違うのです。

大きさは、行列を作った時点で決まります。
中身が何であれ、３行３列は３行３列です。

正則性は、中身によって決まります。

同じ３行３列でも、正則なものとそうでないもの があります。

タロウくん：
中身を見れば分かるんですよね？

専任講師：
分かります。

行列式という量を計算して、それがゼロでなければ正則です。

しかし、その計算が行われるのは、実行時 です。

タロウくん：
型 は、コンパイル時 のものだから。

専任講師：
そうです。

実行時にしか分からないことを、型に書くことはできません。

タロウくん：
じゃあ、どうするんですか。

専任講師：
実際のライブラリを見てみましょう。

hmatrix というライブラリでは、逆行列を求める関数の型がこうなっています。

inv :: Field t => Matrix t -> Matrix t

タロウくん：
行列を受け取って、行列を返す。

専任講師：
そうです。

正則かどうかは、型に現れていません。

タロウくん：
特異行列を渡すと、どうなるんですか。

専任講師：
実は、そこが厄介なところです。

タロウくん：
エラーになるのでは。

専任講師：
なるとは限りません。

タロウくん：
えっ。

専任講師：
inv の実装を見ると、正方行列でない場合はエラーを投げます。

しかし、正方でありながら正則でない場合は、内部の数値計算に委ねられます。

タロウくん：
数値計算に委ねると、どうなるんですか。

専任講師：
第４部で見た浮動小数点数の問題が、ここで効いてきます。

理論上ゼロになるはずの行列式が、計算では $10^{-18}$ 程度の値になることがあります。

タロウくん：
ゼロではない、と判定される。

専任講師：
そうです。

計算が続行され、桁の大きな、意味のない値が返ってきます。

タロウくん：
エラーにならずに、間違った答えが返る。

専任講師：
これは、 Haskell固有の問題ではありません。

NumPy でも同じことが起きます。

浮動小数点数を使う限り、避けられません。

タロウくん：
そのほうが、エラーより怖いですね。

専任講師：
気づけませんから。

タロウくん：
実際に起きるんですか。

専任講師：
起きます。

たとえば、機械学習で共分散行列の逆行列を求める場面。

特徴量どうしに強い相関があると、行列が特異に近づきます。

タロウくん：
そこで、計算が壊れる。

専任講師：
壊れたことに気づかないまま、出てきた数値を使い続けることになります。

タロウくん：
モデルの結果がおかしいのに、原因が分からない。

専任講師：
そういう事態になります。

実務における、よくある落とし穴です。

タロウくん：
どうすればいいんですか。

専任講師：
hmatrix には、別の関数が用意されています。

invlndet :: Field t => Matrix t -> (Matrix t, (t, t))

タロウくん：
何かを一緒に返していますね。

専任講師：
行列式の絶対値の対数と、符号です。

これを見れば、正則かどうかを判断する材料 が得られます。

タロウくん：
判断する材料。

確実に分かるわけではない。

専任講師：
よく気づかれました。

閾値を決めて判定することになります。
どこまで小さければゼロとみなすか。

タロウくん：
それは、人が決める。

専任講師：
そうです。

そして、その判断は問題によって変わります。

タロウくん：
先生、結局 ── 型に書けないだけでなく、値としても確実には分からない。

専任講師：
浮動小数点数を使う限り は、そうです。

有理数など、誤差の出ない数を使えば、確実に判定できます。
ただし計算は遅くなります。

タロウくん：
それでも、invlndet のほうが inv よりましですね。

専任講師：
型ではなく、値として返す。

そこが要点です。

タロウくん：
先生、依存型 があれば 型 に書けるんですか。

専任講師：
書けます。

Idris や Lean であれば、次のような 型 が書けます。

• 「行列 $A$ と、$A$ が正則であることの証明を受け取り、逆行列を返す関数」

タロウくん：
証明 を渡す。

専任講師：
そうです。

証明を持っていない人は、この関数を使えません。

タロウくん：
でも、その証明は誰が書くんですか。

専任講師：
そこが問題です。

行列の中身が実行時に決まるなら、証明も実行時に作るしかありません。

タロウくん：
実行時に証明を作る。

専任講師：
「行列式を計算して、ゼロでないことを確かめ、その結果から証明を構成する」という手順になります。

タロウくん：
結局、実行時に確かめているのと同じでは。

専任講師：
確かめる作業自体は同じです。

違うのは、確かめた結果が値として残り、それを持っていないと次の関数を呼べない という点です。

タロウくん：
確認を忘れることがなくなる。

専任講師：
それが利点です。

タロウくん：
先生、なんだか ── 型 で表せることには限りがあるんですね。

専任講師：
限りがあります。

そして、その限界は、言語によって違います。

Haskell で表せないことが、Idris や Lean で表せることがある。

しかし、どの言語でも、実行時にしか分からないことは実行時にしか分かりません。

タロウくん：
当たり前のようですが、大事なことですね。

専任講師：
型システムに何を期待するか。

その見積もりを誤ると、設計を間違えます。

---

第９部 ── 各言語の型システムを比べる

本記事には、Haskell 以外の言語が複数登場しました。

最後に、それらを並べて整理します。

比較する軸

代数構造 を扱ううえで、 型システム に問われるのは次の点です。

軸	問い
複数の実装	同じ型に、複数の構造を持たせられるか
法則の要求	演算が満たすべき性質を、型で要求できるか
法則の検査	その要求が、コンパイラによって確かめられるか
記述の負担	インスタンスを書くのに、どれだけ手間がかかるか

一覧

言語	複数の実装	法則の要求	法則の検査	記述の負担
Haskell	不可	不可	──	小
Rust	不可	不可	──	小
Idris	可	可（外部）	可	中〜大
Lean 4	可	可	可	大
Rocq	可	可	可	大
Agda	可	可	可	大

「法則の要求」の欄で、Idris だけ「外部」と記しました。
標準ライブラリには法則付きのインターフェースがないためです。

表から読み取れること

左の２列と、右の１列が、逆向きに動いています。

法則を要求できる 言語ほど、記述の負担 が大きくなります。

逆に、負担が小さい言語では、法則を要求できません。

これは偶然ではありません。

法則を要求するとは、その証明を提出させるということです。

証明を書く手間は、そのまま記述の負担になるのです。

	Haskell	Rust	Idris	Lean 4 / Rocq
保証の強さ	弱い	弱い	中間	強い
記述の負担	小さい	小さい	中間	大きい

この交換関係は、避けられません。

どちらか一方だけを取ることはできない ── そう理解したうえで、何を優先するかを決めることになります。

第１０部で、その判断の材料を示します。

法則付きの階層を積み上げられるか

もう１つ、比較したくなる軸があります。

Semigroup の上に Monoid、その上に Group ── そうやって法則付きのクラスを積み上げていけるか、という点です。

なぜ、積み上げが難しいのか

第４部で、Idris が直面した困難を取り上げました。

SemigroupV が「結合律を満たす」と証明していても、その証明がどの <+> についてのものか分からなくなるという問題でした。

この問題は、同じ型に複数の実装を書くことができること に起因します。

どの実装について証明したのかが、特定できなくなるのです。

Idris、Lean、Rocq、Agda は、いずれも同じ型に複数の実装を書けます。

つまり、この問題は４言語すべてに生じうる のです。

では、なぜ Lean ではこの問題が生じないのか

対処の仕方が違うからです。

言語	どう対処しているか
Lean 4、Rocq	演算と法則を、同じクラスに入れる
Agda	代数構造の情報を１つにまとめ、使うときに引数として渡す
Idris	標準では法則を扱わない。外部ライブラリが、この問題に直面している

Lean と Rocq の方法は、第７部で見たとおりです。

Semigroup が Mul を継承し、その * についての結合律を同じクラスの中で要求する。
分離しないので、食い違いようがありません。

Agda が採用した方法 は、どの代数構造を使うかを Agda に選ばせない、というものです。

Haskell や Lean では、x <> y と書けば、どのインスタンスを使うかを処理系が自分で判断します。

Agda の標準ライブラリでは、代数構造について、処理系にその判断をさせません。

「この演算は結合律を満たす」「単位元はこれ」といった情報を１つにまとめたものを作っておき、使うときに、それを引数として手渡します。

どの構造を使っているかが、書いたコードに現れるのです。

module Algebra.Structures where
  record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
    field
      isMagma : IsMagma ∙
      assoc   : Associative ∙

使うときは、こうなります。

-- 自然数の足し算が半群であることを、あらかじめ用意しておく
ℕ+-isSemigroup : IsSemigroup _+_

-- それを、引数として渡して使う
ex : ∀ n → (n + 1) + 1 ≡ n + 2
ex n = assoc ℕ+-isSemigroup n 1 1

最後の行に注目してください。

assoc は「結合律が成り立つ」という証明を取り出す名前です。
その直後に ℕ+-isSemigroup と書いています。

ここが、「どの構造の結合律か」を指定している部分です。

Haskell や Lean であれば、この指定は必要ありません。処理系が探してくれるからです。

Agda では、プログラマが ℕ+-isSemigroup を assoc の引数として渡します。

どの構造を使っているかがコードに明示される のです。

---

Haskell の強み

記述が軽い

インスタンスを書く度に、証明することは必要とされません。

data Move = Move Int Int

instance Semigroup Move where
  Move x1 y1 <> Move x2 y2 = Move (x1 + x2) (y1 + y2)

instance Monoid Move where
  mempty = Move 0 0

平面上の移動を表す型を作り、それをモノイドとして扱っています。

移動を２つ続けることが演算にあたり、動かないことが単位元にあたります。

これだけです。数行で済みます。

同じことを Lean の AddMonoid として書けば、次を証明する必要があります。

• 結合律
• 左単位元の性質
• 右単位元の性質

いずれも整数の性質から従うので、難しくはありません。しかし、書かなければ通りません。

「とりあえず動かす」までの距離が、圧倒的に短い。

インスタンスの選択が一意に決まる

コヒーレンスにより、x <> y がどのインスタンスを使うかは、型から一意に決まります。書かれた場所によって変わりません。

第３部で見たとおり、Lean や Idris では、どのインスタンスが選ばれるかを意識する必要があります。

Haskell では、その心配が要りません。

コードを読むとき、その式が何を意味するかを、局所的に判断できます。

型推論が効く

コヒーレンスの副産物です。

インスタンスが一意に決まるため、型推論が素直に働きます。

idris2-algebra の作者が「型推論をほぼ諦めることになる」と記していたのは、まさにこの点です。

実行時の性能が読みやすい

型クラスの解決がコンパイル時に完結するため、実行時のオーバーヘッドが予測しやすくなります。

Haskell では、証明という値そのものが存在しません。

Lean では、証明も値の一種です。
関数の引数として受け取り、返り値として返すことができます。

そのため、コンパイルして生成されるプログラムの中に、証明が含まれることになります。

実際にはコンパイル時に取り除かれるため、実行速度には影響しません。
ただし、その仕組みを理解しておく必要があります。

---

Haskell の弱み

法則が守られる保証がない

第４部で見たとおりです。

Monoid のインスタンスが結合律を破っていても、コンパイルは通ります。

そして、標準ライブラリ自身がそれをやっています。Double は Num のインスタンスですが、浮動小数点数の足し算は結合律を満たしません。

同じ型に複数の構造を持たせられない

第３部の問題です。

整数の加法と乗法を、両方とも Monoid として扱うことはできません。newtype で包む必要があります。

**そして、包むと構造どうしの関係が失われます。**環という概念が表現できなくなります。

依存型がない

「行列 $A$ と、$A$ が正則であることの証明を受け取る関数」を書けません。

第８部で見たとおりです。

型レベルで自然数を扱う仕組み（KnownNat）はありますが、値についての性質を型に持ち込むことはできません。

---

Lean 4 の強みと弱み

強み ── 法則が証明として要求される

第７部で見たとおりです。

Group のインスタンスを作るには、群の公理をすべて証明する必要があります。嘘の実装ができません。

強み ── 演算と法則が同じクラスにある

Idris が抱える困難を、この設計で回避しています。

Semigroup が Mul を継承し、その * についての結合律を、同じクラスの中で要求する。食い違う余地がありません。

強み ── 大規模なライブラリがある

Mathlib には、10万を超える定理が収められています。

代数構造の階層も、群から可換環、体、加群、代数まで整備されています。

弱み ── 記述の負担が大きい

インスタンスを１つ書くために、複数の証明を書く必要があります。

実際には補助関数が用意されているため、すべてを手で書くことは稀です。しかしどこかで誰かが証明しているという事実は変わりません。

弱み ── インスタンスの解決が複雑

複数のインスタンスを許すため、どれが選ばれるかを制御する仕組みが要ります。

優先度、探索順、instance 属性の管理 ── これらを理解する必要があります。

Mathlib では、この問題を インスタンス・ダイアモンド と呼んで、長く議論しています。

同じ構造に複数の経路で到達したとき、それらが一致することを保証する必要があるためです。

弱み ── 汎用のプログラミング言語としての成熟度

Lean 4 はプログラミング言語としても設計されていますが、ライブラリの層の厚さでは Haskell に及びません。

Web サーバーを書く、データベースに接続する
── そうした用途では、Haskell のほうが選択肢が多くなります。

---

Idris の強みと弱み

強み ── 証明を「選べる」

設計者の言葉を、第４部で引きました。

証明を書きたい人は書ける。書きたくない人は書かなくてよい。

この柔軟さは、実用の場面で効きます。
すべてを証明しなければ動かない体系では、書き始めるまでの負担が大きすぎます。

強み ── Haskell に近い構文

Haskell を書ける人が、比較的短い学習で入れます。

弱み ── 法則の分離が裏目に出る

第４部で見たとおり、法則付きインターフェースの階層を作ることが困難です。

Semigroup（演算）と SemigroupV（法則）を別のインターフェースにした結果、「証明できるが、その証明が何についてのものか追えなくなる」 という問題が生じます。

Lean や Rocq は、演算と法則を同じクラスに入れることで、この問題を回避しています。

コヒーレンスがない点は同じでも、設計によって結果が変わるわけです。

弱み ── 標準ライブラリに法則がない

SemigroupV は外部ライブラリです。
標準の Semigroup は、Haskell と同じく法則を持ちません。

---

Rust の位置

Rust は、この記事で扱った言語の中で、Haskell に最も近い位置にあります。

共通点

• コヒーレンスがある（１つの型に１つの実装）
• 法則を型で要求できない
• 依存型がない

違い

Rust は、PartialEq と Eq を分けています。

第１部で見たとおり、反射性が成り立つかどうかで、トレイトを分けているのです。

Haskell の Eq には、この区別がありません。Double も Integer も、同じ Eq に属します。

法則を検査できないなりに、階層で区別する。

Rust はその方向を選んでいます。

---

何を選ぶか

以上を踏まえると、次のように整理できます。

したいこと	適した言語
代数的な抽象化を使って、実用のプログラムを書く	Haskell
数学の定理を証明する	Lean 4、Rocq
証明を書きつつ、プログラムも書く	Idris
性能と安全性を両立させる	Rust
ホモトピー型理論を扱う	Agda

そして、これらは競合していません。

保証の強さと、記述の負担。この２つは交換関係にあります。

どこで釣り合いを取るかが、言語ごとに違うだけです。

base に代数構造がない、ということの意味

最後に、本記事の出発点に戻ります。

Haskell の base に群も環も体もないのは、怠慢ではありませんでした。

法則を表現できない型システムの上に、法則で定義される構造を置いても、名前だけのものになります。

Group という名前の型クラスを作っても、そのインスタンスが群である保証はありません。ドキュメントに「群の公理を満たすこと」と書くだけです。

それは、Num が抱えている問題と同じです。

外部ライブラリがその道を選ぶのは、それでも有用だからです。名前があれば、意図が伝わります。抽象化もできます。

しかし、標準ライブラリがそれを提供することには、別の重みがあります。

base に入れば、それが Haskell の標準的な語彙になります。保証できないものを標準にすることの是非 ── そこに、判断があったのだと考えられます。

---

第１０部 ── 乗り換えれば解決するのか

第９部で、各言語の強みと弱みを整理しました。

そこで、当然の問いが出てきます。

Haskell でできないことがあるなら、できる言語に乗り換えればよいのではないか。

本節では、この問いに答えます。

結論を先に

そう単純ではありません。

理由は２つです。

第１に、乗り換え先には別の欠点があります。
Haskell にはない欠点です。

第２に、そもそも比較の土俵が違います。

本記事で扱ってきたのは「代数構造を型クラスでどう表現するか」という一点にすぎません。

実際に言語を選ぶときは、他に考慮すべき要素が数多くあります。

順に見ていきます。

---

Haskell以外の言語：各言語の強みと弱み

Lean 4 の場合

得られるもの ── 法則を証明として要求できます。嘘の実装ができません。

失うもの

① 記述の負担

インスタンスを１つ書くたびに、複数の証明が必要になります。

第９部で述べたとおり、実際には補助関数が用意されているため、すべてを手で書くことは稀です。
しかし、新しい構造を定義するときは、誰かがどこかで証明を書くことになります。

② ライブラリの層の厚さ

Haskell には、Web、データベース、並行処理、JSON、暗号など、実用のためのライブラリが揃っています。

Lean 4 も汎用言語として設計されていますが、この層はまだ薄い。
数学の形式化以外の用途では、選択肢が限られます。

③ 実行時の性能

Lean 4 のコンパイラは、C を経由してネイティブコードを生成します。
LLVM を使う経路も開発されています。

性能は改善が続いていますが、GHC が長年かけて積み上げた最適化には、まだ及びません。

なお、Lean 4 のコンパイラ自体が Lean 4 で書かれており、この点では実用言語としての設計が実証されています。

④ コンパイル時間

証明を含むコードのコンパイルは、時間がかかります。Mathlib 全体のビルドには、相当な時間を要します。

Rocq の場合

得られるもの ── Lean と同様、法則を証明として要求できます。より長い歴史と、豊富な形式化の蓄積があります。

失うもの

① プログラムとしての実行

Rocq の内部言語 Gallina で書いた関数は、Rocq の中でも評価できます。ただし、その評価は高速ではありません。

実用的な速度で動かすには、OCaml や Haskell、Scheme へ 抽出（extraction）する必要があります。

抽出では、証明に相当する部分が取り除かれます。データ構造が満たすべき条件の証明は、計算結果に寄与しないためです。

この過程で、性能特性が変わることがあります。

Rocq の豊かな型システムを、 OCamlの型システム へ移す際に、型情報が失われるからです。

② 学習の負担

タクティクという証明の書き方を、別途習得する必要があります。プログラムを書く感覚とは、かなり異なります。

③ 抽出の際に信頼が要る

Rocq で証明したコードを OCaml に抽出するとき、その抽出の仕組み自体は検証されていません。

CompCert の論文 は、この点を明示しています。

信頼すべき対象として、Rocq の実装、抽出機構、 OCaml のコンパイラと実行環境が挙げられています。

Agda の場合

得られるもの ── 依存型を持ち、法則を型で表現できます。ホモトピー型理論も扱えます。

失うもの

① 実用のためのライブラリ

Agda で書いたプログラムは、 Haskell や JavaScript へコンパイルできます。

しかし、実用のプログラムを書くための基盤 ── ネットワーク、データベース、並行処理といった領域 ── は、Haskell に遠く及びません。

Agda は依存型と型理論の研究のために設計されており、産業利用を主眼に置いていないためです。

② インスタンス解決の弱さ

第９部で見たとおり、Agda では構造を明示的に渡す流儀が主流です。

曖昧さは避けられますが、記述は冗長になります。

③ コンパイル速度

型検査に時間がかかります。大きなファイルでは、編集のたびに待つことになります。

Idris 2 の場合

得られるもの ── Haskell に近い構文で、依存型が使えます。証明を書くかどうかを選べます。

失うもの

① コヒーレンスがない

第４部で見たとおりです。

法則付きの階層を積み上げることが困難になります。

② 生態系の規模

Haskell には Hackage という大規模なパッケージ配布の仕組みがあり、数万のライブラリが公開されています。

Idris の生態系は、それに比べるとはるかに小さい。

必要なライブラリが存在しない可能性があります。

③ 言語の変化

Idris 1 から Idris 2 への移行 では、互換性のない変更が多数ありました。

Idris 2 は、 量的型理論 （Quantitative Type Theory）という新しい基盤の上に作り直されています。

研究が進行中の言語である、という点は認識しておく必要があります。

OCaml、Standard ML の場合

ここは、別の話になります。

ML 系の言語は、そもそも型クラスを持ちません。

代わりに、モジュールシステムがあります。

module type MONOID = sig
  type t
  val empty : t
  val combine : t -> t -> t
end

module IntAdd : MONOID with type t = int = struct
  type t = int
  let empty = 0
  let combine x y = x + y
end

module IntMul : MONOID with type t = int = struct
  type t = int
  let empty = 1
  let combine x y = x * y
end

module type が、モジュールの型（シグネチャ）を宣言します。Haskell の class に相当する役割です。

module ... : MONOID with type t = int = struct ... end が、その実装です。

with type t = int という部分に注意してください。

これがないと、モジュールの外から見たとき t が何の型か分からなくなります。IntAdd.combine 3 5 と書いても、3 が IntAdd.t であることをコンパイラが確認できません。

この指定を、型の等式制約と呼びます。

さて、注目すべき点があります。

**同じ int に対して、IntAdd と IntMul の両方を書けます。**しかも、名前が付いています。

使うときは、どちらを使うかを明示します。

IntAdd.combine 3 5    (* 8 *)
IntMul.combine 3 5    (* 15 *)

(* ... *) は、OCaml における注釈の書き方です。

**曖昧さがありません。**そして newtype で包む必要もありません。

得られるもの ── 同じ型に複数の構造を、明示的に持てます。実用のライブラリも充実しています。

失うもの

① 自動的な解決がない

Haskell では mconcat [1,2,3] と書けば、型からインスタンスが決まります。

ML では、どのモジュールを使うかを毎回書くか、ファンクタ（モジュールを受け取ってモジュールを返す仕組み）で受け渡す必要があります。

記述が冗長になります。

② 法則は、やはり検査されない

MONOID というシグネチャに、結合律は書けません。Haskell と同じ立場です。

③ 型推論の範囲

OCaml には強力な型推論がありますが、モジュールの型は自分で書く必要があります。

なお、OCaml には modular implicits という、型クラスに近い機能の提案があります。長く議論されていますが、2026年時点で標準機能にはなっていません。

---

乗り換えの前に考えること

以上を踏まえると、次のことが言えます。

「Haskell でできないこと」の多くは、実務では問題になりません。

Monoid の結合律が検査されないことで、実際にどれだけの障害が生じているか。

多くの現場では、テストで足ります。QuickCheck があれば、大半の誤りは見つかります。

証明が必要になるのは、次のような場面です。

• 誤りが人命や巨額の損失に直結する
• 数学の定理そのものを扱っている
• 検証結果を第三者に示す必要がある

そうでなければ、記述の負担に見合いません。

---

ユースケース別の選び方

具体的な場面ごとに、整理します。

ケース１ ── 業務アプリケーションを書く

Haskell、あるいは OCaml、Scala、Rust

代数構造の厳密さより、ライブラリの充実と開発の速さが重要です。

型クラスの法則が検査されないことは、テストで補えます。

Lean や Agda を選ぶ理由はありません。

ケース２ ── 数値計算ライブラリを作る

Haskell ＋ 外部の代数ライブラリ

algebra や numeric-prelude を使い、法則は QuickCheck で試験する。

第６部で見た algebraic-structures が、まさにこの方針でした。

厳密さが要るなら、Lean や Rocq で仕様を検証し、実装は Haskell で書くという分担もありえます。

ケース３ ── 数学の定理を証明する

Lean 4、Rocq、Agda、Isabelle/HOL

Mathlib をはじめとする既存の形式化の蓄積が効きます。
すでに証明された定理を使って、新しい定理を証明できます。

Haskell は、こうしたことを実現することができません。

定理を型として書き、その証明を値として作る ── そのための依存型が、Haskell にはないためです。

なお、Isabelle/HOL は依存型を持ちませんが、高階論理に基づく別の方式で 定理証明を行います。
解析学や代数の形式化に、長い実績があります。

ケース４ ── 暗号やプロトコルを検証する

Rocq、あるいは F*

この分野には、実際に使われている成果があります。

CompCert は、Rocq（当時の Coq）で検証された C コンパイラです。
ISO C99 のほぼ全体を対象としています。

証明されているのは、コンパイル結果が元のコードの意味を保つということです。

正確には「元のプログラムが持ちうる振る舞いの中に、生成されたコードの振る舞いが含まれる」という形で定式化されています。

検証された部分は Rocq で書かれ、OCaml のコードとして抽出されます。
それを手書きの OCaml コードと組み合わせて、実行可能なコンパイラにしています。

HACL* は、F* で検証された暗号ライブラリです。
Mozilla Firefox で実際に使われています。

ここで、注意すべき点があります。

検証されたからといって、すべてが保証されるわけではありません。

CompCert の場合、信頼しなければならないものが残ります。
Rocq 自身の実装、抽出の仕組み、OCaml のコンパイラと実行環境、そして手書きの OCaml コードです。

これらをまとめて 信頼計算基盤（trusted computing base）と呼びます。

「証明したから安全」ではなく、「何を信頼しているかが明確になった」 というのが、正確な理解です。

ケース５ ── 型システムそのものを研究する

Agda、Rocq

依存型の性質を調べたり、新しい型理論を試したりする用途です。

実用のライブラリは要りません。

ケース６ ── 依存型を使いつつ、プログラムも書きたい

Idris 2

第９部で見た「証明を選べる」という設計が効きます。

ただし、ライブラリの少なさは覚悟する必要があります。

ケース７ ── 既存の Haskell コードがある

Haskell を使い続ける

Haskell以外の言語に乗り換える際に生じるコストは、得られるものに見合いません。

部分的に検証したい箇所があるなら、その部分だけを別の言語で検証し、結果を Haskell に反映させるという方法があります。

---

組み合わせるという選択

乗り換えるか、留まるか。この２択ではありません。

実際の大きな計画では、複数の言語が使い分けられています。

役割	言語の例
仕様の記述と検証	Rocq、Lean 4、Isabelle/HOL、TLA⁺
実装	Haskell、OCaml、Rust、C
テスト	QuickCheck などの性質試験

TLA⁺ は、並行処理や分散システムの仕様を記述するための言語です。定理証明支援系とは方式が異なり、状態を網羅的に探索して誤りを見つけます。Amazon Web Services などで使われています。

すべてを１つの言語で完結させる必要はありません。

そして、検証する部分を絞ることも重要です。すべてを証明するのは、現実には不可能です。

どこが壊れると致命的か。そこだけを検証する。それが実務的な釣り合いです。

---

まとめると

本記事で挙げた Haskell の弱点のうち、法則を検査できない点と複数の構造を持てない点は、別の言語で解消できます。

しかし、乗り換え先には別の弱点があります。

得たいもの	乗り換え先	代わりに失うもの
法則の証明	Lean 4、Rocq	記述の軽さ、ライブラリ
複数の構造	OCaml（モジュール）	自動解決、簡潔さ
依存型と実用性の両立	Idris 2	コヒーレンス、開発規模
型理論の研究	Agda	実用のライブラリ

そして、そもそも代数構造の扱いが、言語選択の決め手になる場面は多くありません。

本記事で扱ってきたのは、言語の設計を理解するための切り口です。言語を選ぶための基準ではありません。

その区別を、最後に申し上げておきます。

---

まとめ

① Haskell の base に、群も環も体も半環もありません。

あるのは Semigroup と Monoid の２つだけです。

② Num は代数構造ではありません。

加算・乗算・符号反転・絶対値・整数からの変換を、実用の都合でまとめたものです。行列やガウス整数を扱うとき、絶対値と符号が障害になります。

③ 障害は３つあります。

コヒーレンス、法則を検査できないこと、階層の設計が一意でないこと。

このうち、コヒーレンスと法則の検査は、通常の型クラス機構を使う限り制約として残ります。ただし、newtype や明示的な辞書の受け渡し、テスト、GDP や LiquidHaskell といった手法によって、用途に応じて影響を緩和することはできます。

④ 整数は、足し算について群、掛け算についてモノイドをなします。

１つの型に１つの実装しか書けないので、両方を同時に表現できません。Sum と Product で包む回避策が使われますが、２つの構造の関係は失われます。

⑤ Monoid の結合律は、ドキュメントに書かれているだけです。

GHC は確かめません。QuickCheck による試験が、実務上の対処になっています。

⑥ Idris では法則を型で要求できますが、階層の構築が困難です。

演算と法則を別のインターフェースに分けた結果、法則付きインターフェースが「どの実装を検証しているのか」を追えなくなります。

⑦ Lean の Mathlib では、演算と法則を同じクラスに入れています。

そのため、Idris の困難が生じません。嘘の実装もできません。ただし、書く負担は増えます。

⑧ 階層の設計は、どの体系でも難問です。

Mathlib も Mathematical Components も、同じ問題に取り組んでいます。

⑨ 「逆行列を持つ」という性質は、Haskell の型では表せません。

行列の大きさは型に書けます。作った時点で決まるからです。しかし正則性は中身によって決まるため、書けません。

さらに、浮動小数点数を使う限り、値としても確実には判定できません。誤差のために、特異行列がエラーにならず、意味のない値が返ることがあります。

結論

本記事は「base に群も環も体もない」という事実から出発しました。

その理由を辿ると、３つの障害に行き当たりました。そして、そのうち最も根深いものは、base の設計判断ではなく、Haskell の型システムそのものの性質でした。

Haskell の型クラスが宣言できるのは、演算の名前と型までです。

その演算が満たすべき法則を、インスタンスの条件として要求することはできません。

この制約は、GHC の通常の型クラス解決を使う限り、外部ライブラリにも等しくかかります。algebra も numeric-prelude も、法則をドキュメントか QuickCheck の性質として置くほかありません。群や環のクラスを用意することはできても、その公理の証明をインスタンスの条件として求めることはできないのです。

なお、冒頭の発展コラムで触れたとおり、Haskell でも法則を型として扱う手法は存在します。ただし、それらはいずれも型クラスの外側にある仕組みです。

値についての法則を、型クラスのフィールドとして直接表現し、その証明をインスタンスの成立条件として要求するには、依存型のような仕組みが必要になります。そして依存型を持つ体系では、今度は証明を書く負担が生じます。

Haskell は、法則を型システムによって強制することよりも、軽量な型クラスによる抽象化を優先する設計になっています。

これは欠陥ではなく、選択です。何を保証したいかによって、適切な選択は変わります。

本記事の限界について

本記事は、各ライブラリのドキュメントとソースコード、および公開されている論文に基づいて書いています。

記事中の Haskell と OCaml のコードは、GHC 9.4.7 および OCaml の処理系で動作を確認しました。Lean と Idris のコードについては、公式ドキュメントの記述に基づいて記載しています。

代数構造の階層設計については、各ライブラリの作者による設計判断が背景にあります。本記事はその一部を整理したものであり、判断の全体を追ったものではありません。

誤りがありましたら、ご指摘いただけますと幸いです。

出典

現行の仕様とドキュメント

• Data.Monoid, base
• Data.Semigroup, base
• numeric-prelude, Hackage
• Numeric Prelude, HaskellWiki
• algebra, Hackage
• hmatrix, Hackage
• stefan-hoeck/idris2-algebra, GitHub
• Interfaces.Verified, Idris 1 contrib
• Algebra.Structures, Agda standard library
• Numeric.LinearAlgebra.Static, hmatrix
• numeric classes, Haskell Prime Wiki
• Haskell 2010 Language Report, Chapter 6: Predefined Types and Classes
• GHC User's Guide
• GHC.Num, base, Hackage

設計史と研究資料

• P. Wadler, S. Blott, "How to make ad-hoc polymorphism less ad hoc", POPL, 1989年
• A. Ghitza, M. Raum, "HLinear: Exact Dense Linear Algebra in Haskell", arXiv:1605.02532, 2016年
• R. Affeldt, C. Cohen, D. Rouhling, "Formalization Techniques for Asymptotic Reasoning in Classical Analysis", Journal of Formalized Reasoning, 2018年
• K. Sakaguchi, "Validating Mathematical Structures", arXiv:2002.00620, 2020年
• H. Ishii, "A Purely Functional Computer Algebra System Embedded in Haskell", arXiv:1807.01456, 2018年
• X. Leroy, "A formally verified compiler back-end", Journal of Automated Reasoning 43(4), 2009年
• D. Monniaux, S. Boulmé, "The Trusted Computing Base of the CompCert Verified Compiler", arXiv:2201.10280, 2022年
• J. Protzenko 他, "EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider", IEEE S&P, 2020年

検証されたソフトウェア

• CompCert
• Project Everest（HACL*、EverCrypt を含む）
• TLA⁺

他の言語

• OCaml Manual: Modules
• Modular implicits, L. White, F. Bour, J. Yallop, ML Workshop, 2014年
• Isabelle

Haskell で法則を扱う手法

• M. Noonan, "Ghosts of Departed Proofs (Functional Pearl)", Haskell Symposium, 2018年
• N. Vazou, "Liquid Haskell: Haskell as a Theorem Prover", University of California San Diego, 2016年
• LiquidHaskell
• Data.Type.Equality, base

Lean の型クラス解決

• Instance Synthesis, The Lean Language Reference
• D. Selsam, S. Ullrich, L. de Moura, "Tabled Typeclass Resolution", arXiv:2001.04301, 2020年
• The mathlib Community, "The Lean mathematical library", CPP, 2020年

型クラスと代数構造

• Semiring, Type Classes
• Mathlib.Algebra.Group.Defs, Mathlib