有趣的类型g x = ys其中ys = [x] ++ filter（curry g x）ys？ [英] Type of fun g x = ys where ys = [x] ++ filter (curry g x) ys?

问题描述

我试图理解为什么类型的fun gx = ys其中ys = [x] ++ filter（curry gx）ys 是（（a，a） - > Bool） - > a - > [a] 。

据我所知：

filter ::（a - > Bool） - > [a] - > [a] 和 curry ::（（a，b） - > c） - > a - > b - > c

但是我不明白如何继续。

解决方案

下面的方法不一定是最简单或最快的方法，但它是比较系统的。 严格来说，您正在寻找

  \g  - > （\ x  - > let ys =（++）[x]（filter（curry gx）ys）in ys）
  

（ let 和其中是等价的，但有时使用< code $> $ > ），给定类型



  filter ::（a  - >布尔） - > [a]  - > （a，b） - > c） - > a  - > b  - > c 
  

不要忘记您还在使用



 （++）:: [a]  - > [a]  - >我们首先看一下语法树中最深的部分：
 [b]   





 咖喱gx 
  

我们有 g 和 x ，我们之前从未见过，所以我们假设他们有一些类型：



  g :: t1 
x :: t2 
  

我们还有咖喱。在这些函数发生的每一点上，类型变量（ a ， b ， c ）可以有不同的专门化，所以每次使用这些函数时都用新名称替换它们是一个好主意。此时， curry 具有以下类型：



  curry :: （（a1，b1）→> c1）→> a1  - > b1  - > c1 
  

然后我们只能说咖喱gx 如果以下类型可以统一：



  t1〜（（a1，b1） - > c1） - 因为我们应用curry to g 
 t2〜a1  - 因为我们将（咖喱克）应用于x 
  

那么假设

  g ::（（a1，b1） - > c1）
x： ：a1 
 --- 
咖喱gx :: b1  - > c1 
  

让我们继续：



  filter（curry gx）ys 
  

我们看到 ys ，所以让我们暂时将它保持在 ys :: t3 。我们还必须实例化 filter 。所以在这一点上，我们知道



  filter ::（a2  - > Bool） - > [a2]  - > [a2] 
 ys :: t3 
  

现在我们必须匹配 filter 的参数：

  b1  - > c1〜a2  - > Bool 
 t3〜[a2] 
  

第一个约束可以分解为

  b1〜a2 
 c1〜Bool 
  

我们现在知道以下内容：



  g ::（（a1，a2） - > Bool）
x :: a1 
 ys :: [a2] 
 --- 
 filter（咖喱gx）ys :: [a2] 
  

让我们继续。



 （ ++）[x]（filter（curry gx）ys）
  

我不会花太多钱在解释 [x] :: [a1] 时，我们来看看（++）的类型：

 （++）:: [a3]  - > [a3]  - > [a3] 
  

我们得到以下限制：



  [a1]〜[a3]  -  [x] 
 [a2]〜[a3]  -  filter（咖喱gx）ys 
  
 
 $ b 
因为这些限制可以被减少到
 
 
  a1〜a3 
 a2〜a2 
  
我们将所有这些 a 的 a1 ： 
 
 
  g ::（（a1，a1） - > Bool）
x :: a1 
 ys :: [a1] 
 --- 
（++） [x]（filter（curry gx）ys）:: [a1] 
  
现在，我们会忽略 ys '类型的泛化，并将注意力集中在 
 
  \\ \\ x  - >让ys 
中的{{ -  ...  - }}  
我们知道我们需要什么类型 x ，我们知道 ys 的类型，所以我们现在知道
  g ::（（a1，a1） - > Bool）
 ys :: [a1] 
 --- 
（\ x  - > let {{ -  ...  - }} in ys）:: a1  - > [a1] 
  
以类似的方式，我们可以得出结论：
 $在ys中）b $ b 
 （\g  - >（\ x  - > let {{ -  ...  - }} ::（（a1，a1 ） - > Bool） - > a1  - > [a1] 
  
此时，您只需重新命名（实际上是泛化，因为您想要将它绑定到 fun ）类型变量，并且您有答案。
 
I'm trying to understand why the type of fun g x = ys where ys = [x] ++ filter (curry g x) ys is ((a, a) -> Bool) -> a -> [a].

I understand that:

filter :: (a -> Bool) -> [a] -> [a] and that curry :: ((a, b) -> c) -> a -> b -> c

But I don't understand how to continue.
解决方案
The approach below is not necessarily the easiest or fastest, but it's relatively systematic.



Strictly speaking, you're looking for the type of
\g -> (\ x -> let ys = (++) [x] (filter (curry g x) ys) in ys)
(let and where are equivalent, but it's sometimes a little easier to reason using let), given the types
filter :: (a -> Bool) -> [a] -> [a]
curry :: ((a, b) -> c) -> a -> b -> c
Don't forget that you're also using
(++) :: [a] -> [a] -> [a]
Let's first look at the 'deepest' part of the syntax tree:
curry g x
We have g and x, of which we haven't seen before yet, so we'll assume that they have some type:
g :: t1
x :: t2
We also have curry. At every point where these functions occur, the type variables (a, b, c) can be specialized differently, so it's a good idea to replace them with a fresh name every time you use these functions. At this point, curry has the following type:
curry :: ((a1, b1) -> c1) -> a1 -> b1 -> c1
We can then only say curry g x if the following types can be unified:
t1  ~  ((a1, b1) -> c1)       -- because we apply curry to g
t2  ~  a1                     -- because we apply (curry g) to x
It's then also safe to assume that
g :: ((a1, b1) -> c1)
x :: a1
---
curry g x :: b1 -> c1
Let's continue:
filter (curry g x) ys
We see ys for the first time, so let's keep it at ys :: t3 for now. We also have to instantiate filter. So at this point, we know
filter :: (a2 -> Bool) -> [a2] -> [a2]
ys :: t3
Now we must match the types of filter's arguments:
b1 -> c1  ~  a2 -> Bool
t3        ~  [a2]
The first constraint can be broken down to
b1  ~  a2
c1  ~  Bool
We now know the following:
g :: ((a1, a2) -> Bool)
x :: a1
ys :: [a2]
---
filter (curry g x) ys :: [a2]
Let's continue.
(++) [x] (filter (curry g x) ys)
I won't spend too much time on explaining [x] :: [a1], let's see the type of (++):
(++) :: [a3] -> [a3] -> [a3]
We get the following constraints:
[a1]  ~  [a3]           -- [x]
[a2]  ~  [a3]           -- filter (curry g x) ys
Since these constraints can be reduced to
a1  ~  a3
a2  ~  a2
we'll just call all these a's a1:
g :: ((a1, a1) -> Bool)
x :: a1
ys :: [a1]
---
(++) [x] (filter (curry g x) ys) :: [a1]
For now, I'll ignore that ys' type gets generalized, and focus on
\x -> let { {- ... -} } in ys
We know what type we need for x, and we know the type of ys, so we now know
g :: ((a1, a1) -> Bool)
ys :: [a1]
---
(\x -> let { {- ... -} } in ys) :: a1 -> [a1]
In a similar fashion, we can conclude that
(\g -> (\x -> let { {- ... -} } in ys)) :: ((a1, a1) -> Bool) -> a1 -> [a1]
At this point, you only have to rename (actually, generalize, because you want to bind it to fun) the type variables and you have your answer.

                        
这篇关于有趣的类型g x = ys其中ys = [x] ++ filter（curry g x）ys？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！