RFC: `@[override_repr]` attribute

Proposal

Add an attribute that allows overriding the representation of an inductive type. All projections, constructors and casesOn should then become noncomputable by default; this should be overridable by @[implemented_by] and friends though. However, @[implemented_by] and friends should not work when the inductive type wasn't declared with @[override_repr].

Motivation:

In some cases there are two representations of a type: one that works well for proofs and another that works well at runtime but doesn't allow for proofs. Infinite lists are an example of this:

-- works well for proofs but inefficient
def InfiniteList (α : Type u) := Nat → α

-- works well at runtime but is formally an empty type
inductive InfiniteList (α : Type u) where
  | cons (x : α) (l : Thunk (InfiniteList α))

The @[override_repr] attribute would then allow specifying a "model implementation" of a type for proofs and using another type for runtime:

inductive InfiniteListImpl (α : Type u) where
  | cons (x : α) (l : Thunk (InfiniteList α))

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

Since InfiniteListImpl is now used as the representation of InfiniteList, the usual implementation of InfiniteList.mk and InfiniteList.get doesn't make any sense anymore (since it relied on the representation being the one of InfiniteList). Thus they should become noncomputable by default. However, you should then be able to override this by specifying your own implementation:

def InfiniteListImpl.get {α : Type u} (l : InfiniteListImpl α) (n : Nat) : α :=
  match n, l with
  | 0, .cons x t => x
  | k + 1, .cons x t => t.get.get k

unsafe def InfiniteList.getImpl {α : Type u} (l : InfiniteList α) (n : Nat) : α := (unsafeCast l : InfiniteListImpl α).get n

attribute [implemented_by InfiniteList.getImpl] InfiniteList.get

Overriding projections (and constructors) only makes sense with @[override_repr] though; as such it should be forbidden for regular inductives and point to @[override_repr]:

structure InfiniteList (α : Type u) where
  get : Nat → α

unsafe def InfiniteList.getImpl {α : Type u} (l : InfiniteList α) (n : Nat) : α := (unsafeCast l : InfiniteListImpl α).get n

/-
invalid implemented_by: target is a projection of InfiniteList but InfiniteList doesn't have an `@[override_repr]` attribute.
-/
attribute [implemented_by InfiniteList.getImpl] InfiniteList.get

Another use case is a simpler definition of Erased that has good reduction properties:

@[override_repr True]
structure Erased (α : Sort u) where
  out : α

Specifying True here should make the representation into the same of True: ◾ (erased). The behavior should then also match what you'd expect from Erased: Erased.out is noncomputable and Erased.mk would be noncomputable but is erased anyways so works similarly to proofs.

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/RFC.3A.20.60.40.5Boverride_repr.5D.60.20attribute/with/530131350

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.