初心者のためのレコード型推論

Haskell for all 2026年6月23日火曜日 初心者のためのレコード型推論 私がこの記事を書いている理由は、匿名レコードの型推論に関するもっと高度な記事を実際に書きたかったのですが、ほとんどの読者はその記事を単独では理解できないことに気づいたからです。そこで、型理論の初心者向けに基礎を教えるための入門記事を書こうと考えました。両方の記事を書いているのは、匿名レコードの優れた型推論が静的型付け言語にとって大きな足かせの一つであり、十分な人々がこれを理解していない、またはその理由を把握していないと私が信じているからです。また、プログラミング言語の専門家が何が可能だと理解していることと、一般のプログラマーが慣れ親しんでいることとの間に大きな隔たりがあるとも考えています。XKCD #2501をもじって言えば: したがって、この記事（および次の記事）は、30年以上前の型理論の分野がどこにあったのかを解説するものであり、私たちの業界はまだそれに追いついていません。 匿名レコード これは匿名レコードの型推論に関する記事だと述べましたが、匿名レコードが何であるかを知らない、あるいはその名前で認識しないプログラマーに何人か会ったことがあるので、簡単に触れておきます。匿名レコードとは、関連するデータ型宣言を必要としないレコードのことで、動的型付け言語では非常に一般的です。例えば、JavaScriptでは「オブジェクト」と呼びます: ```javascript { name: "Alice", age: 25 } ``` Pythonでは「辞書」と呼びます: ```python { "name": "Alice", "age": 25 } ``` Rubyでは「ハッシュ」と呼びます: ```ruby { :name => "Alice", :age => 25 } # … or equivalently: { name: "Alice", age: 25 } ``` …そしてNixでは「アトリビュートセット」と呼びます: ```nix { name = "Alice"; age = 25; } ``` もしJSONを扱ったことがあるなら、匿名レコードを扱ったことがあります。なぜならJSONオブジェクト（JavaScriptオブジェクトと同様に）は匿名レコードだからです。 静的型付け 匿名レコードをサポートする静的型付けプログラミング言語は少数です。なぜなら、静的型付け言語は通常、名前付きデータ型を好むからです。例えば、Haskellは匿名レコードをサポートしておらず、すべてのレコードに対して次のようなデータ型宣言を要求します: ```haskell data Person = Person{ name :: Text, age :: Integer } example :: Person example = Person{ name = "Alice", age = 25 } ``` …しかし、それでも匿名レコードをサポートする静的型付けプログラミング言語はいくつかあります。TypeScript: ```typescript { name: "Alice", age: 25 } : { name: string, age: number } ``` …またはC#（「匿名型」と呼びます）: ```csharp new { Name = "Alice"; Age = 25 } ``` …またはPureScript（レコードと呼びます）: ```purescript { name: "Alice", age: 25 } :: { name :: String, age :: Int } ``` レコードに対する操作なしで、レコードリテラルの言語サポートだけが必要な場合、それらの型を推論するのはかなり簡単です。しかし、そのためには、型理論の記法をいくつか導入する必要があります。まず、式（()）が次のいずれかであると述べる基本的な抽象構文木を定義することから始めましょう: - ブール値 (e.g. `true`) - 文字列 (e.g. `"hello"`) - 数値 (e.g. `123`) - 0個以上のフィールドを含むレコード (e.g. `{ name: "Alice", age: 25 }`) それを形式的に記述する方法は次のとおりです: ``` e :: Expression ``` …そして同等のHaskellコードは次のようになります: ```haskell type Identifier = Text data Expression = Boolean Bool | String Text | Number Double | Record (Map Identifier Expression) ``` フィールドには任意の式を格納できるため、次のようにレコードをネストできます: ``` { name: "Alice", address: { street: "Main St", number: 123 } } ``` また、推論された型についても抽象構文木を定義する必要があります。これは次のいずれかになります: - `BooleanType` 型 - `StringType` 型 - `NumberType` 型 - 0個以上のフィールドを含むレコード型 (e.g. `{ name :: String, age :: Int }`) それに使用する記法は次のとおりです: ``` t :: Type ``` 同等のHaskellコードは次のようになります: ```haskell data Type = BooleanType | StringType | NumberType | RecordType (Map Identifier Type) ``` 式と型の構文ができたので、型推論ルールを定義できます: - ブール値と文字列は常にその型を持ちます (e.g. `true` は `BooleanType`) - 数値は常に `NumberType` 型を持ちます これらのルールをこの記法で記述します: ``` ----------------- true : Boolean ------------------ "foo" : String --------------- 123 : Number ``` この記法を初めて見る場合、型推論関数を実装するための数学的な擬似コードと考えることができます。同等のHaskell関数は次のようになります: ```haskell infer :: [(Identifier, Type)] -- ^ context, a.k.a. "Γ" (currrently unused) -> Expression -- ^ input expression -> Either Text Type -- ^ output inferred type (currently never fails) infer context (Boolean _) = return BooleanType infer context (String _) = return StringType infer context (Number _) = return NumberType ``` 注: 完全なHaskellコードは付録にあります。 さて、次のようなレコードリテラルの型を推論したいとします: ``` { name: "Alice", age: 25 } ``` 通常、この式の型を手作業で次のように推論します: 1. `{