<p>Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your <span class="math-container">$\mathrm{reflexive}$</span> example, there are two polymorphic constants at play:</p>
<p><span class="math-container">$$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$</span>
<span class="math-container">$$(=) : \alpha \to \alpha \to \mathrm{bool}$$</span></p>
<p>You should remember the type used to instantiate any polymorphic constants in your theorems. This solves your problem.</p>
<p>In general, most HOL systems I'm aware of identify constants and variables by their (name, type) pair in the kernel. That is, <span class="math-container">$x_{bool}$</span> and <span class="math-container">$x_{nat}$</span> are different variables, but when they both occur in the same context, the parsing and printing logic are allowed to complain. This is a nice way to think about the logic...</p>

CC BY-SA 4.0
2021-04-15T20:34:13.290Z
2021-04-15T20:34:13.290Z
Maya
<p>A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: <span class="math-container">$$\forall p, (p(T) \wedge p(F)) = \forall x, p(x) $$</span> HM can easily infer that <span class="math-container">$p$</span> has type <code>Bool -&gt; Bool</code> and <span class="math-container">$x$</span> has type <code>Bool</code>.</p>
<p>But IIUC, theorems don't always prove the most general interpretation of a proposition. For example, say that I prove <span class="math-container">$T = T$</span> and <span class="math-container">$F = F$</span>, and use these with the above axiom to prove <span class="math-container">$$\forall x, x = x$$</span></p>
<p>In this case, the proof assistant <strong>must</strong> explicitly keep track of the fact that <span class="math-container">$x$</span> had type <code>Bool</code>, right? Without this extra information, the type system would infer that <span class="math-container">$x$</span> could be any arbitrary <span class="math-container">$\alpha$</span>, even though we've only proved the <span class="math-container">$x : $</span> <code>Bool</code> case. (I know that equality <strong>should</strong> probably be reflexive in every type, but one shouldn't be able to prove this for all types from just checking <span class="math-container">$T$</span> and <span class="math-container">$F$</span>).</p>
<p>How do existing proof assistants combat this issue? How much &quot;extra&quot; type information do they need to track to avoid accidentally &quot;over-generalizing&quot;?* Is this a phenomenon which has been encountered/documented in existing proof assistants (whether they use HM or more complex dependent type systems)?</p>
<p>* I initially believed that you could resolve this issue by just tracking the types of all bound variables, but this doesn't seem to work: Suppose in our theory we define the predicate <span class="math-container">$\mathrm{reflexive}(f) = \forall x, f(x, x)$</span>, then we can use the above theorem to prove <span class="math-container">$\mathrm{reflexive}(=)$</span>. This proposition has no bound variables, but again we must somehow keep track of the fact that it has <strong>only</strong> been proven for equality over type <code>Bool</code>.</p>

CC BY-SA 4.0
2021-03-24T13:31:07.413Z
It is unclear how you intend to use such a proof assistant (I take it you have in mind HOL-style proof assistants) to get from $T = T$ to $F = F$. I suggest that you either provide an  actual example, or a more detailed description of what you have in mind, or choose a better example. The one you have is double unfortunate for being both true and blatantly polymorphic.
Andrej Bauer
CC BY-SA 4.0
2021-03-24T13:32:10.727Z
To be precise, the murky part of your question is "and use these with the above axiom to prove". What *exactly* do you tell the proof assistant when you "use" $T = T$"?
Andrej Bauer
CC BY-SA 4.0
2021-03-24T13:45:28.097Z
I'm not sure of the exact HOL-style syntax. But from $T = T$ and $F = F$ you can prove $(T = T) \wedge (F = F)$, which is beta equivalent to $(\lambda y, y = y)(T) \wedge (\lambda y, y = y)(F)$.  Therefore you can apply the axiom to get $\forall x, (\lambda y, y = y)(x)$ which beta-reduces to the theorem.
user1636815
CC BY-SA 4.0
2021-03-24T13:47:03.440Z
A better example of an theorem which is "obviously wrong when over-generalized" would be: $\forall f \forall x,  f(x) = f(f(f(x)))$.  The proof assistant **must** track that $x$ has type `Bool` to remain sound, even though $x$ could have a more general inferred type.
user1636815
CC BY-SA 4.0
2021-03-24T15:23:54.817Z
I see. Well, there is no problem. As soon as you use your axiom, it will force $x$ in $\forall x, x = x$ to get type $\mathtt{bool}$.
Andrej Bauer
<type-theory><typed-lambda-calculus><proof-assistants>
How much type information do Hindley-Milner proof assistants need to remain sound?
user1636815
# How much type information do Hindley-Milner proof assistants need to remain sound?

(Asked by: username_0 on 2021-03-24)

A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall p, (p(T) \wedge p(F)) = \forall x, p(x) $$ HM can easily infer that $p$ has type `Bool -> Bool` and $x$ has type `Bool`.

But IIUC, theorems don't always prove the most general interpretation of a proposition. For example, say that I prove $T = T$ and $F = F$, and use these with the above axiom to prove $$\forall x, x = x$$

In this case, the proof assistant **must** explicitly keep track of the fact that $x$ had type `Bool`, right? Without this extra information, the type system would infer that $x$ could be any arbitrary $\alpha$, even though we've only proved the $x : $ `Bool` case. (I know that equality **should** probably be reflexive in every type, but one shouldn't be able to prove this for all types from just checking $T$ and $F$).

How do existing proof assistants combat this issue? How much "extra" type information do they need to track to avoid accidentally "over-generalizing"?\* Is this a phenomenon which has been encountered/documented in existing proof assistants (whether they use HM or more complex dependent type systems)?

\* I initially believed that you could resolve this issue by just tracking the types of all bound variables, but this doesn't seem to work: Suppose in our theory we define the predicate $\mathrm{reflexive}(f) = \forall x, f(x, x)$, then we can use the above theorem to prove $\mathrm{reflexive}(=)$. This proposition has no bound variables, but again we must somehow keep track of the fact that it has **only** been proven for equality over type `Bool`.

**Tags:** type-theory, typed-lambda-calculus, proof-assistants
> **Comments:**
> **username_1**: It is unclear how you intend to use such a proof assistant (I take it you have in mind HOL-style proof assistants) to get from $T = T$ to $F = F$. I suggest that you either provide an  actual example, or a more detailed description of what you have in mind, or choose a better example. The one you have is double unfortunate for being both true and blatantly polymorphic.  
> **username_1**: To be precise, the murky part of your question is "and use these with the above axiom to prove". What *exactly* do you tell the proof assistant when you "use" $T = T$"?  
> **username_0**: I'm not sure of the exact HOL-style syntax. But from $T = T$ and $F = F$ you can prove $(T = T) \wedge (F = F)$, which is beta equivalent to $(\lambda y, y = y)(T) \wedge (\lambda y, y = y)(F)$.  Therefore you can apply the axiom to get $\forall x, (\lambda y, y = y)(x)$ which beta-reduces to the theorem.  
> **username_0**: A better example of an theorem which is "obviously wrong when over-generalized" would be: $\forall f \forall x,  f(x) = f(f(f(x)))$.  The proof assistant **must** track that $x$ has type `Bool` to remain sound, even though $x$ could have a more general inferred type.  
> **username_1**: I see. Well, there is no problem. As soon as you use your axiom, it will force $x$ in $\forall x, x = x$ to get type $\mathtt{bool}$.  

---

## 1 answers

### Answer by username_2 on 2021-04-15. Score: 0

Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your $\mathrm{reflexive}$ example, there are two polymorphic constants at play:

$$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$
$$(=) : \alpha \to \alpha \to \mathrm{bool}$$

You should remember the type used to instantiate any polymorphic constants in your theorems. This solves your problem.

In general, most HOL systems I'm aware of identify constants and variables by their (name, type) pair in the kernel. That is, $x\_{bool}$ and $x\_{nat}$ are different variables, but when they both occur in the same context, the parsing and printing logic are allowed to complain. This is a nice way to think about the logic...


---

