Zulip Chat Archive

Stream: general

Topic: Inequality of Types

DayDun (Oct 23 2022 at 00:31):

Is it possible to prove that two Types are not equal? Such as nat and bool. Usually induction can be used to prove inequality of regular values, but is it possible to perform induction over Types?

Junyan Xu (Oct 23 2022 at 02:07):

nat ≠ bool is easy to prove, but if the two types have the same cardinality, then it's probably undecidable independent of Lean's type theory whether they are equal.

import data.fintype.basic

example : nat  bool :=
  intro h,
  have := congr_arg finite h,
  revert this,
  simp only [nat.infinite, imp_false, bool.fintype.finite,
    not_finite_iff_infinite, eq_iff_iff, iff_true],

DayDun (Oct 23 2022 at 03:25):

Thanks! That's an interesting way of proving it. Is there anything special about cardinality though? Wouldn't it be possible to construct some other proposition which holds for one type but not the other?

Adam Topaz (Oct 23 2022 at 03:28):

If you can prove that there is no bijection between your two types, then you can prove that the two types are not equal.

DayDun (Oct 23 2022 at 03:33):

So lean considers them equal if there's a bijection between the types?

Junyan Xu (Oct 23 2022 at 03:41):

@Mario Carneiro seems to indicate the existence of a "minimal model" of Lean's type theory such that nat = int and a "maximal model" such that nat ≠ int here (update: more explicit claim). I don't think the models are explicitly written down though. The model in his master thesis is probably closer to the maximal model.

Mario Carneiro (Oct 23 2022 at 03:45):

I have some unfinished work on a slightly more maximal model, where you can tag types with their method of construction and thus distinguish between identically defined inductive types or functions vs universes vs structures

Mario Carneiro (Oct 23 2022 at 03:46):

The cardinality model seems straightforward enough but it has not been written down in detail

Mario Carneiro (Oct 23 2022 at 03:47):

It would probably make more sense to write down a scheme for constructing models with any collection of types under some assumptions

Mario Carneiro (Oct 23 2022 at 03:48):

Assuming there are no issues in the construction, the cardinality model implies that the only thing you can use to provably distinguish types in lean is cardinality

Mario Carneiro (Oct 23 2022 at 03:57):

In more detail, the cardinality model works as follows: Types are represented as cardinals (initial ordinals), and we fix in advance a family of bijections for every possible way you can interpret a cardinal as a pair, a sigma type, a function type, a universe etc. The elements of a type are just the elements of the cardinal in the ZFC sense. Then when f:ABf : A \to B and x:Ax : A, f  xf\;x is interpreted as taking fABf \in |A \to B|, using the chosen bijection τA,B:AB(AB)\tau_{|A|,|B|}:|A \to B|\simeq(|A| \to |B|) to get a function τA,B(f)\tau_{|A|,|B|}(f), and then applying it to xx to get an element τA,B(f)(x)B\tau_{|A|,|B|}(f)(x)\in |B|.

Kevin Buzzard (Oct 23 2022 at 07:07):

@DayDun the point is that equality of types is often neither provable nor disprovable, because the axioms of type theory don't tell you what's going on "under the hood". An analogy would be that if I don't explicitly tell you which construction of the integers I'm using in a model of mathematics built within set theory then you can never be 100% sure whether the set underlying the integers happens to conclude with the set underlying the naturals.

DayDun (Oct 23 2022 at 07:10):

What determines if a pair of types can be compared? Just the cardinality?

Kevin Buzzard (Oct 23 2022 at 07:23):

Again: if two types don't have the same cardinality then they are not equal, and if they do then it's almost certainly undecidable whether they're equal or not and hence it's not the right question.

Kevin Buzzard (Oct 23 2022 at 07:25):

If you make two different classes in the same way in a programming language and then ask whether these classes are equal, the question doesn't really make sense, it will depend on things like how the compiler actually implemented the classes. It's not a meaningful question. This isn't set theory, where extensionality gives you a built in criterion for equality of sets.

Mario Carneiro (Oct 23 2022 at 07:28):

There are also examples in the other direction, where two not-obviously equal types are provably equal in lean. These are normally things like {x : nat // x > 0} vs {x : nat // x != 0}: here the types themselves are equal, because they are the subtype function applied to two lambdas that are equal due to funext and propext

Mario Carneiro (Oct 23 2022 at 07:30):

There aren't too many examples like this, it is basically only when you give equal arguments to a type former (and hence the resulting types have to be equal because type formers are functions and obey congr_arg like everything else).

Mario Carneiro (Oct 23 2022 at 07:34):

The other kind of example is when a type former can't be injective simply by cantor's theorem:

import tactic.by_contra
import logic.function.basic

inductive foo : set Type  Type

example :  x y, x  y  foo x = foo y :=
  by_contra' H,
  exact function.cantor_injective foo (λ x y h, by_contra $ λ h', H _ _ h' h),

(This one was responsible for an unsoundness in Agda, which wanted to assume all type formers are injective.)

Last updated: Aug 03 2023 at 10:10 UTC