我被要求寫出s k k結果的最簡單定義，其中
s= f g x -> f x (g x)
s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k = x y -> x
k :: p1 -> p2 -> p1
在終端中寫下:t s k k，可以得到。t -> t。
我認為s需要兩個函式--f和g.其中f需要t1和t2作為輸入并回傳t3。函式g將t1作為輸入并回傳t2，而x是t1。為什么t3是回傳型別？
我想我理解了函式k，你把x和y作為輸入，x的型別是輸出。當涉及到理解這兩個函式將如何共同形成s k k時，是否有一個共同的方法。
我也試著一步一步地輸入:t s k，得到的結果是(t3 -> t2) -> t3 -> t3，然而，這對我沒有太大的幫助:) 誰能給剛接觸Haskell的人解釋一下這個問題呢？
uj5u.com熱心網友回復：
如果fun :: a1 -> b和arg :: a2，那么應用fun arg :: b和a1 ~ a2（a1等于a2）。
s k k與(s k) k相同，因為函式應用關聯到了左邊。所以我們有一個應用s k：
s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k :: (p1 -> p2 -> p1)
s k :: (t1 -> t2) -> t1 -> t3
p1 ~ t1
p2 ~ t2
p1 ~ t3
注意，p1 ~ t1和p1 ~ t3，因此t1 ~ t3：
s k :: (t1 -> t2) -> t1 -> t1
在應用程式(s k) k中，發生了類似的事情；我將用質數'重命名型別變數，以表明這是k的型別的不同實體化：
(s k) :: (t1 -> t2 ) -> t1 -> t1
k :: (p1' -> p2' -> p1')
(s k) k :: t1 -> t1
t1 ~ p1'
t2 ~ p2' -> p1'
注意，當t1 -> t2與p1' -> p2' -> p1'統一時，等于p1' -> (p2' -> p1')，因為函式型別是右聯的，t2被等同于函式型別p2' -> p1'
結果，整個運算式的型別是t1 -> t1，或forall t1. t1 -> t1與ExplicitForAll。即使不知道這里的術語，也只有一個forall a. a -> a型別的函式(這是總的)，那就是id。事實上，s k k只是實作身份函式的一種迂回方式，因為對于我們給它的任何X，它都回傳X：
s k k X.
( f g x -> f x (g x)) k kX
( g x -> k x (g x)) kX
( x -> k x (k x)) X
k X ( k X)
( x y -> x) X (k X)
( y -> X) ( k X)
X)
第一個k選擇了X，而第二個k的應用被忽略了。這就是為什么第二次使用k的型別變數（p1'和p2'）都沒有出現在結果型別中。
uj5u.com熱心網友回復：
那么我們從他們的定義中知道
s k k x = k x （k x） = x
-- s = f g x -> f x (g x)
-- s k k x = k x (k x)
-- k = x y -> x
-- k x y = x
-- k x (k x) = x
因此，
s k k = x -> x
因此它的型別是
a -> a
GHCi同意（正如你已經注意到的）：
> :t s k k
s k k :: t3 -> t3
至于你問到的s中的型別，
s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
s = f g x -> f x (g x)
s f g x = f x (g x)
--
-- x :: t1
-- g :: t1 -> t2
-- g x :: t2
-- x :: t1
-- f :: t1 -> t2 -> t3
-- f x (g x) :: t3
只需遵循應用程式中型別推理的最基本規則，
x :: A x :: a
f :: A -> B f :: b -> c
------------------- --------------
f x :: B f x :: c , a ~ b
這類似于邏輯學中的Modus Ponens，"如果我們有A，并且A意味著B，那么B也成立"。
"如果我們有A，并且A意味著B，那么B也成立。
如果你想從s和k的型別中得到這一點，一個類似的圖表也可以用于此：
s :: (a -> b -> c) -> (a -> b ) -> a -> c
k :: x -> y -> x
------- a~x, b~y, c~x => c~x~a -------------------
s k :: (a -> b ) -> a -> a
k :: x2 -> y2 -> x2
---------------------- a~x2, b~（y2 -> x2） ---------
s k k :: a -> a
（你可以看到你所問的型別，s k :: (a->b)->a->a，那里）。) 在這里，你可以看到型別的統一是 "一步一步 "完成的，但這兩個統一很可能是一起完成的，
s :: (a -> b -> c) -> (a -> b ) -> a -> c
k :: x -> y -> x
k :: x2 -> y2 -> x2
------- a~x, b~y, c~x => c~x~a -------------------
---------------------- a~x2, b~(y2 -> x2) ---------
s k k :: a -> a
最終的結果當然是一樣的。無論我們是一次性閱讀上圖還是分階段閱讀，它都是同一個圖。詛咒是很好的，它有效。既然它有效，當你已經將一個東西應用到兩個其他東西上時，你就不需要關心分階段的部分應用。除了作為一種精神上的練習。
沒有什么比這更重要的了。
對于所有這些臨時型別，其實沒有什么可說的。你只需將它們一個一個地寫在另一個下面，注意在不同的呼叫中一致地重命名變數以避免被捕獲，注意由此產生的等價關系并使用它們來簡化所產生的型別。
最后要注意的是，s k s和s k (s k)等也可以用于相同的目的。幾乎，就像($)是幾乎與id相同。
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/316904.html
標籤：