是否有任何使用情况下此功能：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）

回答

相关问题