Stream: Beginner Questions

Topic: Introduced fixed type variable(s)???

Yoav Cohen (Jul 22 2026 at 10:38):

What even is the difference between those instances such that I need to like

fix a :: 'b

in the second one or whatever.

Mathias Fleury (Jul 22 2026 at 18:16):

the types to infer are "deferred" to the next line

Mathias Fleury (Jul 22 2026 at 18:17):

in a = a, you have no restriction, so you end up with type 'b, while in the first case F a restricts a to be exactly the right type

Yoav Cohen (Jul 22 2026 at 18:33):

I don't understand. what kinda restriction does F a put on a's type?

Mathias Fleury (Jul 23 2026 at 19:58):

F has a type due to the lemma

Mathias Fleury (Jul 23 2026 at 19:59):

the type is inferred there

Yoav Cohen (Aug 22 2026 at 17:45):

I don't get it :sob:

Ant S. (Aug 22 2026 at 17:51):

Yoav Cohen said:

I don't get it :sob:

what exactly do you not get? That F has a type? That the type can be inferred?

Yoav Cohen (Aug 22 2026 at 17:52):

both, but mostly like how are the types working here? F has a predicate type? is = not also a predicate?

Ant S. (Aug 22 2026 at 17:54):

Let me copy your snippets into a scratch file and write up a quick explanation

Ant S. (Aug 22 2026 at 18:01):

Yoav Cohen said:

F has a predicate type?

Suppose you want to say something about some object x, and you don't specify what type x has. It could be a nat, a bool or something else. Suppose you have some predicate F and you want to prove F x, that is, in more traditional math notation, $F(x)$. Now, Isabelle does not know what type to assign to x, so by default, we will assume it is polymorphic, that is to say, "it is some type, but I cannot tell you what it is".

Are you familiar with polymorphism over functions?

Yoav Cohen (Aug 22 2026 at 18:02):

I am not

Ant S. (Aug 22 2026 at 18:06):

ok, that's a good place to start.
In a typed language (such as ML, or Haskell, and Isabelle for that matter), we can write some functions that take in an input of some type without specifying what that type is. The quintessential example of this is the identity function. This function takes in "an x" and spits out the same "x".

id :: a => a
id x = x

Notice how id can work if you used a bool, a nat, or some other wacky type you'd like to build. So we use a type variable to say that it is "some type, but I can't tell you anything else until you give me a concrete input". So for example, id 5 = 5 here treats id as a function of typenat => nat while id true = true here treats id as a function of typebool => bool

Ant S. (Aug 22 2026 at 18:07):

a => a means "you give me a thing of type a, and I will spit out something of type a"

Ant S. (Aug 22 2026 at 18:07):

does that make sense?

Yoav Cohen (Aug 22 2026 at 18:08):

well but this far into the thing, isn't F the same, as far as isabelle is aware? like wouldn't F be able to take any input as far as it knows? just like =

Ant S. (Aug 22 2026 at 18:14):

F can, in fact, take in "any input", that is, it is polymorphic over its input x. From the structure of the first lemma, we can infer that F is a predicate (I will elide this step for now, and we can get back to it later). Since it takes in some x, we will say that x is of type a. Later on, when you use this theorem on say, the natural numbers, you can apply the theorem in the same way as you would if x were a boolean.

For what its worth, that a fixed type variable is introduced in your second theorem is a warning from the proof system, not an error.

Yoav Cohen (Aug 22 2026 at 18:15):

but well basically, polymorphism allows you to specify one "type" for id, and it will make an instance of it for all types?

Ant S. (Aug 22 2026 at 18:17):

for whatever type of some input that is passed in to id, yes. You can think of id acting that way. How "will make an instance of [id]" works sounds like an implementation detail of polymorphism, which is an unrelated but interesting thing to read about.

Ant S. (Aug 22 2026 at 18:22):

If you want to understand polymorphism, that's usually covered in notes in a functional programming course. I'm biased towards Haskell (despite Isabelle being tied a lot more to ML, a lot of the functional programming ideas transfer over quite easily) so I'd recommend reading this to understand type variables.

Ant S. (Aug 22 2026 at 18:24):

does that help? I see two different questions here. One is really about what type variables are and how they work, and the other is what's going on in your proof and why the warning comes up with equality.

Ant S. (Aug 22 2026 at 18:25):

That's what it seems to me, that is

Yoav Cohen (Aug 22 2026 at 18:30):

well so what's the reason for this warning? isn't = also a predicate? or maybe there is something to do with the quantification instead?

Ant S. (Aug 22 2026 at 18:31):

lemme draw this out real quick

Ant S. (Aug 22 2026 at 18:39):

Ok this is taking a little longer than I thought to annotate, might be more like 10 minutes

Yoav Cohen (Aug 22 2026 at 18:40):

take your time, I am in no hurry

Ant S. (Aug 22 2026 at 18:42):

Ant S. (Aug 22 2026 at 18:42):

Ant S. (Aug 22 2026 at 18:42):

Ant S. (Aug 22 2026 at 18:42):

as for the other proof

Ant S. (Aug 22 2026 at 18:51):

Notice specifically where F comes from and where equality comes from. F is arbitrary but defined by you for your proof, while equality isn't, and I think that's where the difference stems from

Ant S. (Aug 22 2026 at 18:52):

lemma "(∀x. F x ∧ G x) ⟶ (∀x. F x)"
proof
  assume meow: "(∀x. F x ∧ G x)"
  have "F b" sorry
  have "F c" sorry
  show "∀ x. F x"
  proof
    fix a
    fix b
    from meow have "F a ∧ G a" ..
    thus "F a" ..
  qed
qed

in this example, I have added two lines. It might make more sense if you hover around the type of b and c

Ant S. (Aug 22 2026 at 18:54):

lemma "∀x. ∃y. x = y"
proof -
  fix a
  have "b = b" sorry
  have "c = c" sorry
  have "a = a" by (rule refl)
  have "∃y. a = y" by blast
  show "∀x. ∃y. x = y" by blast
qed

Now do the same thing here. Equality is already given to you, so every time you make a claim about some equality, it can be a different type. b and c need not be the same. you could have "true = true" in one line, and "2 + 3 = 3 + 2" in the other

Ant S. (Aug 22 2026 at 18:55):

Mathias Fleury said:

in a = a, you have no restriction, so you end up with type 'b, while in the first case F a restricts a to be exactly the right type

that's what this is trying to say

Ant S. (Aug 22 2026 at 18:55):

From what I understand, the difference is where F and equality are "coming from", respectively

Ant S. (Aug 22 2026 at 18:58):

lemma "(∀x. F x ∧ G x) ⟶ (∀x. F x)"
proof
  assume meow: "(∀x. F x ∧ G x)"
  show "∀ x. F x"
  proof
    fix a
    have "H a" sorry
    from meow have "F a ∧ G a" ..
    thus "F a" ..
oops

notice what happens in this proof. You haven't specified H beforehand, so what can we infer about a? So it's given a new type: 'b. Now notice how we can't say F a anymore because we have no clue if this thing of some type 'b is the same as 'a. It could be the same, we don't know.

Ant S. (Aug 22 2026 at 18:58):

I hope that makes it a bit more enlightening

Ant S. (Aug 22 2026 at 19:19):

@Yoav Cohen it may also be useful to add this to your file, so you can see intermediate types in the proof state:
declare [[show_types]]

Yoav Cohen (Aug 24 2026 at 18:21):

I think maybe there is something about = being polymorphic that makes it so that every occurence of it uses a different arbitrary type or something

Yoav Cohen (Aug 24 2026 at 18:22):

Though I couldn't find the implementation details for that

Yoav Cohen (Aug 24 2026 at 18:42):

Yoav Cohen said:

both, but mostly like how are the types working here? F has a predicate type? is = not also a predicate?

Let's consider a predicate Same that is binary instead of the F here. We could then characterize the type of both Same and = as ['a,'a] => Bool, however, for = it would also be polymorphic? so for every occurence of it 'a would be changed to something else, first 'b and then 'c and so on

Ant S. (Aug 24 2026 at 19:25):

I think the question you're trying to ask is "is the arity (how many arguments a predicate takes) of my predicate relevant?" and I think no.

I think the underlying question is that you want to know when and where Same, F and ='s types are being inferred

Ant S. (Aug 24 2026 at 19:30):

@Makarius Wenzel Is your thesis, section 3.4.3 (type inference and polymorphism) relevant here?

Yoav Cohen (Aug 24 2026 at 19:31):

Sorry I wasn't clear there, the arity change was irrelevant, it's just so I could characterize their types more easily and stuff

Ant S. (Aug 24 2026 at 19:32):

No worries, making clear questions takes time :)

Yoav Cohen (Aug 24 2026 at 19:54):

I've found this https://stackoverflow.com/q/33857454

Ant S. (Aug 24 2026 at 19:58):

Good catch. That was 11 years ago, so is it still good practice to bind the type variable explicitly?

Ant S. (Aug 24 2026 at 19:58):

(I'm asking because I don't know)

Last updated: Sep 08 2026 at 08:41 UTC