手动推导'f1 x xs =（filter。（<））x xs`的类型 [英] Manual derivation of the type for `f1 x xs = (filter . (&lt;)) x xs`

问题描述

我想手动派生类型：

f1 x xs =（filter。（<））x xs $ b

第一次看到 x ，所以：

  x :: t1 
  

然后（<）具有此类型：

 （<）:: Ord a1 => a1  - > a1  - > Bool 
  

我们只能说（< x）如果以下类型可以统一：

  t1〜a1 
  

然后

  x :: a1 
  

所以

 （ < x）:: Ord a1 => a1  - > Bool 
  

过滤器有这种类型

  filter ::（a2  - > Bool） - > [a2]  - >第一次看到xs，所以： 
 $ b  

$ b

  xs :: t2 
  

我们只能例如（filter。（<））x xs ，如果以下类型可以统一：

  a1  - > Bool〜a2  - > Bool 
 t2〜[a2] 
  

所以我得到 f1 ::（a2 - > Bool） - > [a2] - >当正确的类型是 Ord a =>时，与 filter 类型相同的[a2] a - > [a] - > [b]



任何帮助？约束

  a1  - >方案

Bool〜a2 - > Bool


可以分解为



  a1〜a2 
  

以及明显的真正的

  Bool〜Bool 
  

所以你有 a1〜a2 。你已经知道 x 是 a1 ， xs 是 [a2] ，并且，感谢 filter ，结果类型为 [a2] 。因此，您最终得到：



  f1 :: Ord a2 => a2  - > [a2]  - > [a2] 
  

（不要忘记类约束 a1 来自（<）。）

I want to manually derive the type of:

f1 x xs = (filter . (<)) x xs

First time we see x, so:

x :: t1

Then (<) has this type:

(<) :: Ord a1 => a1 -> a1 -> Bool

We can only say (< x) if the following types can be unified:

t1  ~  a1

Then

x :: a1

So

(<x) :: Ord a1 => a1 -> Bool

Filter has this type

filter :: (a2 -> Bool) -> [a2] -> [a2]

First time to see xs, so:

xs :: t2

We can only say (filter . (<)) x xs if the following types can be unified:

a1 -> Bool ~ a2 -> Bool
t2  ~ [a2]

So I get that f1 :: (a2 -> Bool) -> [a2] -> [a2], the same type as filter, when the correct type is Ord a => a -> [a] -> [a] (asking GHCi).

Any help?

解决方案

The constraint

a1 -> Bool ~ a2 -> Bool

can be broken down to

a1 ~ a2

and the obviously true

Bool ~ Bool

So you have a1 ~ a2. You already know that x is a1, xs is [a2] and, thanks to filter, the result type is [a2]. Therefore, you end up with:

f1 :: Ord a2 => a2 -> [a2] -> [a2]

(Don't forget the class constraint a1 got from (<).)

这篇关于手动推导'f1 x xs =（filter。（<））x xs`的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！