组合子的类型签名与其等价的Lambda函数的类型签名不匹配 [英] The type signature of a combinator does not match the type signature of its equivalent Lambda function

问题描述

考虑这个组合：

  S（SK）
  

$ b $ p将其应用于参数XY：

$ p $ S（SK）XY


合约到：

  XY 
  

我将S（SK）转换为相应的Lambda项并得到这个结果：

 （\xy  - > xy）
  

我使用Haskell WinGHCi工具来获取（\xy - > xy）的类型签名并返回：

 （t1  - > t） - > t1  - > t 
  

这对我很有意义。

接下来，我使用WinGHCi来获取s（sk）的类型签名并返回：

 （（t  - > t1）→t）→> （t  - > t1） - > t 
  

这对我没有意义。为什么类型签名不同？

注意：我将s，k和i定义为：

<$ p $ （\ f - > - > fx（gx））
k =（\ ax - > a）
i =（\ f - > f）

解决方案

感谢所有回答我的问题的人。我研究了你的回答。为了确保我了解我所学到的知识，我已经为自己的问题写下了自己的答案。如果我的回答不正确，请告诉我。

我们从 k 和 s ：

  k :: t1  - > t2  - > t1 
 k =（\ a x  - > a）
 
 s ::（t3  - > t4  - > t5） - > （t3→t4）→> t3  - > t5 
s =（\ fgx  - > fx（gx））
  

确定（sk）的类型签名。

回顾 s


  s =（\ fgx  - > fx（gx））
  



代替 f
<$ p $（$ \\ cg） p> （\ gx - > kx（gx））


重要 g和x的类型必须与 k 的类型签名保持一致

回想一下， k 有这样的签名：

  k :: t1 - > t2  - > t1 
  

所以，对于这个函数定义 kx（gx）我们可以推断：

• x 的类型是 k 的第一个参数类型，即类型 t1 。




• k 的第二个参数的类型是 t2 ，所以（gx）必须是 t2 。

我们已经确定的类型是 t1 。因此，（gx）的类型签名是（t1 - > t2）。



• k 的结果类型为 t1 ，所以结果（sk）是 t1 。

因此，（\ gx - > kx（gx））的类型签名是这样的：

 （t1  - > t2） - > t1  - > t1 
  

接下来， k 定义为始终返回它的第一个参数。所以这个：

  kx（gx）
  

与此合约：

  x 
  
 
 
 
而且： 
 
 
 （\gx  - > kx（gx））
  
与此合约： 
 
 
 （\ gx  - > x）
  
 
 
 <好吧，现在我们已经计算出了（sk）：
  sk ::（t1→t2）→> t1  - > t1 
sk =（\ gx  - > x）
  
现在让我们确定类型签名 s（sk）。
 
 
 
我们以同样的方式进行。 
 
 
回顾 s 的定义： 
 
 
  s =（\ fgx  - > fx（gx））
  
替换（ sk）为 f 结果为（\ fgx  - > fx（gx））签约到： 
 
 
 （\ gx  - >（sk）x（gx））
  
 重要  g 和 x 必须与（sk）的类型签名保持一致
 
 
 
  sk ::（t1→t2）→> t1  - > t1 
  
所以，对于这个函数定义（sk）x（gx）我们可以推断出： 
 
 
 
 
  x 是（sk）的第一个参数的类型，它是类型（t1  - > t2）  
 
 
 
 （sk）的第二个参数的类型是 t1 ，因此（gx）的结果必须是 t1 。  
           ，我们已经确定了类型（t1  - > t2）。 
因此，（gx）的类型签名是（（t1  - > t2） - > t1） 
 
 （sk）的结果类型为 t1 ，因此 s（sk）的结果是 t1 。
所以，类型签名（\ gx  - >（sk）x（gx）） 是： 
 
 
 （（t1  - > t2） - > t1） - > （t1→t2）→> t1 
  
之前我们确定 sk 有这个定义：
 （\ gx  - > x）
  
 
 
也就是说，它是一个接受两个参数并返回第二个参数的函数。
 
 
 
因此，这个
 （sk）x（gx）
  
与此合约： 
 
 
 （gx）
  
  
 
 $ p 
 $ p $ （\gx - >（sk）x（gx））
  
与此合约：
 （\ gx  - > gx）
  
好的，现在我们已经计算出 s（sk）。
  s（sk）::（（t 1  - > t 2） - > t 1） - > （t1→t2）→> t1 
s（sk）=（\ gx  - > gx）
  
最后，比较 s（sk）的类型签名以及此函数的类型签名： 
 
 
   
 <$ c $ 
 
 
  p ::（t1  - > t） - > t1  - > t 
  
  p 和 s（sk）具有相同的定义（\ gx  - > gx），为什么它们有不同的类型签名？
 
 
 
原因是 s（sk）的类型签名不同于 p 在 p 没有限制。我们看到（sk）中的 s 被限制为与 k ，并且 s（sk）中的第一个 s 被限制为一致与类型签名（sk）。因此， s（s k）的类型签名由于其参数而受到约束。即使 p 和 s（sk）具有相同的定义， g 和 x 不同。
 
Consider this combinator:
S (S K)
Apply it to the arguments X Y:
S (S K) X Y
It contracts to:
X Y
I converted S (S K) to the corresponding Lambda terms and got this result:
(\x y -> x y)
I used the Haskell WinGHCi tool to get the type signature of (\x y -> x y) and it returned:
(t1 -> t) -> t1 -> t
That makes sense to me.

Next, I used WinGHCi to get the type signature of s (s k) and it returned:
((t -> t1) -> t) -> (t -> t1) -> t
That doesn't make sense to me. Why are the type signatures different?

Note: I defined s, k, and i as:
s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)

解决方案
Thanks to all who responded to my question. I have studied your responses. To be sure that I understand what I've learned I have written my own answer to my question. If my answer is not correct, please let me know.

We start with the types of k and s:
   k  :: t1 -> t2 -> t1 
   k  =  (\a x -> a) 

   s  :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
   s  =  (\f g x -> f x (g x)) 
Let's first work on determing the type signature of (s k).

Recall s's definition:
s = (\f g x -> f x (g x))
Substituting k for f results in (\f g x -> f x (g x)) contracting to: 
(\g x -> k x (g x))
Important The type of g and x must be consistent with k's type signature.

Recall that k has this type signature:
   k :: t1 -> t2 -> t1
So, for this function definition k x (g x) we can infer:


The type of x is the type of k's first argument, which is the type t1.
The type of k's second argument is t2, so the result of (g x) must be t2. 
g has x as its argument which we've already determined has type t1. So the type signature of (g x) is (t1 -> t2).
The type of k's result is t1, so the result of (s k) is t1.


So, the type signature of (\g x -> k x (g x)) is this:
   (t1 -> t2) -> t1 -> t1
Next, k is defined to always return its first argument. So this:
k x (g x)
contracts to this:
x
And this:
(\g x -> k x (g x))
contracts to this:
(\g x -> x)
Okay, now we have figured out (s k):
   s k  :: (t1 -> t2) -> t1 -> t1 
   s k  =  (\g x -> x)
Now let's determine the type signature of s (s k).

We proceed in the same manner.

Recall s's definition:
s = (\f g x -> f x (g x))
Substituting (s k) for f results in (\f g x -> f x (g x)) contracting to: 
(\g x -> (s k) x (g x))
Important The type of g and x must be consistent with (s k)'s type signature.

Recall that (s k) has this type signature:
   s k :: (t1 -> t2) -> t1 -> t1
So, for this function definition (s k) x (g x) we can infer:


The type of x is the type of (s k)'s first argument, which is the type (t1 -> t2).
The type of (s k)'s second argument is t1, so the result of (g x) must be t1. 
g has x as its argument, which we've already determined has type (t1 -> t2). 
So the type signature of (g x) is ((t1 -> t2) -> t1).
The type of (s k)'s result is t1, so the result of s (s k) is t1.


So, the type signature of (\g x -> (s k) x (g x)) is this:
   ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1
Earlier we determined that s k has this definition:
   (\g x -> x)
That is, it is a function that takes two arguments and returns the second.

Therefore, this:
   (s k) x (g x)
Contracts to this:
   (g x)
And this:
   (\g x -> (s k) x (g x))
contracts to this:
   (\g x -> g x)
Okay, now we have figured out s (s k).
   s (s k)  :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
   s (s k)  =  (\g x -> g x)
Lastly, compare the type signature of s (s k) with the type signature of this function:
   p = (\g x -> g x)
The type of p is:
   p :: (t1 -> t) -> t1 -> t
p and s (s k) have the same definition (\g x -> g x) so why do they have different type signatures?

The reason that s (s k) has a different type signature than p is that there are no constraints on p. We saw that the s in (s k) is constrained to be consistent with the type signature of k, and the first s in s (s k) is constrained to be consistent with the type signature of (s k). So, the type signature of s (s k) is constrained due to its argument. Even though p and s (s k) have the same definition the constraints on g and x differ.

                        
这篇关于组合子的类型签名与其等价的Lambda函数的类型签名不匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！