RFC: `@[override_repr]` attribute

Stream: lean4

[Robin Arnez]

This has come up before (see e.g. lean4#2292) but I figured I'd make this into a concrete proposal. The idea is the following:
In some cases there is a definition of a type that's convenient for proofs but at the same time is very slow to use at runtime; but there is another definition of a type that's efficient at runtime but can't be used for proofs.
One such example is an infinite list which can be defined as a function f : Nat → α where f n corresponds to the nth element of the list. However, using this definition often leads to inefficient code running in O(n^2) time where O(n) would be possible. A better definition would be:

inductive InfiniteList (α : Type u) where
  | mk (head : α) (tail : Thunk (InfiniteList α))

but there's a problem: this type isn't formally inhabited so proof world can't do anything with it. So you need to choose: proofs or efficiency? The idea is to add an attribute similar to @[implemented_by] but for inductive types, which would allow you to solve this problem:

inductive InfiniteListImpl (α : Type u) where
  | mk (head : α) (tail : Thunk (InfiniteList α))

@[override_repr InfiniteListImpl]
structure InfiniteList (α : Type u) where
  get : Nat → α

This attribute should make sure that InfiniteList doesn't use the representation provided by the structure but the representation of InfiniteListImpl; thus InfiniteList.mk and InfiniteList.get don't make any sense at this point and become noncomputable. However, you should be able to then use @[implemented_by], @[csimp] and @[extern] on these as if they were regular noncomputable functions. At the same time @[implemented_by], @[csimp] and @[extern] would then not be allowed on constructors and projections of inductives without @[override_repr].

[Robin Arnez]

@Mario Carneiro and @Cameron Zwarich you might be interested in this

[Cameron Zwarich]

I definitely think we should do something like this. A few points:

• We need some specification of how casesOn should work. I assume that general recursors (which I've started working on a bit for "ordinary" inductive types) will just never work?
• Would we actually want to support csimp for these types?
• Whatever mechanism we pick should be able to subsume the builtin support for overridden runtime types; I don't want to support two very similar paths at once. I don't expect this to be a serious problem, maybe a few types (e.g. Thunk) will need their interface to be refactored.
• Similarly, I would like the implementation of this to share as much as possible with the implementation of computed fields (after some improvements, as it is currently deficient).

[Robin Arnez]

Maybe a reasonable restriction would be to only permit structures with one field? Most builtin runtime types already fulfill this requirement, except Nat and Int which we could hardcode in the worst case.

[Robin Arnez]

Oh and another point is the syntax; should we allow @[override_repr] to only take in a single identifier or an entire term? In some cases it might be useful to be able to specify a full type term -- at the same time you could always write a def -- which is what has been done with @[implemented_by] for a long time already. One compromise I thought of was to allow the type you override from to have less parameters, so something like:

@[override_repr UInt8]
structure TestMe (n : Nat) where
  a : Fin 3
  b : Fin 3
  h : a * b < n

would work.

[Robin Arnez]

Oh and

@[override_repr True]
structure MyErased (α : Sort u) where
  value : α

would also be cool