同型再帰型
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/17 16:09 UTC 版)
同型再帰型では、再帰型 μ α . T {\displaystyle \mu \alpha .T} とその展開結果である T [ μ α . T / α ] {\displaystyle T[\mu \alpha .T/\alpha ]} は別の型であり、特殊な項構成 fold と unfold で識別され、これらの間で同型写像を構成する。正確に記せば、 fold : T [ μ α . T / α ] → μ α . T {\displaystyle {\mbox{fold}}:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T} と unfold : μ α . T → T [ μ α . T / α ] {\displaystyle {\mbox{unfold}}:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]} であり、これらは互いに逆関数である。 部分型付けにおいてよく使われる方法として Amber 規則があり、μX.S <: μY.T かどうかを判定するにあたり、X <: Y という仮定を置いた上で、S <: T であれば、μX.S <: μY.T とする、という判定方法である。Java は構造的型システムではないが、分かりやすくするために Java の表記方法を使うと、 class ListA { Integer value; ListA next;}class ListB { Object value; ListB next;} で、ListA <: ListB であるかの判定をするにあたり、X は ListA の内側で再帰的に使っている ListA を指し、Y は ListB の内側で再帰的に使っている ListB を指すので、X <: Y であるという仮定を置いて、残りの value の部分が Integer <: Object なので、ListA <: ListB であると判定する方法である。再帰型同士しか比較しなく、再帰型を内部で利用している場合はそれを展開したりしないので、部分型付けの判定が有限時間で終わることが分かる。Amber 規則で出来ることは、概ね名前的型システムに近い。書籍『型システム入門』の「21.11 同型再帰型の部分型付け」で解説されている。
※この「同型再帰型」の解説は、「再帰データ型」の解説の一部です。
「同型再帰型」を含む「再帰データ型」の記事については、「再帰データ型」の概要を参照ください。
- 同型再帰型のページへのリンク
