'（。）の種類を手動で推論する方法。 （。）。 （。） '？スライド上のエドワードKmettの話<a href="https://youtu.be/cefnmjtAolY?t=496" rel="nofollow">Lenses, Folds, and Traversals</a>で

Question

、「パワーがドットである」、彼は(.) . (.) . (.)のタイプは

(a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b

であることを示している私は、GHCiの中にその型を示すことによって、それを見ることができます。しかし、なぜか知りたいのですが。 (.) . (.)と(.) . (.) . (.)から(.)からのパラメータの定期的な変化のパターンがありますなぜ私が理解したいのですが、他の事は次のとおりです。

(.)    :: (a -> b) -> (c ->   a) -> c ->   b 
(.) . (.)  :: (a -> b) -> (c -> d ->  a) -> c -> d ->  b 
(.) . (.) . (.) :: (a -> b) -> (c -> d -> e -> a) -> c -> d -> e -> b 

P.S.関数定義を(.) . (.)に拡張して、自分自身で(.) . (.)を解決しようとしました。私は(.)の定義を適用した後だ：

\x y z t -> x ((y z) t) 

だから私はタイプを推測さ：

x :: a -> b 
y :: c -> d -> a 
z :: c 
t :: d 

私は(.) . (.) . (.)に失われてしまったが。これが手動型推論を行う正しい方法であるかどうかはわかりません。機能付き

Answer 1

、

instance Functor ((->) r) where 
    -- fmap :: (a -> b) -> f a -> f b 
    --   (a -> b) -> (r -> a) -> (r -> b) 
    fmap   p   q   x = p (q x) -- fmap = (.) 

ので、あなたが実際に持っていることはfmap . fmap . fmapです：

(a -> b) -> (c -> (d -> (e -> a))) -> (c -> (d -> (e -> b))) ~ 
(a -> b) -> (c -> d -> e -> a) -> (c -> d -> e -> b)  

ある

fmap    :: (a -> b) -> f  a -> f  b 
fmap . fmap  :: (a -> b) -> f (g a) -> f (g b) 
fmap . fmap . fmap :: (a -> b) -> f (g (h a)) -> f (g (h b)) 

なぜfmap . fmap :: (a -> b) -> f (g a) -> f (g b)はありますか？機械タイプの導出はすべて型変数の置換と一貫した名前の変更に関するものです。もっと見るhereまたはhere。

Answer 2

(.) . (.) . (.)は二段階で削減：最初の周りの括弧なしのドットを減らす：

((.) . (.) . (.)) f = (.) ((.) ((.) f)) 
        = (.) ((.) (f .)) 
        = (.) ((f .) .) 
        = ((f .) .) .) 

を二だから、最初にあなたがn - 1ドットを使用して括弧でnドットを構成する残りの表現

((f .) .) .) g = ((f .) .) . g 
       = \x -> ((f .) .) (g x) 
       = \x -> (f .) . g x 
       = \x y -> (f .) (g x y) 
       = \x y -> f . g x y 
       = \x y z -> f (g x y z) 

を減らします。次に、この構造を関数f :: a -> bとgに適用し、それぞれのドットがgが受け取る引数に対応します。そのためパターンがあります：括弧内の各ドットはgの1つの引数を処理し、このドットを構成する別のドットが必要ですすべて前のすべての縮小の後、式は

\x1 x2 ... xn -> f (g x1 x2 ... xn) 

になり、そのタイプは明らかです。

---

一つの良いところは、

open import Function renaming (_∘′_ to _∘_) using() 

_% = _∘_ 

postulate 
    a b c d e : Set 
    f : a -> b 
    g : c -> d -> e -> a 

fg : c -> d -> e -> b 
fg = f % % ∘ g 

の代わりに、((f .) .) . g（コードがAgdaである）我々は書くことができます後置演算子を持っているならばということです。