summary:
$K$ を有限集合[例：name, age, email]などの識別子の集合とする.そして,その各 $k \in K$ に対して,その値の型 $T(k)$ が定義されているものとする.このとき,型アノテーションをともなうレコードスキーマを $\tau : K \to \mathsf{Type}$ という写像で与えると,各レコード $r$ は,以下のような写像で表される.\[r : \prod_{k \in K} \tau(k) \]
形式的には、レコード $r$ は従属直積 $\prod_{k \in K} \tau(k)$ の要素である.これは,各キー $ k \in K $ に対して,型 $\tau(k)$ に属する値 $ v_k $ を対応させるような写像\[r : K \to \bigcup_{k \in K} \tau(k), \quad r(k) = v_k \in \tau(k)\]として記述されることを意味する.
この定義は,プログラミング言語におけるレコード型[例：Haskell, ML, Rust 等]を抽象化した構造的モデルであり,型安全なフィールドアクセス,部分型,多相的レコードなどの型理論的議論の基礎となる.
また,この定義は,プログラミング言語における以下のような構造を,型理論的・集合論的に正確にモデル化しているものである.
data Person = { name :: String, age :: Int }つまり,レコードのフィールド名 name と age からなる有限集合を,次のように定めると,\[K = \{ \texttt{name}, \texttt{age} \}\]これは,レコードのキーすなわち識別子の集合である.
次に,各キーに対応する型を与える写像 $ \tau : K \to \mathsf{Type} $ を定める.具体的には,\[\tau(\texttt{name}) = \mathsf{String}, \quad \tau(\texttt{age}) = \mathsf{Int}\]
このようにして,キーとそれに対応する型の対が決まり,レコードスキーマが形成される.
すると,具体的なレコード $ r $[例えば, "Alice" という名前と 30 という年齢を持つ人物]とは,関数\[r : \prod_{k \in K} \tau(k)\]
の要素,すなわち各キー $ k \in K $ に対して値 $ v_k \in \tau(k) $ を対応させるような写像として定義される.この写像は具体的には次のように記述される.\[r(\texttt{name}) = \text{"Alice"}, \quad r(\texttt{age}) = 30\]
従って,レコードとは,与えられたスキーマに従って定まる有限集合上の 従属直積[dependent product] の要素である.
Mathematics is the language with which God has written the universe.