是否有任何使用情況下此功能：FOO ::（B - > C） - >（A - > B） - >（A - > C）

-1

對於這個功能：是否有任何使用情況下此功能：FOO ::（B - > C） - >（A - > B） - >（A - > C）

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

取自http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

這是一個沒有實際用途的功能嗎？由於(b -> c)不能構造，除非類型c是該函數中的另一個輸入參數？

和(a -> b) -> (a -> c)相同：b & c不是這些函數的輸入參數。

這個函數有沒有用例？

來源

2015-05-15 blue-sky

什麼意思是無意義的？它是兩個功能的組合。順便說一句，鏈接文章明確指出。 – kraskevich

@kraskevich ive更新了問題。 –

如果問題是關於在實踐中使用函數組合，這裏是一個小例子。我們假設我們想寫一個函數，它是數字列表中所有元素的平方和。我們怎麼能這樣做？那麼，我們可以寫一些如：squareSum xs = sum (map (^2)) xs。但是我們也可以使用函數組合來代替：squareSum = sum . map (^2)（我使用.代替foo來代替foo，但它並不重要）。這個例子展示了一個使用函數組合得到的函數（至少在某種意義上它是可編譯和正常工作的）。當我們需要編寫多個函數（可能部分應用）時，函數組合的好處變得更加明顯。

來源

2015-05-15 10:41:12 kraskevich

功能b -> c可以構造 - 因爲b和c可以是任何類型，那麼任何函數都可以與它兼容。然而，功能foo不能本身（明智地）構造這樣的功能，因爲它不知道b和c。這是一個很大的好處，因爲它大大減少了功能foo的可能實現的數量。這就是所謂的parametricity

此功能是功能複合算(.)類型：

來源

2015-05-15 10:24:27 Lee

*它大大減少了函數foo的可能實現的數量* - 是否存在與常規函數不同的實現* 1 *的實現？ –

'let x = x in x';） –

@BartekBanachewicz - 我不這麼認爲，我敢肯定有人比我更有知識可以證明它。 – Lee

我只是想編造(.)可能是在任何好的Haskell代碼庫中使用最多的前三個函數。這當然是在我的代碼中。

由於積分文字，前三個中的另外兩個是由編譯器插入的fromInteger的隱式調用，以及從do表示式對(>>=)的隱式調用。而後者在深層次上與(.)的操作相同，只是數值略有不同的形狀。

來源

2015-05-15 12:52:31 Carl

補充其他的答案，讓我嘗試證明，只有一個（總）函數

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

或者，換句話說，即foo = (.)。通過外延性，我們要證明

foo f g n = f (g n)

其中f,g,n是由foo簽名授權的類型abritrary值。

f :: b -> c 
g :: a -> b 
n :: a

我們從相關的自由定理，它可以是automatically generated on the web開始：

forall t1,t2 in TYPES, R in REL(t1,t2). 
forall t3,t4 in TYPES, S in REL(t3,t4). 
    forall t5,t6 in TYPES, R1 in REL(t5,t6). 
    forall p :: t3 -> t5. 
    forall q :: t4 -> t6. 
    (forall (x, y) in S. (p x, q y) in R1) 
    ==> (forall r :: t1 -> t3. 
      forall s :: t2 -> t4. 
      (forall (z, v) in R. (r z, s v) in S) 
      ==> (forall (w, u) in R. 
        (foo p r w, foo q s u) in R1))

讓我們通過專門它簡化了這個巨大的公式。我們挑選：

t1 = a t2 =() 
t3 = b t4 =() 
t5 = c t6 =()

，我們選擇關係如下：

R = { (n  ,()) } which is indeed in REL(t1,t2) = REL(a,()) 
S = { (g n  ,()) } which is indeed in REL(t3,t4) = REL(b,()) 
R1= { (f (g n) ,()) } which is indeed in REL(t5,t6) = REL(c,())

自由定理變成：

forall p :: b -> c. 
    forall q ::() ->(). 
    (forall (x, y) in S. (p x, q y) in R1) 
    ==> (forall r :: a -> b. 
      forall s ::() ->(). 
      (forall (z, v) in R. (r z, s v) in S) 
      ==> (forall (w, u) in R. 
        (foo p r w, foo q s u) in R1))

採摘p = f和q = id我們得到，由S和R1定義：

 (forall x = g n, y =() . f x = f (g n) /\ y = id y) 
    ==> (forall r :: a -> b. 
      forall s ::() ->(). 
      (forall (z, v) in R. (r z, s v) in S) 
      ==> (forall (w, u) in R. 
        (foo f r w, foo id s u) in R1))

頂層含義的前提是真實的，所以我們解決它。我們現在選擇r = g和s = id。我們得到的，由r1和R定義：

  (forall z = n, v =() . g z = g n , id v =()) 
      ==> (forall (w, u) in R. 
        (foo f g w, foo id id u) in R1)

我們能排出的真正前提。此外，我們可以選擇w = n和u =()。我們最終獲得：

    foo f g n = f (g n) /\ foo id id u =()

Q.E.D.

來源

2015-05-16 11:47:45 chi

是否有任何使用情況下此功能：FOO ::（B - > C） - >（A - > B） - >（A - > C）

回答

相關問題