haskell - Haskell 如何执行 Beta 转换以派生类型?
问题描述
我正在通过参加fp 课程练习来学习 Haskell。有一个问题挡住了我的去路。我不知道 Haskell 是如何推断lift2 (<$>) (,)
的类型,结果如何Functor k => (a1 -> k a2) -> a1 -> k (a1, a2)
。
我试过lift2 (<$>)
's type,并通过 GHCI's command 验证: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
with (m -> n)
, b
with (f m)
, c
with(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)
。
要应用的值是, ,(,) :: a -> b -> (a, b)
如何替换为, ?k
m
n
a
b
GHCI 的答案是lift2 (<$>) (,) :: Functor k => (a1 -> k a2) -> a1 -> k (a1, a2)
输入:t lift2 (<$>) (,)
. 我无法自己推断出这个答案。
所以我有2个问题。
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
forApplicative
和F
for 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
. 我们可以通过:i Applicative
在 GHCi 中的提示符下键入来查看它。查看它打印的实例列表,我们发现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)
。这是我们得出的。
(*)另请参阅:
推荐阅读
- r - 删除选择列中缺少数据的行,前提是它们在所有列中都没有缺失数据(最好使用 complete.cases)
- python - 并非所有组都在 Telethon 中可见
- selenium - 如何使用 selenium 将 PDF 文件下载到我的框架文件夹中
- c++ - 套接字编程中连接错误的原因(在客户端)?
- python - 如何知道图像预测的区域?
- nginx - 如何在 Pacemaker/Corosync 中优先考虑节点?
- angularjs - 如何使用单向绑定更改传递给子组件的对象
- c - 将十六进制输入存储到 int 变量中而不使用 C 中的 scanf() 函数
- ms-access - 包含来自访问中的多个字段的数据的组合框
- java - Spring Boot 无法反序列化包含 OffsetDateTime 的对象