问题描述
我通过练习 fp-course 来学习 Haskell。有一个 question 挡住了我的去路。我不知道 Haskell 如何推断 lift2 (<$>) (,)
的类型,结果是 Functor k => (a1 -> k a2) -> a1 -> k (a1,a2)
。
我已经尝试了 lift2 (<$>)
的类型,并通过 GHCI 的命令 :t lift2 (<$>)
进行了验证。步骤如下。
我知道lift2 :: applicative k => (a -> b -> c) -> k a -> k b -> k c
我也知道(<$>) :: Functor f => (m -> n) -> (f m) -> (f n)
然后通过lambda演算的Beta转换,我可以算出lift2 (<$>)
的类型是(applicative k,Functor f) => k (m -> n) -> k (f m) -> k (f n)
将 a
替换为 (m -> n)
,将 b
替换为 (f m)
,将 c
替换为 (f n)
当我要弄清楚lift2 (<$>) (,)
的类型时,它阻止了我。
我知道(,) :: a -> b -> (a,b)
还有lift2 (<$>) :: (applicative k,Functor f) => k (m -> n) -> k (f m) -> k (f n)
。
Haskell 如何将 lift2 (<$>)
应用于 (,)
?lift2 (<$>)
的第一个变量是 applicative k => k (m -> n)
。
要应用的值为 (,b)
k
、m
、n
如何替换为 a
、b
?
GHCI 的答案是 lift2 (<$>) (,) :: Functor k => (a1 -> k a2) -> a1 -> k (a1,a2)
,输入 :t lift2 (<$>) (,)
。我自己无法推断出这个答案。
所以我有两个问题。
1.谁能给我一步一步地展示推理?
2.在这种情况下,转换似乎不是 lambda 演算中的 Beta 转换(可能是我错了)。转换是什么?
解决方法
类型推导是一个机械问题。(*) 关键是函数箭头->
实际上是一个二进制 运算符 此处,在右侧关联(而应用程序/并列在左侧关联)。
因此 A -> B -> C
实际上是 A -> (B -> C)
实际上 (->) A ((->) B C)
实际上是 ((->) A) (((->) B) C)
。在这种形式中,很明显它由两部分组成,因此可以匹配例如f t
,注意等价的 f ~ ((->) A)
和 t ~ (((->) B) C)
(或伪代码 f ~ (A ->)
,以及普通符号中的 t ~ (B -> C)
)。
当“应用”两种类型的术语时,会执行结构统一。两个项的结构匹配,它们的子部分匹配,结果等价被标记为“替代”(... ~ ...
),可用于执行并确保结果类型项的进一步简化(和如果因此发现某些不兼容,则该类型将被拒绝)。
这遵循根植于 Modus Ponens 逻辑规则的一般结构/类型推导规则:
A -> B C
--------------
B,where A ~ C
因此,
liftA2 :: A f => ( a -> b -> c ) -> f a -> f b -> f c
(<$>) :: F h => (d -> e) -> h d -> h e
(,) :: s -> (t -> (s,t))
---------------------------------------------------------------------------------
liftA2 (<$>) (,) :: f b -> f c
---------------------------------------------------------------------------------
b ~ h d f ~ (s->)
a ~ d->e c ~ h e a ~ t->(s,t)
\_ _ _ _ _ _ _ _ _ _ _ _ _ _ a ~ d->e
----------------------------------------------------
d ~ t e ~ (s,t)
liftA2 (<$>) (,) :: f b -> f c
~ (s -> b ) -> (s -> c )
~ F h => (s -> h d) -> (s -> h e )
~ F h => (s -> h t) -> (s -> h (s,t))
(将 A
写为 Applicative
,将 F
写为 Functor
,作为缩写)。当没有更多类型变量要替换时,替换停止。
对于哪些类型变量在每个步骤中被选择替换有一定的自由度,但结果项将等同于一致重命名类型变量,反正。例如我们可以选择
~ F h => (s -> h d) -> (s -> h e )
~ F h => (s -> h d) -> (s -> h (s,t))
~ F h => (s -> h d) -> (s -> h (s,d))
在过程中发现了 Applicative ((->) s)
约束。由于此实例存在于所有 s
中,因此它会检出。我们可以通过在 GHCi 的提示符下输入 :i Applicative
来查看它。查看它打印的实例列表,我们发现 instance Applicative ((->) a) -- Defined in `Control.Applicative'
。
如果没有这样的实例,类型派生将停止并报告错误,它不会只是跳过它。但是由于约束成立,它只是消失了,因为它不约束派生类型 Functor h => (s -> h t) -> (s -> h (s,t))
。它已经“烤熟”了。
实例定义了 (f <*> g) x = f x $ g x
,但在类型派生中不需要定义本身,只需要它存在的事实。至于liftA2
,定义为
liftA2 h f g x = (h <$> f <*> g) x -- for any Applicative (sans the `x`)
= (h . f <*> g) x -- for functions
= (h . f) x (g x)
= f x `h` g x -- just another combinator
(是的,(<*>) = liftA2 ($)
),所以
liftA2 (<$>) (,) g s = (,) s <$> g s
= do { r <- g s -- in pseudocode,with
; return (s,r) -- "Functorial" Do
}
或者换句话说,liftA2 (<$>) (,) = \ g s -> (s,) <$> g s
。
类型为 Functor m => (s -> m t) -> s -> m (s,t)
。哪个是我们得出的。
(*) 另见: