エイプリールではないユニフィケーションをしてる話
とくに嘘なネタはないので書いてません。面白くなくて申し訳ないんですけど。
ここのところ日記の更新出来てません。
型推論の基本はパターンマッチングとユニフィケーションです。
実はパターンマッチングは理解していたのだけど、ユニフィケーションは理解していなかったので、最近よく使っているPHPでunifyを書いてみてます。
参考: http://www.gesource.jp/weblog/?p=654
パターンマッチングは片方の式にだけ変数を入れる事が出来ます。
対してユニフィケーションでは、マッチする式の両方に変数が入れられます。
ここが大きく異なるところです。
そして、変数から変数への伝搬も起こる事があり得ます。
ここらへんの実装が難しいところのようです。
教科書的な説明が出来るといいんですけど、まだ全然出来てないので他のソースもいくつか読んで、サクっと作れるようになろうと思っています。
なんとなくは、分かるんですよ。Scalaのコードも読んだりはしてるし、何となく分かる。でも、完全に分かりたい。それにはまだ時間がかかりそうです。
まず、パターンマッチが出来て、それをユニフィケーション出来るように拡張していく。で、問題あるので対策した結果、ちゃんとうまく行くようになる。で、効率が悪いとか、immutableな環境で計算する為に、substとか使う。とかいう発展させていくというストーリーが欲しいのでそれを作れて、ダダダダダっとキーボード打ちまくって、実装出来るようになれれば、きっと本当に理解していると言えると思うので、とにかく何回も作ってみようと思ってます。
<?php class unify { static $vars = array(); static $buf1 = array(); static $buf2 = array(); static function apply($str1, $str2) { self::$vars = array(); echo $str1."\n"; echo $str2."\n"; // 各々トークンに分ける self::$buf1 = preg_split("/\\s/", $str1); self::$buf2 = preg_split("/\\s/", $str2); // 数が異なったら失敗 if (count(self::$buf1) != count(self::$buf2)) { return false; } foreach (self::$buf1 as $i => $b1) { if (!self::t_match($b1, self::$buf2[$i])) return false; } var_export(self::$vars); return true; } static function t_match($t1, $t2) { if ($t1 == $t2) return true; if (is_var($a) && !is_var($b)) return self::var_match($a, $b); if (is_var($b)) return self::var_match($b, $a); if (is_var($a)) return self::var_match($a, $b); return false; } static function var_match($vt, $t) { if (isset(self::$vars[$vt])) return ($t == self::$vars[$vt]); self::replace_buf($vt, $t); if (in_array($vt, self::$vars)) self::replace_vars($vt, $t); self::$vars[$vt] = $t; return true; } static function replace_buf($s, $d) { foreach (self::$buf1 as &$b) if ($s == $b) $b = $d; foreach (self::$buf2 as &$b) if ($s == $b) $b = $d; } static function replace_vars($s, $d) { foreach (self::$vars as $k => $v) if ($s == $v) self::$vars[$k] = $d; } } function unify($a, $b) { return unify::apply($a, $b); } function is_var($str) { return substr($str,0,1)=="?"; } function p($str) { var_export($str); echo "\n"; } p(unify("Takayuki", "Takayuki")); p(unify("Takayuki", "Takoyuki")); p(unify("?x am Takayuki", "I am Takayuki")); p(unify("?x is ?x", "a is b")); p(unify("?x is ?x", "a is a")); p(unify("?x is a", "b is ?y")); p(unify("?x is a", "?y is ?x"));