プロシージャの実装に基づいてプロシージャのHM型を派生させるには？

Question

これら2つの手順（JavaScriptで書かれています）とhellipを指定すると、

// comp :: (b -> c) -> (a -> b) -> (a -> c) 
const comp = f=> g=> x=> f (g (x)) 

// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d) 
const comp2 = comp (comp) (comp) 

私の質問は、私たちがcompの実装を知っている場合、それは簡単＆hellipだの実装

---

'compを参照なしのHindley-Milner Type' comp2を導出する方法です。展開モデル＆hellipに到達するためには、評価全体を通じて置換モデルを使用できます。

comp (comp) (comp) 
= (f => g => x => f (g (x))) (comp) (comp) 
= x => comp (comp (x)) 
= y => comp (comp (y)) 
= y => (f => g => x => f (g (x))) (comp (y)) 
... keep going until ... 
= f=> g=> x=> y=> f (g (x) (y))

Ring-a-ding。拡大評価はcomp2のタイプと一致します。誰も感銘を受けません。

// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d) 
const comp2 = f=> g=> x=> y=> f (g (x) (y)) 

しかし、私たちが唯一compのタイプを知っていたし、はないその実装をご存知でしたか？もし型を決定するためにコードを評価する代わりに、comp2の型になるようにcompの型の置換/評価を実行できましたか？

---

この場合、問題はもっと難しくなります。 （少なくとも私のために）

ちょっと道がありますか？これは何ではないalgebraic data typesはすべてについてですか？

---

のは私の質問を明確にするために簡略化した例を見てみましょう：私たちはaddとmap＆hellipのような機能を持っている場合。

// add :: Number -> Number -> Number 
// map :: (a -> b) -> [a] -> [b] 

我々はmapとaddを使用して関数を定義したい場合は、我々はタイプを把握できたが、体系

// add :: Number -> Number -> Number 
// map :: (a -> b) -> [a] -> [b] 

// add6 :: Number -> Number 
let add6 = add (6) 

// mapAdd6 :: [Number] -> [Number] 
let mapAdd6 = map(add6) 

addまたはmapの実装を知らなくても、これは本当に強力であることので実装を掘り進むことなく、あなたが作っていなかったコードを推論することができます（それだけ）

comp2例でそれをやろうとしたときにしかし、私は、我々が知っているか見てみましょうMILNER

Answer 1

をヒンドリーかたかなり速い

// comp :: (b -> c) -> (a -> b) -> (a -> c) 

// comp2 :: ?? 
const comp2 = comp (comp) (comp) 

// initial type 
(b -> c) -> (a -> b) -> (a -> c) 

// apply to comp once ... ??? 
[(b -> c) -> (a -> b) -> (a -> c)] -> (a -> b) -> (a -> c) 

// apply the second time ... ??? 
[(b -> c) -> (a -> b) -> (a -> c)] -> [(b -> c) -> (a -> b) -> (a -> c)] -> (a -> c) 

// no... this can't be right 

を動けなくなります。さんはcomp2を見てみましょう "単独での実装：

comp2 = comp comp comp 

をとのがcomp考えるの型シグネチャ：今すぐ

comp :: (b -> c) -> (a -> b) -> (a -> c) 

は、comp2の結果は2つに適用されるcompの結果になるだろう引数は、comp型シグネチャの右端にあります。したがって、タイプa -> cのcomp2は、aとcはまだわかりません。

しかし、わかります。手動でをタイプ（同じタイプにする必要があることがわかっている）に統一して手動で処理することができます。具体的なタイプの既知タイプ変数をに置き換えます。 2つの引数は両方ともcompですが、それぞれ異なるタイプ（とa -> b）を持つ必要があります。のは、もう少し明確ことを確認するために、いくつかのタイプの注釈を追加してみましょう：

comp2 = (comp (comp :: b -> c) 
       (comp :: a -> b)) 

我々は最初bとcが何であるかを決定するためにcompの種類とb -> cを統一しようとすることができますが、我々はいくつかのアルファを行う必要があります

：

b   -> c 
(b1 -> c1) -> (a1 -> b1) -> (a1 -> c1) 

b = b1 -> c1 
c = (a1 -> b1) -> (a1 -> c1) 

次に、我々はタイプa -> bで統一し、第二引数で同じことを行うことができます。私たちの変数名が衝突しないように名前を変更

お待ちください！同じタイプの変数bには2つの異なる定義があるので、それらも統一する必要があります。のは、これらの2つのタイプのために同じプロセスを実行してみましょう：

a -> c             | type of comp2, from the return type of comp 
(b2 -> c2) -> c          | substituting the definition of a 
(b2 -> c2) -> (a1 -> b1) -> (a1 -> c1)     | substituting the definition of c 
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> c1)   | substituting the definition of b1 
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> (a2 -> c2)) | substituting the definition of c1 
(b2 -> c2) -> (a1 -> a2 -> b2) -> a1 -> a2 -> c2  | removing unnecessary parentheses 
(c -> d) -> (a -> b -> c) -> a -> b -> d    | alpha renaming 

：

b1   -> c1 
(a2 -> b2) -> (a2 -> c2) 

b1 = a2 -> b2 
c1 = a2 -> c2 

今、私たちはcomp2のために与えた元の型に戻る、私たちは完全な形で終わるために置換のシリーズを実行することができます

これは、手動で指定したタイプと同じであることがわかります。