我尝试按照Gabriel Gonzalez的文章进行操作,但是我遇到了类型不匹配的问题。请考虑以下简短的模块:
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types #-}
module Yoneda where
newtype F a = F a deriving (Show, Functor)
type G f a = forall a'. (a -> a') -> f a'
fw :: Functor f => G f a -> f a
fw x = x id
bw :: Functor f => f a -> G f a
bw x = \f -> fmap f x
它能够成功编译。(无论是使用ghc
8.2.2还是8.4.3。)但当我在repl中运行它时,fw
和bw
不能组合:
λ :t bw . fw
<interactive>:1:6: error:
• Couldn't match type ‘a’ with ‘G f a1’
‘a’ is a rigid type variable bound by
the inferred type of it :: Functor f => a -> (a1 -> a') -> f a'
at <interactive>:1:1
Expected type: a -> f a1
Actual type: G f a1 -> f a1
• In the second argument of ‘(.)’, namely ‘fw’
In the expression: bw . fw
当我更仔细地看 bw
时,它似乎接受和返回的函子类型是不同的:
λ :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'
即使我在类型签名中表示它们应该相同!无论我如何在fw
和bw
中添加类型注释,它们都不想统一。
如果我从fw
中删除类型签名,一切都可以顺利进行。特别是,推断的类型签名将是:
fw :: ((a -> a) -> t) -> t
因此,似乎普遍量词
forall
会破坏事情的发展。但我不明白为什么。它难道不应该意味着“任何类型的a -> a'
都可以,包括a -> a
”吗?看起来好像相同的类型同义词G f a
在fw
和bw
的类型签名中扮演了不同的角色!这里到底发生了什么?
更多实验:
λ (fw . bw) (F 1)
...error...
λ (fw (bw (F 1)))
F 1
λ :t fw . undefined
...error...
λ :t undefined . fw
...error
λ :t bw . undefined
bw . undefined :: Functor f => a1 -> (a2 -> a') -> f a'
λ :t undefined . bw
undefined . bw :: Functor f => f a -> c
正如@chi在答案中指出的那样,没有任何函数可以与fw
组合。但是对于bw
并非如此。为什么?
bw :: Functor f => f a -> (a -> a') -> f a'
。你是如何得到上面的f1
和f2
的? - chi