Loading article…
コンピュータサイエンスにおいて、多相再帰（ミルナー・マイクロフト型付け可能性またはミルナー・マイクロフト計算とも呼ばれる）とは、型パラメータが一定ではなく、再帰呼び出しごとに変化する再帰的なパラメトリック多相関数を指す。多相再帰の型推論は半単一化と同等であり、したがって決定不能であり、半アルゴリズムまたはプログラマが提供する型注釈の使用が必要となる。[ 1 ]
Haskellにおける以下のネストされたデータ型について考えてみましょう。
データNested a = a :<: ( Nested [ a ]) | Epsilon infixr 5 :<:ネストされた= 1 :<: [ 2 , 3 , 4 ] :<: [[ 5 , 6 ],[ 7 ],[ 8 , 9 ]] :<:イプシロンこのデータ型に対して定義された長さ関数は、再帰呼び出しにおいて引数の型がからに変化するため、多相的に再帰的になりますNested a。Nested [a]
length :: Nested a -> Int length Epsilon = 0 length ( _ :<: xs ) = 1 + length xsHaskellは通常、このように単純に見える関数の型シグネチャを推論しますが、ここでは型エラーを発生させずに省略することはできません。
型ベースのプログラム解析では、解析の精度を高めるために多相再帰が不可欠な場合が多い。多相再帰を採用しているシステムの注目すべき例としては、Dussart、Henglein、Mossinのバインディング時間解析[ 2 ]やTofte - Talpinの領域ベースのメモリ管理システム[ 3 ]などがある。これらのシステムは、式が既に基となる型システムで型付けされていることを前提としているため（必ずしも多相再帰を採用しているわけではない）、推論を再び決定可能にすることができる。
関数型プログラミングのデータ構造では、型エラーチェックを簡素化し、ツリーなどの従来型のデータ構造でメモリを大量に消費する厄介な「中間」一時的ソリューションの問題を解決するために、多相再帰がよく使用されます。以下の 2 つの引用文献で、岡崎 (pp. 144–146) は、多相型システムがプログラマのエラーを自動的に検出するHaskell の CONS の例を示しています。 [ 4 ]再帰的な側面は、型定義によって、最も外側のコンストラクタが単一の要素を持ち、2 番目がペア、3 番目がペアのペアなど、再帰的に続くことが保証され、データ型に自動エラー検出パターンが設定されることです。Roberts (p. 171) は、スタック フレームを表すクラスを使用するJavaの関連例を示しています。示されている例は、開始、一時、終了のネストされたスタック置換構造でスタックが多相再帰をシミュレートするハノイの塔問題のソリューションです。 [ 5 ]