1. 導入：なぜ「単射」を知る必要があるのか
プログラミングをしていて、「コンパイラがなぜこんなに賢く型を推論できるのか？」と不思議に思ったことはありませんか？その秘密の一つが、データ型が持つ「単射（インジェクティブ）」という性質です。この性質を理解することで、型エラーに悩まされた時に「なぜコンパイラが型を特定できないのか」という原因を論理的に突き止められるようになります。
2. 基礎知識：単射（Injective）とは何か
数学的な定義を噛み砕くと、「T a = T b ならば a = b である」という性質のことです。
例えば、リスト型 [a] を考えてみましょう。もし [Int] = [String] であれば、それはつまり Int = String であることを意味します。これが「単射」です。
逆に、もし T a = T b であっても a と b が異なり得るような型があったらどうでしょう？コンパイラは「T a が何の型なのか」を逆算して特定することができず、型推論で迷子になってしまいます。
3. 実装と解決策
通常の data や newtype で定義されたデータ型は、常に単射です。しかし、高度な型機能である「型族（Type Family）」を使うと、この性質が崩れることがあります。
型族は「型から型への関数」のようなものですが、複数の異なる入力（aとb）に対して同じ出力（c）を返すことが可能です。この場合、コンパイラは「c から a を推論する」ことができず、エラーを吐くことがあります。これを解決するには、GHCの拡張機能である TypeFamilyDependencies を使用して、「この型族は単射である」とコンパイラに明示的に教える必要があります。
4. サンプルプログラム
以下のコードは、通常のデータ型が持つ単射性を利用した型推論の例です。
— data型はデフォルトで単射です
data Box a = Box a
— この関数はコンテナの型から中身の型を自然に推論します
— Box a が Box Int であるとわかれば、a は Int であると推論されます
extract :: Box a -> a
extract (Box x) = x
main :: IO ()
main = do
let myBox = Box 10 — myBox は Box Int 型として推論される
let value = extract myBox
print value — 結果: 10
— 単射性のおかげで、コンパイラは a が Int であることを知っています
5. 応用・注意点
現場で型族を使っている際、「Couldn’t match type…」というエラーが出た場合、多くは「コンパイラが単射性を証明できない」ことが原因です。
注意点：型族を定義する際は、可能な限り単射になるように設計するか、もし推論がうまくいかない場合は、明示的な型注釈（Type Annotations）を添えるのが最も安全な回避策です。型推論は魔法ではなく、このような「一意に決まるルール」の積み重ねで動いています。この仕組みを意識するだけで、より堅牢なプログラムが書けるようになりますよ。
コメント