型推論、型再構築は静的型付け言語の記述を簡潔にしてくれる素晴らしい機能です。
型推論をするには単一化 (Unification) の概念を理解する必要があります。
この単一化を最初から型推論の文脈で理解しようとすると、なんだかややこしい話になるのは型推論の仕組みに苦しんでインターネット上の資料を探し回った経験がある方ならご存知でしょう。
操作的意味論や型理論で用いられる型付け規則でも単一化を使った図式が使われていますが、関数型言語やRustを使ってもパターンマッチはあるけど単一化は言語機能としてないので理解に苦しむことになります。
正規表現を理解するには、JavaScriptの正規表現リテラルを使って覚えるとネイティブ感が身につきます。
オブジェクト指向を理解するには、Java、RubyやPythonなどをつかうといいでしょう。
単一化が機能としてある言語処理系を使えば、単一化に付いてのネイティブ感がつくはずです。
単一化変数がある処理系を探すとあります。Prologです。
また、Prologか。Prologなんて、AIといえば機械学習の時代に古い。終わっている。と考える気持ちもわかります。
:-みたいな演算子使うのおかしいでしょ？関数がネストできない言語なんて、、、。
変数が大文字とか今どきの言語とは逆で古臭い。
様々なネガティブな気持ちが湧いてくるのはわかりますが、ちょっと待ってください。
今回は型推論で使われる単一化のネイティブ感を身につけるためにPrologの単一化変数を使うだけです。他の要素は扱いません。
インストール
Linux,WindowsのWSLで
apt install swi-prolog
Macなら
brew install swi-prolog
などコマンド１つでインストールできます。
SWI-Prologの使い方
% swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 9.0.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).
?-
swipl コマンドでインタプリタが起動します。
終了の仕方
?- halt.
halt. と入力するとhalt/0 述語が動いて終了できます。
ああうざいと ctrl+c を押すと
?- ^C
Action (h for help) ?
と表示されるので e を押すと終了できます。
単一化変数を使ってみる
では単一化変数を使ってみましょう。
?- A=1.
A = 1.
?- A=1,B=A.
A = B, B = 1.
?- A=[1,2],B=A.
A = B, B = [1, 2].
?- A=[1,2],B=A.
A = B, B = [1, 2].
ここまでは単なる代入できる変数と同じように思えます。
?- A=1,A=2.
false.
単一化変数は内容を入れ替えることができません。mutableなのかな？
パターンマッチもできます。
?- A=[1,2],[B,_]=A.
A = [1, 2],
B = 1.
?- A=[1,_],A=[_,2].
A = [1, 2].
mutableではないな。バインドされてない穴にうめることはできる。
ここからが単一化変数の凄いところです。
?- A=[1,2],A=[B,_].
A = [1, 2],
B = 1.
パターンマッチは１方向に対して飲みデータが移動しますが、単一化は双方向にデータが移動します。
左から右にデータが流れている点がパターンマッチより凄いところです。
型推論でも同じことが起きるわけですが、一般的に単一化変数はパターンマッチより凄いことがおきます。
?- [[1,2,3],[A]]=[B,[2]].
A = 2,
B = [1,2,3].
より双方向性がわかる例ですね。構造化されたデータも単一化でまとめられます。
?- A=B,B=1,C=D,D=A,B=C.
A = B, B = C, C = D, D = 1.
?- A=B,B=1,C=D,D=A,B=C,writeln(A).
1
A = B, B = C, C = D, D = 1.
Aは1になります。
まとめ
型推論で使われる単一化は難しく感じる概念です。
難しい概念は使ってみることでネイティブ感を身につけられます。
単一化変数をもつPrologを使えば単一化変数のネイティブ感を知識ではなく教養として身につけることができます。
単一化変数のネイティブ感を身につけると単一化は難しいことではなくなります。