RFC: `@[override_repr]` attribute

[Rob23oba]

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.

[nomeata]

Thanks for the RFC! Something like this is on my wishlist as well.

I wonder if we can do without unsafe here; an equivalent to csimp would be nice. What if you first register the whole type as noncomputable, then define an equivalence to another type (back and forth with proofs, like Equiv), and then tell the compiler to make these conversation functions casts. Then one can add csimp lemmas for the existing noncomputable functions on the model type. Would that work for your use cases?

[Rob23oba]

For these use cases, mathlib could perhaps define:

import Mathlib.Logic.Equiv.Defs

def WithReprImpl (α : Sort u) (repr : Sort v) (_eqv : α ≃ repr) := repr

@[override_repr WithReprImpl]
structure WithRepr (α : Sort u) (repr : Sort v) (eqv : α ≃ repr) where
  value : α

variable {α : Sort u} {r : Sort v} {eqv : α ≃ r}

unsafe def WithRepr.toReprImpl (x : WithRepr α r eqv) : r := unsafeCast x
unsafe def WithRepr.ofReprImpl (x : r) : WithRepr α r eqv := unsafeCast x

@[implemented_by WithRepr.toReprImpl] def WithRepr.toRepr (x : WithRepr α r eqv) : r := eqv x.value
@[implemented_by WithRepr.ofReprImpl] def WithRepr.ofRepr (x : r) : WithRepr α r eqv := ⟨eqv.symm x⟩

def WithRepr.mkImpl (x : α) : WithRepr α r eqv := .ofRepr (eqv x)
def WithRepr.valueImpl (x : WithRepr α r eqv) : α := eqv.symm x.toRepr

@[csimp] theorem WithRepr.mk_eq_mkImpl : @mk = @mkImpl := by funext α r eqv x; simp [mkImpl, ofRepr]
@[csimp] theorem WithRepr.value_eq_valueImpl : @value = @valueImpl := by funext α r eqv x; simp [valueImpl, toRepr]

But there are cases where this doesn't work (the examples I've provided above) that need to be supported directly.

[datokrat]

@nomeata's suggestion could be generalized to use cases such as Erased if instead of an equivalence, only an arbitrary map from the kernel's representation to the internal representation is required.

Worked example for `Erased`

@[no_repr] -- makes all of the auto-generated functions noncomputable even before @[override_repr]
structure Erased (α : Type u) where
  out : α

-- In this proposal, @[override_repr] is attached to a function mapping the "kernel type"
-- to its intended internal representation.
-- The provided definition can be noncomputable, but the compiler will automatically provide an
-- implementation that is compiled to the identity.
@[override_repr]
noncomputable def Erased.toImpl {α : Type u} (x : Erased α) : PUnit

-- Moreover, a computable map into the reverse direction, also implemented by `id`, will be auto-generated:

-- info: implToQuot : {α : Type u} (x : PUnit) -> (∃ a, toImpl a = x) -> Quot (fun a b => toImpl a = toImpl b)
#check Erased.implToQuot

@nomeata's extension would also make it possible to safely create a version of Mathlib's Shrink, which "shrinks" a type into a lower universe given a nonconstructive proof that the type is small enough, where the shrinking and unshrinking operations are both computable (and compiled to id).

[Rob23oba]

Hmm that's also an interesting idea; I guess the idea is similar to the WithRepr except the ofRepr / toRepr part is handled for you (that you then use csimp later to implement constructors and projections). Kinda funny since @zwarich questioned whether csimp should even be supported (I guess the answer is yes?)
Some questions:

1. What if you wrote

   def funnyFunction (x : Erased Nat) : List (Erased Nat) := [x]

   in between the no_repr and override_repr? Should this simply be rejected in the sense of "Erased doesn't have a representation"?
2. What about InfiniteList? There, you can't really write a toImpl function that isn't unsafe (since InfiniteListImpl isn't inhabited).
3. What about writing @[override_repr] in a different module? Should this be prohibited? (probably)

Otherwise, this idea is quite nice because you don't need to unsafeCast yourself (and in particular often don't need unsafe at all) and it's simpler to specify the override than with my WithReprImpl above.

[zwarich]

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

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

This is implicitly assuming that the compiler can't exploit a type (or individual constructor) being uninhabited in its representation choices. Edit: I guess the assumption is technically being made by the unsafe code, not the override_repr itself.

[Rob23oba]

You're right; but Lean doesn't have support for coinductive types and you certainly want to be able to use such a representation. I guess if it would exploit this then either:

1. Anything hidden behind a Thunk or a function wouldn't be considered
2. It uses the original "kernel type" (InfiniteList) to make such judgments.

[sgraf812]

FWIW, I think a "safe" implementation could be achieved by axiomatizing a wrapper around Thunk called Later together with the "usual" applicative instance and the Löb induction/guarded fixpoint operator gfix : (Later α -> α) -> α: https://github.com/sgraf812/abs-den.lean/blob/3afc0c5532ef85f5056da8437dfdd30722224937/igdtt/IGDTT/Axioms.lean
I don't think the compiler would be prone to peeking into the definition of Later as it would be prone to reasoning about Thunk.

My axiomatization is often enough for simple guarded recursive programs. Plus, you could justify every such axiom by providing a proof in the model of guarded domain theory. (Eliminating the later modality in a finite way is still a safety issue, though; every use of unsafeForce in a function such as Stream.take must be audited.)

Unfortunately last time I tried I encountered some strange segfaults. Perhaps it's better with the new compiler.

[datokrat]

Responding to #9508 (comment):

1. What if you wrote def funnyFunction (x : Erased Nat) : List (Erased Nat) := [x]
   in between the no_repr and override_repr? Should this simply be rejected in the sense of "Erased doesn't have a representation"?

In my opinion yes, because this behavior feels consistent with the fact that I can't use a noncomputable function in computable code even if I later used csimp/implemented_by. I suppose this helps that things are compiled in order.

2. What about InfiniteList? There, you can't really write a toImpl function that isn't unsafe (since InfiniteListImpl isn't inhabited).

Sadly, the inductive-based implementation doesn't fit nicely into this approach. However, we can get (at least asymptotically) efficient InfiniteLists with a different implementation:

an attempt at `InfiniteList`

@[no_repr]
structure InfiniteList (α : Type u) where
  get : Nat -> α

-- state machine implementation of `InfiniteList`
structure InfiniteListImpl (α : Type u) : Type (u + 1) where
  State : Type u
  state : State
  next: State -> State \times α

-- We could make this noncomputable, it is only needed to construct an equivalence relation.
def InfiniteListImpl.toInfiniteList {α : Type u} (xs : InfiniteListImpl α) : InfiniteList α where
  get n :=
    let rec get' xs n := match n with
      | 0 => (xs.next xs.state).2
      | n + 1 => get' (InfiniteListImpl.mk xs.State (xs.next xs.state).1 xs.next) n
    get' xs n

/-- Two state machines are equivalent if they emit the same elements in order. -/
def InfiniteListImpl' (α : Type u) : Type (u + 1) := Quot (fun xs ys : InfiniteListImpl α => xs.toInfiniteList = ys.toInfiniteList)

/-- Derives a state machine from the kernel type `InfiniteList α`. -/
@[override_repr]
noncomputable def InfiniteList.toImpl {α : Type u} (xs : InfiniteList α) : InfiniteListImpl' α :=
  Quot.mk (InfiniteListImpl.mk (InfiniteList α) xs fun ys => (InfiniteList.mk fun n => ys.get (n + 1), ys.get 0))

-- info:
-- implToQuot  : {α : Type u} -> (xs : InfiniteListImpl' α) -> (∃ ys, ys.toImpl = xs) ->
--     Quot (fun xs ys : InfiniteList α => xs.toImpl = ys.toImpl
#check InfiniteList.implToQuot

-- Now, we can define and `csimp` all the functions we'd like to have on `InfiniteList`.

Given that override_repr works as proposed, no unsafeCast/implemented_by is necessary at all, so all the "unsafety" is encapsulated in the proposed language feature. I haven't tested whether this comes with a performance penalty, though.

3. What about writing @[override_repr] in a different module? Should this be prohibited? (probably)

Yes, I think I'd forbid that. Personally, I even find it questionable that implemented_by works beyond module boundaries because it makes it really hard to find the actual implementation of a type/def.

[Rob23oba]

Maybe to address 1 and 3 we can use a design similar to computed fields? The with clause currently only supports computed fields but what about:

structure InfiniteListImpl (α : Type u) : Type (u + 1) where
  State : Type u
  state : State
  next : State → State × α

def InfiniteListImpl.get (x : InfiniteListImpl α) : Nat → α :=
  go x.state
where
  go (s : x.State) : Nat → α
  | 0 => (x.next s).2
  | k + 1 => go (x.next s).1 k

structure InfiniteList (α : Type u) where
  get : Nat → α
with
  @[override_repr]
  toImpl : InfiniteList α → Quot (fun a b : InfiniteListImpl α => ∀ n, a.get n = b.get n)
  | ⟨get⟩ => Quot.mk _ (InfiniteListImpl.mk Nat 0 fun val => (val + 1, get val))

Computed fields need a rework anyways so why not combine it with a similar feature :-)
(computed fields + override_repr would obviously not be allowed since computed fields already assume something like an override_repr)

[nomeata]

(Small note for when this discussion eventually converges: we should probably look for a different name for the attribute that does not sounds like you are changing the Repr instance.)

[cppio]

I had an idea similar to WithRepr in https://leanprover.zulipchat.com/#narrow/channel/341532-lean4-dev/topic/Proposal.3A.20Customizable.20runtime.20representations/near/525950357 (I called it Encoded). As I mentioned there, you could use an opaque equivalence for unsafe/external representations:

unsafe structure InfListImpl (α : Type u) where
  hd : α
  tl : Thunk (InfListImpl α)

unsafe def InfListImpl.get (xs : InfListImpl α) : Nat → α
  | 0 => xs.hd
  | n + 1 => xs.tl.get.get n

unsafe def InfListImpl.iter (f : Nat → α) (n := 0) : InfListImpl α :=
  ⟨f n, iter f (n + 1)⟩

unsafe def InfListImpl.Repr (α : Type u) : (β : Type u) × ((Nat → α) ≃ β) := ⟨InfListImpl α, iter, get, lcProof, lcProof⟩

@[implemented_by InfListImpl.Repr]
opaque InfList.Repr (α : Type u) : (β : Type u) × ((Nat → α) ≃ β) := ⟨Nat → α, id, id, fun _ => rfl, fun _ => rfl⟩

Similarly, you could use the existing noncomputable equivalence Erased.equiv to implement the better Erased.

A downside with this approach is that it does not support the case where only one of the constructor and projection is computable, though I'm not sure of a situation where you would want that.

[Rob23oba]

Yeah, I believe something like this could be useful tool but shouldn't be "the main feature". In other words, you should be able to write this (mathlib should probably have this) and also use it to simplify the procedure for other types but other variants should also be allowed.