RFC: Types with holes

Stream: lean4

[Jakub Nowak]

I was thinking that maybe the following language construct might be useful.

Given type with parameters like Foo : Nat → Type the term Foo ?n would be equivalent to (n : Nat) × Foo n, but, with some additional properties. The point is to think about Foo ?n as Foo n for some arbitrary n. So instances of Foo ?n should behave identically to instances of Foo n. The properties I think we would want from it to achieve this (there might be more) are:

• a : Foo ?n is coercible to Foo a.1;
• Foo n is coercible to Foo ?n;
• Both coercions should happen implicitly and be essentially "invisible" to the user;
• Dot notation for Foo ?n works just like for Foo n.

We might also want some kind of syntax to be able to refer to parameters of Foo ?n, e.g. a.?n.

One additional design decision I am unsure about, is that (n : Nat) × Foo n forces n to be part of runtime representation. We might want to avoid it, though I am unsure about how to do that, maybe use (n : Erased Nat) × Foo n.out instead? In which case we would want, for a : Foo ?n, a.?n to return (noncomputable) Nat, instead of Erased Nat.

I came up with this idea because of #graph theory > How to return Walk. Basically, such a feature would mean I could replace (v : V) × G.Walk v v with G.Walk ?v ?v and get all the nice UX-improving properties I listed above.
Another place this could potentially be useful is that there's a common problem of coercion between SimpleGraph.Subgraph and SimpleGraph. Instead of SimpleGraph.Subgraph we could use G' : SimpleGraph (?verts : Set V(G)) with some G' ≤g G property, which could potentially solve some issues, because now G' is "almost" SimpleGraph. It's "almost" SimpleGraph, because it's a SimpleGraph with a hole, but the point of defining types with holes as a language construct is that instance of SimpleGraph with hole should behave exactly the same as instance of SimpleGraph.

One other place this could be useful is that we could define Array α to be Vector α ?size, thus avoiding code duplication between Array and Vector.

I believe other people can come up with more example of where having to juggle type parameters leads to DTT hell. This feature has a potential of helping in all these cases too.

[Jakub Nowak]

Maybe someone is aware of a similar feature existing in some other language?

[Mirek Olšák]

I don't get this, how does it differ from standard implicit arguments?

structure Foo {n : Nat} where
  a : Fin n
  h : n > 0

#check (Foo)
#eval Foo.mk (2 : Fin 5) (by grind)

This definitely does NOT make sense as an extension to the kernel logic, perhaps as yet another syntax sugar on top of something but then it would help if you write on top of what exactly.

[Jakub Nowak]

Mirek Olšák said:

I don't get this, how does it differ from standard implicit arguments?

structure Foo {n : Nat} where
  a : Fin n
  h : n > 0

#check (Foo)
#eval Foo.mk (2 : Fin 5) (by grind)

My proposition is unlike implicit arguments. Types with holes don't make much sense when used as arguments of definitions, because you can always "pass" argument as an implicit argument of definition. But the following doesn't work with implicit arguments:

def mkFoo (x : α) : Foo := ...

While you can have:

def mkFoo (x : α) : @Foo ?n := ...

Mirek Olšák said:

This definitely does NOT make sense as an extension to the kernel logic [...]

I don't think we need to extend kernel logic to implement this. Except maybe «Both coercions should happen implicitly and be essentially "invisible" to the user» part?

[Jakub Nowak]

(deleted)

[Mirek Olšák]

Write more basic examples of Lean code with your features. It is hard to follow what you want.

[Eric Wieser]

I think you're asking for

instance badCoeSort.{u, v} {α : Type u} : CoeSort (α → Type v) (Type max u v) where
  coe := Sigma

def wat : Vector Int := ⟨3, #v[1, 2, 3]⟩

instance badCoeSortTrans.{u, v} {α : Type u} {β : Type v} [CoeSort β (Type w)] : CoeSort (α → β) (Type max u w) where
  coe f := Σ a, (f a)

def wat2 : Vector := ⟨Int, 3, #v[1, 2, 3]⟩

[Jakub Nowak]

Eric Wieser said:

I think you're asking for

instance badCoeSort.{u, v} {α : Type u} : CoeSort (α → Type v) (Type max u v) where
  coe := Sigma

def wat : Vector Int := ⟨3, #v[1, 2, 3]⟩

instance badCoeSortTrans.{u, v} {α : Type u} {β : Type v} [CoeSort β (Type w)] : CoeSort (α → β) (Type max u w) where
  coe f := Σ a, (f a)

def wat2 : Vector := ⟨Int, 3, #v[1, 2, 3]⟩

Hm, kinda? But that's just small portion. Dot notation for wat (e.g. #check wat.push) doesn't work. And given function foo : Vector Int n → β foo wat should also work. So basically coercion from xs : Sigma (Vector Int) to Vector Int xs.1.

[Jakub Nowak]

I've modified my code from #Is there code for X? > bipartite iff does not contain an odd cycle @ 💬 to show how I would imagine this feature. I've commented parts of the original code for comparison.
There's some bug with copy-pasting long code here in zulip, so here's a link: https://live.lean-lang.org/...

[Jakub Nowak]

Hm, maybe, what I would want is for the following code to work, i.e. Lean should automatically deduce the type for mkFoo, like in mkFoo':

structure Foo (n : Nat) where
  a : Fin n
  h : n > 0

def mkFoo (x : Nat) :=
  match x with
  | 0 => Foo.mk (n := 2) 0 (by simp)
  | x + 1 => Foo.mk (n := 4) 0 (by simp)

def mkFoo' (x : Nat) : Foo (match x with | 0 => 2 | _ + 1 => 4) :=
  match x with
  | 0 => Foo.mk (n := 2) 0 (by simp)
  | x + 1 => Foo.mk (n := 4) 0 (by simp)

[Mirek Olšák]

I see, this is the eternal dilemma between bundled & unbundled datastructures. By the way, was it you who was saying that Finset is not needed as a bundled "Set which is finite" because it can be always written separately :wink: ? Here, working with a bundled Walk seems better (but I get the difference, the bundled Walk carries data). I indeed don't think you want types with match -- that leads to most of DTT hell.

Regarding the Walk code you linked in live lean: You can add a coercion (like Eric said), something like

instance : CoeOut (G.Walk u u) (Σ u, G.Walk u u) where
  coe x := ⟨u, x⟩

With this, you don't have to write ⟨_, cycle⟩, and it is sufficient to write cycle.
I don't know how you imagined coercion from Walk.nil to work since it is very non-obvious that you want to store u inside.
Regarding dot notation, it is a little hack on itself, and I am rather impressed how well it works (unfolds definitions). People usually accept writing some extra .2 inside.

[Jakub Nowak]

Here it's index parameters vs structure field. Which is e.g. G.Walk u v vs G.Walk.

That's I think very much different than bundled vs unbundled. Which is e.g. Finset α vs (s : Set α)+s.Finite as separate arguments.

Unless there's a connection between the two I'm not seeing?

[Aaron Liu]

isn't that the same thing

[Aaron Liu]

if you have it as structure field then compared to having it as an index you've bundled in the index into the structure

[Jakub Nowak]

Hmm, you're kinda right. There is some connection, but I wouldn't say it's the same.

Let's say you have foo : Finset α. Then "unbudling" it would mean defining first foo : Set α, and then foo_fin : foo.Finite.

Let's say you have bar : G.Walk'. By G.Walk' I mean the type of walks without index parameters for first and last vertex. "Unbudling" bar would mean first defining bar_u : V and bar_v : V, and then defining bar : G.Walk bar_u bar_v.

In the first case, you first write more generic definition, and then prove desired property. In the latter case you first have to define indices separately, and only then you can state the definition.

[Mirek Olšák]

Jakub Nowak said:

Hmm, you're kinda right. There is some connection, but I wouldn't say it's the same.

Depending on the definition of "same" :slight_smile:

[Mirek Olšák]

The difference is that Walk u u is a Type, and Set.Finite s is a Prop.

[Mirek Olšák]

As long as you treat Prop and Type the same way (and Lean's syntax does that to a great extent), it is the same.

[Jakub Nowak]

Sorry, I think I've lost you. What are you referring to now?

[Jakub Nowak]

I was explaining that bundling type parameters and bundling properties are different things.

[Mirek Olšák]

Oh, I was saying that bundled "finite set", and bundled "walk with arbitrary endpoints" are kind of the same.

[Jakub Nowak]

Ah, I think I've got your point. Hm, you're right. Walk u u and Set.Finite s are in fact the same thing for the purpose of this discussion.

[Jakub Nowak]

Hm, I think we've got offtopic here. The main discussion of this topic was how to handle e.g. Walk u u when u cannot be easily defined.

[Mirek Olšák]

I didn't see such case in the linked example in live lean.

[Jakub Nowak]

Another idea I've got is that given

private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    G.Walk ?w ?w :=
  match suf with
  | .nil => ⟨u, Walk.nil⟩ -- unreachable
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        ⟨v, cycle⟩
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (pref.concat hAdj) suf'

Lean could automatically define the following two definitions:

private def odd_cycle_of_odd_walk_step_aux_w [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) : V :=
  match suf with
  | .nil => u
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        v
      else
        odd_cycle_of_odd_walk_step_aux_w pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step_aux_w (pref.concat hAdj) suf'

private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    G.Walk (odd_cycle_of_odd_walk_step_aux_w pref suf) (odd_cycle_of_odd_walk_step_aux_w pref suf) :=
  match suf with
  | .nil => Walk.nil
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        cycle
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (pref.concat hAdj) suf'

But that's very similar to what I described here, and you're saying this would likely lead to DTT hell.

[Mirek Olšák]

What do you mean with unreachable?

[Mirek Olšák]

If you can prove that the case cannot happen, you can use False.elim there.

[Jakub Nowak]

Ah, it doesn't matter, it's a leftover from where I copied this code from. This case doesn't happen, but with some additional assumptions that are part of the theorem about this definition but not the definition itself.

[Mirek Olšák]

I would indeed prefer to use bundled walk here. What is wrong with bundled walks (Sigma type) except you sometimes have to insert .2?

[Jakub Nowak]

That and the fact that dot-notation isn't working.

[Mirek Olšák]

It is when you insert .2

[Jakub Nowak]

Hm, true.

[Jakub Nowak]

I think that having to insert .2 sometimes is a thing that's worth trying to improve. This is an instance of manual coercion. I found things like that slowing me down when writing proofs and it's an additional thing I have to keep track of in a limited context window of my brain.

[Mirek Olšák]

I kind of get it, you could ask for a fix in two places

• (a) You could want Walk to be unbundled by default, or to have an unbundled alternative. This would require changing some graph theory in Mathlib, I suppose there are other places where unbundled walk is better, so it needs either (a.1) convince others that bundled walks are better, or (a.2) create a parallel structure for bundled walks.
• (b) Smoother transition between bundled & unbundled datastructures. If this can be done well, it could help many people, however doing it well is a hard preliminary to accomplish. Then you should take a more principled approach, look at pain points that occur in practice in more general than in your specific use case. Algebraic structures (they are currently mostly unbundled, and done with typeclasses), finite sets, ... I don't know how to do it well, and so far, I am not really convinced by Walk ?w ?w.