手动推导`f1 x xs =(filter.(<))x xs`的类型

Question

我想手动派生类型:

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

我们第一次看到x,所以:

x :: t1

然后(<)有这种类型:

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

我们只能说(< x)是否可以统一以下类型:

t1  ~  a1

然后

x :: a1

所以

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

过滤器有这种类型

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

第一次看到xs,所以:

xs :: t2

我们只能说(filter . (<)) x xs是否可以统一以下类型:

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

所以我得到的,与正确类型f1 :: (a2 -> Bool) -> [a2] -> [a2]相同的类型(询问GHCi).filterOrd a => a -> [a] -> [a]

有帮助吗？

Answer 1

约束

a1 -> Bool ~ a2 -> Bool

可以细分为

a1 ~ a2

而且显然是真的

Bool ~ Bool

所以你有a1 ~ a2.你已经知道那x是a1,xs是,[a2]并且,由于filter结果类型是[a2].因此,您最终得到:

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

(不要忘记阶级约束a1从获得(<).)