プログラミング言語の基礎概念オンライン演習

100問突破!
飽きっぽい私としてはめずらしいことよ。
単純型システムに入った時、intのつもりで、natと書いてしまっており、なんで通らないんじゃーと一時間くらい無駄にした。

97問目
k2の型は int->???->int のような形になるけど、真ん中に何を入れても成立した。
OCaml本体はどないなってんのやろか。

Cでも関数宣言してないでコンパイルすると、とりあえずint型を返す関数と仮定しまーす。みたいなワーニングが出るし、矛盾が起きない限りわりとどうでもいいのかもしれない。

(*
TYPE_S=(int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int  
TYPE_K1=int -> (bool -> int) -> int
TYPE_K2=int -> bool -> int
*)
|- let s = fun f -> fun g -> fun x -> f x (g x) in
   let k1 = fun x -> fun y -> x in
   let k2 = fun x -> fun y -> x in
  s k1 k2 : int -> int by T-Let {
	|- fun f -> fun g -> fun x -> f x (g x) : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int by T-Fun {
		f : int -> (bool -> int) -> int |- fun g -> fun x -> f x (g x) : (int -> bool -> int) -> int -> int by T-Fun {
			f : int -> (bool -> int) -> int, g : int -> bool -> int |- fun x -> f x (g x) : int -> int by T-Fun {
				f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- f x (g x) : int by T-App {
					f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- f x  : (bool -> int) -> int by T-App {
						f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- f : int -> (bool -> int) -> int by T-Var { };
						f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- x : int by T-Var { };
					};
					f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- g x  : bool -> int by T-App {
						f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- g : int -> bool -> int by T-Var { };
						f : int -> (bool -> int) -> int, g : int -> bool -> int, x : int |- x : int by T-Var { }
					}
				}
			}
		}
	};
	s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int |- let k1 = fun x -> fun y -> x in let k2 = fun x -> fun y -> x in s k1 k2 : int -> int by T-Let {
		s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int |- fun x -> fun y -> x : int -> (bool -> int) -> int by T-Fun {
			s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, x : int |- fun y -> x : (bool -> int) -> int by T-Fun {
				s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, x :int, y : bool -> int |- x : int by T-Var { }
			}
		};
		s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int |- let k2 = fun x -> fun y -> x in s k1 k2 : int -> int by T-Let {
			s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int |- fun x -> fun y -> x : int -> bool -> int by T-Fun {
				s : (int -> (bool -> int) -> int) -> (int -> bool -> int) ->
				int -> int, k1 : int -> (bool -> int) -> int, x : int |- fun y -> x : bool -> int by T-Fun {
					s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, x : int, y : bool |- x : int by T-Var { }
				}
			};
			s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, k2 : int -> bool -> int |- s k1 k2 : int -> int by T-App {
				s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, k2 : int -> bool -> int |- s k1 : (int -> bool -> int) -> int -> int by T-App {
					s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, k2 : int -> bool -> int |- s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int by T-Var { };
					s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, k2 : int -> bool -> int |- k1 : int -> (bool -> int) -> int by T-Var { }
				};
				s : (int -> (bool -> int) -> int) -> (int -> bool -> int) -> int -> int, k1 : int -> (bool -> int) -> int, k2 : int -> bool -> int |- k2 : int -> bool -> int by T-Var { }
			}
		}
	}
}

一度評価された値は変更されないから、簡単なマクロのような文字列置換でわりとサクサク進められることが分かった。