有趣的类型g x = ys其中ys = [x] ++ filter（curry g x）ys？

本文介绍了有趣的类型g x = ys其中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 和其中是等价的，但有时使用 $ > ），给定类型 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 -> cBut 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 typesfilter :: (a -> Bool) -> [a] -> [a]curry :: ((a, b) -> c) -> a -> b -> cDon't forget that you're also using(++) :: [a] -> [a] -> [a]Let's first look at the 'deepest' part of the syntax tree:curry g xWe have g and x, of which we haven't seen before yet, so we'll assume that they have some type:g :: t1x :: t2We 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 -> c1We can then only say curry g x if the following types can be unified:t1 ~ ((a1, b1) -> c1) -- because we apply curry to gt2 ~ a1 -- because we apply (curry g) to xIt's then also safe to assume thatg :: ((a1, b1) -> c1)x :: a1---curry g x :: b1 -> c1Let's continue:filter (curry g x) ysWe 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 knowfilter :: (a2 -> Bool) -> [a2] -> [a2]ys :: t3Now we must match the types of filter's arguments:b1 -> c1 ~ a2 -> Boolt3 ~ [a2]The first constraint can be broken down tob1 ~ a2c1 ~ BoolWe now know the following:g :: ((a1, a2) -> Bool)x :: a1ys :: [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) ysSince these constraints can be reduced toa1 ~ a3a2 ~ a2we'll just call all these a's a1:g :: ((a1, a1) -> Bool)x :: a1ys :: [a1]---(++) [x] (filter (curry g x) ys) :: [a1]For now, I'll ignore that ys' type gets generalized, and focus on\x -> let { {- ... -} } in ysWe know what type we need for x, and we know the type of ys, so we now knowg :: ((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？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！