类型类实例中的统一怪异

Question

假设我有以下（愚蠢的）class：

class BlindMap m where
    mapB :: m a -> m b

我可以提供以下 [] 实例：

instance BlindMap [] where
    mapB = map id

RHS的类型是[a] -> [a]，应该和[a] -> [b]统一，但是GHC不这么认为：

Couldn't match type ‘a’ with ‘b’
  ‘a’ is a rigid type variable bound by
      the type signature for mapB :: [a] -> [b] at dingas.hs:11:5
  ‘b’ is a rigid type variable bound by
      the type signature for mapB :: [a] -> [b] at dingas.hs:11:5
Expected type: a -> b
  Actual type: b -> b
Relevant bindings include
  mapB :: [a] -> [b]
In the first argument of ‘map’, namely ‘id’
In the expression: map id

我在这里错过了什么？

提前致谢。

Answer 1

What am I missing here?

map id 生成一些任意类型的值列表，给定此类值的列表。 [a] -> [b] 承诺在给定 可能不同 类型的值列表的情况下生成某个任意类型的值列表。

因此它期望的是 a -> b，但是你的基于 id 的函数只能接受它 returns，所以 b -> b.

Answer 2

更一般地说，您说您将提供以下类型的函数：

forall a b.[a] -> [b]

在您的实例定义中。编译器接受了你的话。

既然你想出了一个实例，编译器确实需要看到这个神奇的功能。并且它会拒绝所有没有达到您承诺的效果的代码。

在继续之前，您应该尝试编写一个函数

forall a b. a -> b

你会发现你最多只能想出类似的东西：

f x = f x
g x = error "not terminating."

并且只要没有可用的元素映射函数，就只能写出如下实例：

instance BlindMap (Maybe a) where mapB _ = Nothing
instance BlindMap ([a])     where mapB _ = []

以此类推。

类型类实例中的统一怪异

Unification Weirdness in Typeclass Instance

haskell

functional-programming

typeclass

unification

type-theory