/herp-technote/value restriction

generated at 2/15/2025, 6:41:24 PM
value restriction
#型システム

問題
非純粋･call by value･多相の3つが揃うとき大変なことが起こる｡

今､value restrictionのないML方言と参照セルとリストコンストラクタを用意する｡let多相があると､let-boundなものを多相にすることができる｡
ocamllet r : 'a list ref = ref [] in
......
 r は多相なリスト 'a list を持っているので 'a list ref  型になる｡さて､ r のリストの参照を更新していくわけだが
ocamlr := "hello" :: !r;
r := "world" :: !r;
 !r  では  string list ref  に型が特殊化されるが､  :=  左辺の  r は依然として 'a list ref 型である｡つまり…
ocamlr := true :: !r; (* エッ?! *)
このコードは型システムによって咎められない｡というのも右辺の r は利用されるまでは 'a list ref 型であり､ !r で初めて bool list ref になる｡したがってこの参照セルの中身は [true; "world"; "hello"]  となり､型エラーがランタイムに発生する可能性がある｡

弱い多相たそ
このように､型システムがあっても健全性が失われる悲しい事態を避けるために､弱い多相を入れる｡
ocamllet r : '_a list ref = ref [] in
......

 '_a  は一見してただの型変数だが､一度特殊化されるとソレ以降ずっと特殊化された(つまり単相な)型になる｡
ocamlr := "hello" :: !r;
(* ==> val r : _string_ list ref *)
したがって次のようなコードが続くと静的に型エラーで弾くことができる｡
ocamlr := true :: !r; (* Error: This expression has type bool but なんとかかんとか､つまりダメ *)

問題2
しかし何でもかんでも弱い多相にすると大変困る｡よくある例として id 関数を見てみる｡
ocamllet id : '_a -> '_a ...? = fun x -> x
コレが弱い多相になっちまうってぇと…
ocamllet s = id "string" in (* ==> id : string -> string (x_x) *)
let i = id 3 in (* Error: This expression has type int but idはstring -> stringだよ〜ん *)
......
まあ､とにかくダメですね｡

relaxed value restriction
ML､もう全部単相か…というお通夜ムードに対し､Jacques Garrigue氏が打開策を出した｡
簡単に述べると､ let で束縛される値(リテラル)の型変数､または式の型のcovariant positionに現れる型変数は多相性を回復して良いというものである｡
covariant positionとは､あまり理解してないけど､  ->  の右辺のことである｡
ocaml(* fun x -> x というリテラルに相当するので 'a -> 'a *)
let id x = x

(* リテラルではない､かつ (('a -> 'b) -> 'a list -> 'b list) に ある型'_aに特殊化されたid:'_a -> '_aが適用されるので *)
(** '_a list -> '_a list *)
let map_id = List.map id

(* fun l -> List.map id l というリテラルに相当し､ '_a -> '_a から多相性を回復して 'a -> 'a *)
let map_id' l = List.map id l

特に最後の例は､ map_id  の定義をeta conversionしたものと考えることができる｡

TypeScriptに関する残念なお知らせ
弊社でも利用しているTypeScriptは､ var  または  let  で定義した変数への代入を許している( var は使うなマジで)｡
typescriptconst × = 3;
x = 2; // 構文エラー
let y = 5;
y = 8; // OK

TSにおいて型変数は関数でしか利用できない｡ところで any  は考えないものとする｡
typescriptlet t = []; // 型変数を許さない(しanyなんて信じない)のでArray<なんとか>になる
t = [3, ...t]; // 型推論が働いてくれればtは Array<number>になる
t = ["aa", ...t]; // なので無事型エラー

call by value､多相のTypeScriptには参照セルがないので問題なかった｡
…わけではない｡ こちらをご覧ください｡https://github.com/microsoft/TypeScript/issues/31152

TypeScriptにおいては､ Object を参照セルとして扱うことができる｡これを利用すると､簡単に型エラーをランタイムに発生させることができる｡上記で問題となるコードを少し変えて見てみる｡
typescriptfunction ref<T>(f: (x: T) => T): () => { val: (x: T) => T } {
 const r = {val : f};
 return () => r;
};

const id = <T>(x: T) => x;
const r = ref(id);

const r1 = r<number>();
const r2 = r<string>();

r1.val = (x: number) => x + 1;

console.log(r2.val("ok") === "ok"); // ==> false
console.log(r2.val("ok") === "ok1"); // ==> true (!)

 r がクロージングしているオブジェクトを r1 と r2 が共有してしまっている｡したがって r1.val  に関数を代入すると r2.val  でも同じ関数を指すことになる｡なので r2.val("ok") とすると "ok" + 1  の結果が出てくるようになる｡幸い(?)なことに二項演算子 + は number => string => string  をオーバーロードしている(嘘)ので型エラーこそ起こらないが全く意味不明な文字列 "ok1" が生成され､バグの温床となることは容易に想像できる｡多相なオブジェクトには細心の注意を払う必要がある｡

この問題は､tsc 3.5.3で確認した｡

Reference
Garrigue, Jacques. "Relaxing the value restriction." International Symposium on Functional and Logic Programming. Springer, Berlin, Heidelberg, 2004.