我如何手动推断实例const :: a - ＆gt; a - ＆gt;一个

发布于 2025-02-08 18:05:07 字数 618 浏览 0 评论 0原文

Haskell类型变量被隐式量化。关键字forall出现在::之后。

例如，const类型签名

const :: a -> b -> a

写为：

const :: forall a b. a -> b -> a

我的问题是：如何有效地

const :: forall a. a -> a -> a

从该定义中推断签名。我尝试使用从一阶逻辑中学到的概念，例如 universion消除，但从理论的角度看不到合理。

当然，这是有道理的，因为没有什么阻止b与a相同。

为什么我无法证明使用该推论规则是合理的？因为我无法在第二个量词上使用消除，因为变量会发生冲突。我无法用a实例化b。

原文

Haskell type variables are implicitly quantified. The keywords forall appear after ::.

For example, const type signature

const :: a -> b -> a

is written as:

const :: forall a b. a -> b -> a

My question is: how can I validly infer the signature

const :: forall a. a -> a -> a

from that definition. I tried using concepts I learned from first-order logic like Universal Elimination but couldn't justify from a theoretic standpoint.

Of course, it makes sense since nothing precludes b being the same as a.

Why I couldn't justify using that inference rule ? Because I can't use elimination on that second quantifier since variables would clash. I can't instantiate b with a.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

〆凄凉。 2025-02-15 18:05:07

考虑：

(1) const :: forall a b. a -> b -> a

(2) const :: forall a. a -> a -> a

您不能推断（2）（1）;如果可以的话，那意味着const 始终的类型拟合forall a。 a - ＆gt; a - ＆gt;（在（1）中还不明显，因为我们还没有应用足够的推理步骤）。但是我显然可以在const true'a'a''的情况下使用const，其中const具有类型bool - ＆gt; char - ＆gt;布尔。

您能做的就是意识到（2）是（1）的实例化。 B与A 一般不同，但是（如您所说），没有什么停止b与a在任何一种特定用法中都是同一件事。因此，从使用const的上下文中，您可能可以推断特定用法具有类型for a。 a - ＆gt; a - ＆gt;。例如，这发生在以下情况下：

silly :: forall a. a -> a
silly x = const x x

您还可以从const :: forall a b中分辨出来。 a - ＆gt; b - ＆gt;仅一个，如果您选择实例b与a相同 - ＆gt; a - ＆gt; 。我们始终有一个选项，因为承诺对 All 可能有效的类型可能的类型b包括可能性子集，其中我们总是为b 就像我们为a所做的那样。

为此，我们只需将b s替换为a s（在我们正在实例化的量词范围内，但这是整个表达式）。您表示怀疑您可以这样做，因为变量会发生冲突，但是实例化一个变量与另一个变量相同，是我们在这里所做的 point 。它与简单地重命名变量和偶然地通过给出的变量相同的名称来更改表达式的情况并不相同；在这里，我们正在做出故意的选择，以检查特殊情况时，当它们不是截然不同的情况下。

但是，没有const :: forall a - ＆gt的纯推理链； b - ＆gt;单独（没有任何使用何处的上下文）到const :: forall a。 a - ＆gt; a - ＆gt;，因为当您进行更改时，您正在削弱/专业化const;您选择将其限制为最通用类型的子类型。推理规则不会从（1）到（2）将您添加到选择将b与a相同的其他信息。（用haskelly术语，这将是一个附加的a〜b约束）

Consider:

(1) const :: forall a b. a -> b -> a

(2) const :: forall a. a -> a -> a

You can't infer (2) from (1); if you could that would imply that const always has a type fitting forall a. a -> a -> a (and it just wasn't obvious in (1) because we hadn't applied enough inference steps yet). But I can obviously use const in situations like const True 'a', where const has type Bool -> Char -> Bool.

What you can do is realise that (2) is an instantiation of (1). b is not the same as a in general, but (as you said) there is nothing stopping b from being the same thing as a in any one particular usage. So from a context where const is used you may be able to infer that particular usage has type forall a. a -> a -> a. For example, that happens in:

silly :: forall a. a -> a
silly x = const x x

You can also tell from const :: forall a b. a -> b -> a alone that if you choose to instantiate b to be the same as a you get const :: forall a -> a -> a. We always have that as an option because the type promised to be valid for all possible types b, which includes the subset of possibilities where we always choose the same thing for b as we do for a.

To do that we do simply replace the bs with as (within the scope of the quantifier that we're instantiating, but here that's the whole expression). You expressed doubt that you could do this because the variables would clash, but instantiating one variable to be the same as the other is the point of what we're doing here. It's not the same as simply renaming variables and accidentally changing the expression by giving variables the same name that were supposed to be distinct; here we are making the deliberate choice to examine the special case when they are not distinct.

But there is no chain of pure inference from const :: forall a -> b -> a alone (without any context of where it is used) to const :: forall a. a -> a -> a, because when you make that change you are weakening/specialising const; you're choosing to limit it to a subtype of its most general type. Inference rules won't get you from (1) to (2) without you adding the additional information that you are choosing to limit b to be the same as a. (In Haskelly terms, this would be an additional a ~ b constraint)

回复收藏 0 原文

孤寂小茶 2025-02-15 18:05:07

以下是作为评论开始的，并被搬到这里。

因为我无法在第二个量词上使用消除，因为变量会发生冲突。

我认为您在这里是错的。实际上，您可以使用消除，变量冲突与普遍消除无关。 [从我从下面的来源中学到的，有时候发生冲突是相关的，有时不是。]

您能告诉我哪种自然扣除系统允许在通用消除推理中使用界变量？

斯坦福大学逻辑概论第8章
作为

∀ν.φ[ν]
------------
φ[τ]
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在∀ba⇒（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

。 a的量词 in ∀Ba⇒（b⇒a），因此a在（非现有）量词的范围内没有免费发生a的 in ∀ba⇒（b⇒a）。

The following started as comments and was moved here.

Because I can't use elimination on that second quantifier since variables would clash.

I think here you are simply wrong. You can in fact use elimination and the clash of variables is irrelevant for Universal Elimination. [From what I learned from the source below it seems to be the case that sometimes a clash is relevant and sometimes it is not.]

Could you tell me which Natural Deduction system allows using a bound variable in an Universal Elimination inference?

Chapter 8 of Stanford Introduction to Logic defines Universal Elimination (UE)
as

∀ν.φ[ν]
------------
φ[τ]
where τ is substitutable for ν in φ

and

We say that a term τ is free for a variable ν in a sentence φ if and only if no free occurrence of ν occurs within the scope of a quantifier of some variable in τ.

With this and Universal Introduction (UI) I would argue

∀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.

This leaves the claims that a is free for a in ∀b.a⇒(b⇒a), etc.

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

There is no quantifier of a in ∀b.a⇒(b⇒a), therefore a does not occur free within the scope of (the non existing) quantifier of a in ∀b.a⇒(b⇒a).

回复收藏 0 原文

~没有更多了~