Haskell类型变量是隐式量化的。关键词forall
出现在::
之后。
例如:const
类型签名
const :: a -> b -> a
被写成:
const :: forall a b. a -> b -> a
我的问题是:我如何才能有效地推断签名
const :: forall a. a -> a -> a
定义中的。我尝试使用从一阶逻辑中学到的概念,如普遍消去,但无法从理论的角度证明。
当然,这是有意义的,因为没有什么可以排除b
与a
相同。
为什么我不能证明使用推理规则是合理的?因为我不能对第二个量词使用消去法因为变量会冲突。我不能用a
实例化b
。
考虑:
(1) const :: forall a b. a -> b -> a
(2) const :: forall a. a -> a -> a
你不能推断(2)从(1);如果可以的话,这意味着const
总是具有适合forall a. a -> a -> a
的类型(在(1)中并不明显,因为我们还没有应用足够的推理步骤)。但我显然可以在const True 'a'
的情况下使用const
,其中const
的类型为Bool -> Char -> Bool
。
您可以做的是意识到(2)是(1)的实例化。b
与a
一般不同,但是(正如你所说的)没有什么可以阻止b
在任何一个特定的用法中与a
相同。因此,从使用const
的上下文中,你可以推断出的特定用法类型为forall a. a -> a -> a
。例如:
silly :: forall a. a -> a
silly x = const x x
您还可以从const :: forall a b. a -> b -> a
单独看出,如果选择将b
实例化为与a
相同的const :: forall a -> a -> a
。我们总是把它作为一个选项因为该类型承诺对所有有效可能类型b
,其中包括我们总是为b
选择与a
相同的东西的可能性子集。
要做到这一点,我们只需将b
s替换为a
s(在我们实例化的量词范围内,但这里是整个表达式)。您表示怀疑是否可以这样做,因为变量会冲突,但是实例化一个变量使其与另一个变量相同是点我们在这里做的事。这与简单地重命名变量和不小心通过给应该不同的变量赋予相同的名称来改变表达式是不同的;当不不同时,这里我们故意选择检查特殊情况。
但是不存在从const :: forall a -> b -> a
到const :: forall a. a -> a -> a
的纯粹推理链(没有任何使用它的上下文),因为当你做出改变时,你正在削弱/专门化const
;您选择将其限制为最一般类型的子类型。如果不添加您选择将b
限制为与a
相同的附加信息,推理规则将无法使您从(1)到(2)。(在Haskelly术语中,这将是一个额外的a ~ b
约束)
下面的开始为注释,被移到这里
因为我不能在第二个量词上使用消去,因为变量会冲突。
我认为你完全错了。事实上,你可以使用消去法,变量的冲突与通用消去法无关。[从我从下面的来源了解到的情况来看,似乎冲突有时是相关的,有时不是。]
你能告诉我哪个自然演绎系统允许在全称消除推理中使用有界变量吗?
斯坦福逻辑导论第8章将普遍消去(UE)定义为
∀ν.φ[ν]
------------
φ[τ]
where τ is substitutable for ν in φ
和
我们说,当且仅当在句子φ中某个变量的量词范围内没有ν自由出现时,项τ对变量ν是自由的。
与通用介绍(UI)我认为
∀a.∀b.a⇒(b⇒a)
-------------- UE, a is free for a in ∀b.a⇒(b⇒a).
∀b.a⇒(b⇒a)
-------------- UE, a is free for b in a⇒(b⇒a).
a⇒(a⇒a)
-------------- UI, a does not occur free in both a⇒(a⇒a) and
∀a.a⇒(a⇒a) an active assumption. I am not sure about this.
这留下了a is free for a in ∀b.a⇒(b⇒a)
等的声明
a is free for a in ∀b.a⇒(b⇒a)
⇔
no free occurrence of a occurs within the scope of a quantifier of some variable in a
∀b.a⇒(b⇒a)
中没有a
的量词,因此a
不会在∀b.a⇒(b⇒a)
中(不存在的)a
的量词范围内自由出现。