Should I avoid using HEq?

Stream: new members

[aron]

When I first dived into Lean I got very excited about dependent types and put values in all of my types. Unfortunately this led to intractable messes of casts and type conversion functions in my theorems and inductives when trying to express propositions about relationship of various types which are not definitionally equal. E.g. Vec (4+2) a = Vec (3 * 2) a. So I removed the values from all my data-carrying Types :cry:

Afterwards however I came across heterogenous equality. Although I've seen it mentioned a few times (can't remember exactly where, sorry) that heterogenous equality is quite hairy in Lean so to avoid it whenever possible.

I'd like to understand a bit more about this. Why is HEq fiddly? Is it indeed recommended to stay away from it and stick to making my data-carrying types "dumb" so values of that type can always be compared with Eq? Are there any use cases HEq _is_ recommended for? Thanks :folded_hands:

[Riccardo Brasca]

The short answer is that heterogeneous equality is not well behaved and it's usually better to avoid it (for example there is no functional extensionality).

[Riccardo Brasca]

Usually you should even avoid equality of types: you can think that two types are literally the same thing (like Nat and ℕ) or totally distinct. So ignore the fact that you can prove A = B if the proof is not rfl.

[Aaron Liu]

The reason HEq is so bad is that it says the types are equal when usually what you want is that you have an indexed type family and you want to say the indices are equal

[aron]

@Aaron Liu in my use cases I usually make the type index surface some property of the value that I care about. So no it's not about asserting that the indices are equal but indeed that the values are equal. If the values are equal their types will be equal too, but often not definitionally so.

[aron]

@Riccardo Brasca sorry can you expand a little more on what "not well behaved" means? And what functional extensionality means in this context?

[Riccardo Brasca]

For example the analogue of docs#congr is false for heterogeneous equality.

[aron]

And @Riccardo Brasca yeah I usually don't care about asserting equality between types – it only comes up because I want to equate two values of types that I know are the same, but Lean doesn't (not without me proving it first)

[Riccardo Brasca]

This is what I mean: it's much better to think that type that Lean doesn't realize are equal are actually distinct.

[aron]

Right. But... that means it's practically impossible to use dependent types for data. Which... means you're basically forbidden from using dependent types – at least for anything other than props

[aron]

Which feels like being told Christmas is cancelled :sob:

[Riccardo Brasca]

I am not sure I understand what you mean here. For sure sometimes you have to introduce equivalences that on paper you don't see, but it's not at all impossible

[Riccardo Brasca]

For example it is surely possible to work with lists

[Kenny Lau]

aron said:

you're basically forbidden from using dependent types

well, we have tried very hard to use (better imo) alternatives exactly because of this. This is exactly the reason why 3-5=0 and 1/0=0. We've learnt that dependent types are bad (for good reasons) and we've tried very hard to make everything independent.

What is the appeal of dependent types to you?

[Aaron Liu]

aron said:

Aaron Liu in my use cases I usually make the type index surface some property of the value that I care about. So no it's not about asserting that the indices are equal but indeed that the values are equal. If the values are equal their types will be equal too, but often not definitionally so.

Can you give a #mwe?

[Weiyi Wang]

:smiling_face_with_tear: I had a similar experience trying to use types like this. In the end I was able to prove what I wanted but I ended up with weird lemma like this

[suhr]

aron said:

Right. But... that means it's practically impossible to use dependent types for data. Which... means you're basically forbidden from using dependent types – at least for anything other than props

Structures can have Prop fields, so you can have dependent types for some data. If you want more dependent types though, then you should use a HoTT prover rather than Lean.

[Philippe Duchon]

Riccardo Brasca said:

For example the analogue of docs#congr is false for heterogeneous equality.

Out of curiosity, what would that analogue be? (the documentation says it would be false for dependent types but I'm not even sure if that's the same issue)

[Kenny Lau]

@Philippe Duchon I would guess that the following is consistent but unprovable?

axiom dCongr {A B C D : Type} (f : A → C) (g : B → D) (a : A) (b : B)
  (h₁ : f ≍ g) (h₂ : a ≍ b) : f a ≍ g b

(from h1 and h2 you can deduce that (A -> C) = (A -> D), but it is independent (of Lean) that this implies C = D)

[Robert Maxton]

aron said:

Which feels like being told Christmas is cancelled :sob:

I completely understand and had much the same reaction.

[Robert Maxton]

Using categorical idioms helps here; you still have to avoid type equality, but you can have heavily dependently typed data without tearing your hair out, by instead keeping track of the precise sense in which two objects are 'equivalent' and using that instead. In fact, you can prove that this is precisely the reason that HEq is 'badly behaved': @HEq α β a b amounts to a proof h that α = β, packaged with a proof that cast h a = b, and since Lean has proof irrelevance you lose everything about the proof h you used other than its type. In particular, that means that once you go from e.g. C = D in @Kenny Lau 's example to (A -> C) = (A -> D), you can't go back; so HEq is erasing important context behind your back if you use it carelessly.

[Robert Maxton]

Kenny Lau said:

What is the appeal of dependent types to you?

While I can't speak for aron, personally it's a combination of "ultimate form of type safety" which itself is a big part of the appeal of Lean as a programming language as a whole; the theoretical power and convenience of having extremely precise type information and proof-by-reflection/proof-by-case-analysis; and the simple fact that they constantly come up naturally any time you start trying to build any kind of automatic proof-of-correctness-checker in many, many domains, so I certainly came to it with quite a lot of built-up instances of "man I really wish this language allowed dependent types" in my history.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The solution to all issues with HEq, btw, is "telescopic equality" (also called PathP in the cubical context). It was described by Chung-Kil Hur and amounts to using equalities of dependent pairs ⟨i, a⟩ = ⟨j, b⟩, where i, j : A, B : A → Type, a : B i, b : B j. This implies HEq a b, but crucially keeps around the proof of index equality that cannot be recovered from B i = B j. I started some extremely simple experiments with this, but it would be amazing to see a proper library.

[Jakub Nowak]

I can't find any practical example of where Vec would be better to use than List. Instead of v : Vec n α, you can just have l : List α and a proof l.length = n. And you can even state some less trivial property about the length then just equality.

[Aaron Liu]

I am using heavily dependently typed terms because I think they are the simplist way to express the ideas I am transcribing proofs about in Lean (that is simply typed lambda calculus)

[Aaron Liu]

I think I have been using some of the ideas @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 mentioned ("telescopic equality") in working with my dependent types also because it seemed to be the simplest way to express my ideas in Lean

[Jakub Nowak]

I was also formalizing simply typed lambda calculus in Lean with dependant types, it looked great while doing simple stuff, but turned out too be hard to work with when I moved to more complicated algorithms.

[Ilmārs Cīrulis]

Does HoTT make such use of dependent types easier?

[metakuntyyy]

I recall a comment made by @Kevin Buzzard where he said that he uses lean because it has dependent types and quotients. Meanwhile every topic I've witnessed boils down to "Avoid dependent types".

Which is absolutely hilarious, it's like saying: "A is the best because it has property b and property b is bad."
I guess the only real uses for dependent types is something that goes into prop.

import Mathlib

theorem exampleGoodDepType : ∀ (n : ℕ) , n ≤ n * n := sorry

If I understand correctly, exampleGoodDepType are the only "good" dependent types?

[Aaron Liu]

Dependent data is difficult because of all the coherence you need to show

[Aaron Liu]

Dependent proofs however are always definitionally coherent

[metakuntyyy]

So is the "only good feature" types that map into prop? How do simple type systems express exampleGoodDepType then?

[Kevin Buzzard]

metakuntyyy said:

I recall a comment made by @Kevin Buzzard where he said that he uses lean because it has dependent types and quotients. Meanwhile every topic I've witnessed boils down to "Avoid dependent types".

The intent of this comment has been twisted a little. I use dependent types all the time, there's nothing wrong with them. What's wrong is asking pathological questions about them such as asking if two dependent types are equal, or using HEq etc. I stay away from the pathological questions and whilst I need dependent types have never explicitly used HEq in my work; I don't need that because it doesn't come up in e.g. the proof of FLT.

[Aaron Liu]

HEq is fine if you know additionally that the indices are equal

[Aaron Liu]

that's why it's used internally by the cases tactic

[Aaron Liu]

but if you don't know that then it tells you nothing

[metakuntyyy]

But what would a simple example be. I guess the question to @Kevin Buzzard is what theorem or definition makes him happy that he's doing in lean and not in a simply typed language. The definition can be as simple as possible.

And to @Aaron Liu what would one simple example be where HEq is fine. It reminds me of #mathlib4 > Mathlib: the Missing Manuals where @Anne Baanen is working on updating the documentation according to the divio design.

I'm in favour of having a good compiled document that describes just design decisions to help one understand topics better. However I must note that documentation has massively improved in the last year or so. I've read the full reference manual on my drive home. It was actually a pleasant read as it was a very nicely compiled document with about 200 pages worth of information that I otherwise wouldn't get.

[Aaron Liu]

Here's an example where HEq is useful https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Puzzle.3A.20Decidable.20HEq/near/536803714

[metakuntyyy]

Thanks, that's helpful.

[Kevin Buzzard]

The killer example for dependent types is homological algebra. Here we have abelian groups $A_i$ (or objects in a category) indexed by the naturals or integers $i$, and with maps $A_i\to A_{i+1}.$ Our dependent type problems were solved by just defining $d_{ij}:A_i\to A_j$ for all $i,j$ and demanding that $d_{ij}=0$ if $j\not=i+1$. This is a bit of a hack but it has worked absolutely fine (we have a usable theory of group cohomology, I know this because I've been using it in the class field theory repo).

[metakuntyyy]

Very nice. Thank you both for your answers.

[metakuntyyy]

Do you know where I can find the code? I'd like to study it a bit.

[Aaron Liu]

Well docs#HomologicalComplex is the type

[Patrick Nicodemus]

Ilmārs Cīrulis said:

Does HoTT make such use of dependent types easier?

Understanding HoTT should make it easier in some ways to use dependent types in Lean, but the same solutions should be easier in Lean than in HoTT because of proof irrelevance. Proof irrelevance makes some things easier and some things harder: in HoTT if A, B are types and $p, q : A = B$ then to prove that cast p x = cast q x it may be necessary to prove p=q. In Lean you get this for free by proof irrelevance. It would be possible to translate many HoTT constructions into Lean, many of them would simplify or become degenerate but many would still be useful.

Robert Maxton says "so HEq is erasing important context behind your back if you use it carelessly", which is true, but as long as you don't use it "destructively" (i.e. you remember the original equality and you deploy it when necessary rather than forgetting it by weakeneing it to heterogeneous equality) it should be okay.

[Patrick Nicodemus]

When Robert Maxton says:

Using categorical idioms helps here; you still have to avoid type equality, but you can have heavily dependently typed data without tearing your hair out, by instead keeping track of the precise sense in which two objects are 'equivalent' and using that instead.

this is true in some sense but taken literally it is false because two types are equal in at most one way and so one does not have to keep track of how or why they are equal. so this point needs some clarification.

One point which is relevant is that if P : A -> Type and p : a = b then P a = P b but you probably still need to keep around the theorem that a = b.

That is, if x : P a and y : P b, assuming you prove that casting x across p is equal to y, you might want to work with heq x y instead. From this you can recover that P a = P b, but P need not be injective in general, so you cannot necessarily recover p: a = b from this, and so you have really lost something in that reasoning step.

(Whoops, I guess this is really what Wojciech said earlier, that one should keep around the proofs of equality on indices for the dependent types - sorry for the redundancy.)

[Eric Rodriguez]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

The solution to all issues with HEq, btw, is "telescopic equality" (also called PathP in the cubical context). It was described by Chung-Kil Hur and amounts to using equalities of dependent pairs ⟨i, a⟩ = ⟨j, b⟩, where i, j : A, B : A → Type, a : B i, b : B j. This implies HEq a b, but crucially keeps around the proof of index equality that cannot be recovered from B i = B j. I started some extremely simple experiments with this, but it would be amazing to see a proper library.

I think @Eric Wieser worked on something like this before