Content-hashing declarations

Stream: mathlib4

[Johan Commelin]

Intuitively, I'm a big proponent of everything that increases the decoupling of names from lambda expressions.

[Mario Carneiro]

I think there is a meaningful intermediary here, i.e. it would not be a good idea to go "full unison" and say that names are just resolving to lambda expressions. Rather names resolve to definitions which have lambda expression bodies

[Mario Carneiro]

otherwise we don't have anywhere to hang definition unfolding heuristics

[Mario Carneiro]

But I see no innate issue with a definition having multiple names like a linux hard link

[Johan Commelin]

Mario Carneiro said:

otherwise we don't have anywhere to hang definition unfolding heuristics

You can hang those in a separate db, indexed by hashes, right?

[Mario Carneiro]

hashes of what?

[Mario Carneiro]

if you are hashing the lambda term then you would not be able to have two definitions with the same content and different metadata

[Mario Carneiro]

basically I'm saying that if we erase all the names and just look at it as a soup of nodes, then there is a node type representing expressions but there is also a node type representing definitions together with all their metadata (except the name)

[Mario Carneiro]

and constant references in expressions refer to definitions, not the body expression directly

[Mario Carneiro]

and then you can layer names on top of that and content hash to your heart's content

[Mario Carneiro]

Another case of content hashing causing problems is if you erase names in inductive types, it would make structure Foo where n : Nat and structure Bar where n : Nat the same type

[Mario Carneiro]

some things have to be "generative"

[Mario Carneiro]

in the soup of nodes picture these would be distinct nodes that have the same subnodes

[Johan Commelin]

Mario Carneiro said:

Another case of content hashing causing problems is if you erase names in inductive types, it would make structure Foo where n : Nat and structure Bar where n : Nat the same type

Is that a feature or a bug?

[Johan Commelin]

Anyway, maybe we should split this thread.

[Notification Bot]

15 messages were moved here from #mathlib maintainers > Deprecating field names by Mario Carneiro.

[Mario Carneiro]

On the subject of nominal types, the #leantt formalization does not use nominal inductive types, it has a $\mu T:F. K$ term constructor for inductive types instead of an inductive declaration form

[Mario Carneiro]

which has the side effect that you can prove the equality of types like Foo and Bar

[Mario Carneiro]

And the way you can "fix" that is to put the name in the constructor, i.e. $\mu[Foo]T:F.K$, or an auto-incrementing counter

[Johan Commelin]

Maybe I'm naive, but to me it seems that names are strictly an elaborator feature.
I don't see harm in being able to prove that Foo and Bar are equal.

[Mario Carneiro]

The standard argument for newtypes is things like structure Meters where n : Real and structure Feet where n : Real

[Mario Carneiro]

if I have such types and have a function def tooBig : Meters -> Bool it should be a type error to pass Feet.mk 37 to it

[Mario Carneiro]

Put another way, a type is not just a set of values but also an interpretation of those values, even though only the set of values is explicitly expressed in the syntax. If the interpretation changes then using a different type puts guard rails avoiding accidental misinterpretation

[Mario Carneiro]

Mario Carneiro said:

And the way you can "fix" that is to put the name in the constructor, i.e. $\mu[Foo]T:F.K$, or an auto-incrementing counter

When I call it an auto-incrementing counter it makes this sound rather unnatural, but there are other ways of presenting type declarations that are more like variable bindings, and it should not be any surprise that when you are in a scope x : Nat, y : Nat |- ..., x and y do not magically become equal simply because they have the same type. They are different variables and the type theory respects this, and in the underlying system this is accomplished using de bruijn variables, i.e. "an auto-incrementing counter". Note that this really has nothing to do with the names x and y, rather just that they are different variables because the declaration operation was performed twice.

[Johan Commelin]

But that auto-incrementing counter does imply that you need some global entity that knows about all declarations out there, and then assigns them a "de bruijn index".

[Johan Commelin]

Mario Carneiro said:

if I have such types and have a function def tooBig : Meters -> Bool it should be a type error to pass Feet.mk 37 to it

Can't it be enough from a UX POV to have this be a type error at the elaboration level?

[Mario Carneiro]

Johan Commelin said:

But that auto-incrementing counter does imply that you need some global entity that knows about all declarations out there, and then assigns them a "de bruijn index".

That depends on how you conceptualize it, I suppose. You need them to be recognized as distinct, but there are ways to get that without central coordination points, e.g. UUIDs

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro said:

if I have such types and have a function def tooBig : Meters -> Bool it should be a type error to pass Feet.mk 37 to it

Can't it be enough from a UX POV to have this be a type error at the elaboration level?

:shrug: I think all typing can be done at the elaboration level

[Mario Carneiro]

but if you do that then it's not clear how you've done anything other than shift the burden of checking to a different subsystem and still having nominal semantics

[Johan Commelin]

Well, I'm not doing all typing at the elaboration level.

My main application is mathematical consistency, proof correctness. Plugging Feet.mk 37 into tooBig will not give you a proof of False.

[Johan Commelin]

Mario Carneiro said:

That depends on how you conceptualize it, I suppose. You need them to be recognized as distinct, but there are ways to get that without central coordination points, e.g. UUIDs

But then you lose the feature that if person Foo defines Nat in Greece in 370 BC and person Bar defines Nat in India in 530 BC, that they automatically end up with the same Nat.
And so now person Foo can't use theorems by Bar, when they discovers them.

[Mario Carneiro]

yeah I think that is by design, that's the same thing you would get if both the ancient Greek and Indian lean users used the inductive command separately

[Mario Carneiro]

Johan Commelin said:

My main application is mathematical consistency, proof correctness. Plugging Feet.mk 37 into tooBig will not give you a proof of False.

It can lead to proofs by explosion though

[Mario Carneiro]

I think it is more appropriate to have separate types but use something HoTT-styled to mediate the various ways that the types can be identified. Just because they have the same structure doesn't mean the "identity function" induced by this is the right isomorphism to apply to turn Greek mathematics into Indian mathematics

[Mario Carneiro]

Nat is a special case because it has no nontrivial isomorphisms

[Aaron Liu]

Mario Carneiro said:

Nat is a special case because it has no nontrivial isomorphisms

What kind of isomorphisms?

[Kevin Buzzard]

Does every inductive have no nontrivial automorphisms if by "automorphism" you been "constructor-preserving map"?

[Aaron Liu]

Then Bool would seem to have Bool.not

[Mario Carneiro]

I think kevin means mapping each constructor to the corresponding constructor

[Aaron Liu]

Preserves constructors up to renaming

[Kevin Buzzard]

That doesn't preserve the constructor Bool.true. This is why your question is pertinent!

[Mario Carneiro]

and I think the answer is yes

[Aaron Liu]

What about Prod.swap?

[Aaron Liu]

It preserves the only constructor Prod.mk

[Anatole Dedecker]

No, because this takes two arguments in order

[Mario Carneiro]

(I also assume that preserving a constructor means mapping the arguments in the same order :stuck_out_tongue_closed_eyes: )

[Aaron Liu]

Actually, what does "preserves constructors" even mean?

[Mario Carneiro]

a homomorphism of Nat is a function f such that f zero = zero and f (succ n) = succ (f n)

[Mario Carneiro]

and since this has clauses mirroring those of a definition by recursion, you can prove by induction that it's the identity function

[Mario Carneiro]

so this is true for all inductive types

[Mario Carneiro]

This is interesting, it's a kind of "rigidity" I associate with ZFC set theory, "junk theorems" and all that

[Aaron Liu]

Mario Carneiro said:

a homomorphism of Nat is a function f such that f zero = zero and f (succ n) = succ (f n)

So how does this definition apply to Prod (or Prod Nat Nat if you want to be concrete)?

[Aaron Liu]

Would it just be f (a, b) = (a, b)?

[Mario Carneiro]

a homomorphism of h : A x B -> A' x B' relative to morphisms f : A -> A', g : B -> B' is a function such that h (a, b) = (f a, g b)

[Yaël Dillies]

(misread)

[Mario Carneiro]

the "relative to" part is because Prod is a parameterized type

[Mario Carneiro]

but if f and g are identity functions then you can prove by recursion that h is also an identity function

[Aaron Liu]

What about arrow types?

[Mario Carneiro]

I think you need isomorphisms to do contravariant things, a homomorphism of f : (A -> B) -> (A' -> B') over a : A ~= A' and b : B ~= B' satisfies f g = fun x => b (g (a^-1 x))

[Aaron Liu]

What about universe types, like Prop and Type? Those don't seem to have any constructors.

[Mario Carneiro]

HoTT can basically compute these expressions for any type former

[Mario Carneiro]

I was just getting to that: the universe is an example of a non-rigid type since it is not inductively defined. It actually has nontrivial isomorphisms

[Mario Carneiro]

and those isomorphisms are precisely the things that e.g. interchange Meters and Feet

[Aaron Liu]

So what's a homomorphism of Type have to satisfy?

[Mario Carneiro]

In HoTT, it would be a function F : Type -> Type such that (A = B) ~= (F A ~= F B)

[Mario Carneiro]

that really doesn't make a lot of sense without HoTT though, since applied to the identity function it's literally univalence

[Mario Carneiro]

but the simple consequence would be that isomorphic types are mapped to isomorphic types

[Mario Carneiro]

(Don't quote me on that one though, I haven't actually worked it out)

[Kevin Buzzard]

Type is a category and you could ask for an equivalence from Type to itself (or slightly more ridiculously for an isomorphism). One such isomorphism could be "swap Meters and Feet and fix everything else" although of course there is a model of Lean where this is the identity and another model where it's not ;-)