Renaming existing fields in structure?

Stream: metaprogramming / tactics

[Quang Dao]

@Devon Tuma and I are building VCVio, which defines an oracle computation framework that is equal to taking the free monad over a polynomial functor (seen as a (dependent) oracle). Specifically, our stack is:

import Mathlib.Data.PFunctor.Univariate.Basic

universe uA uB u v

/-- Alias the base functor. -/
abbrev OracleSpec := PFunctor.{uA,uB}

namespace OracleSpec
/-- Pretty names for `PFunctor.A`/`PFunctor.B`. -/
abbrev Domain (spec : OracleSpec) : Type uA := spec.A
abbrev Range (spec : OracleSpec) (t : spec.Domain) : Type uB := spec.B t
end OracleSpec

inductive FreeM (P : PFunctor.{uA,uB}) : Type u → Type (max uA uB u)
  | pure {α : Type u} (x : α) : FreeM P α
  | roll {α : Type u} (a : P.A) (k : P.B a → FreeM P α) : FreeM P α

/-- Query object is the polynomial functor object. -/
abbrev OracleQuery (spec : OracleSpec.{uA,uB}) : Type u → Type (max uA uB u) :=
  PFunctor.Obj spec

/-- Syntactic query (same as `⟨t, id⟩`). -/
def query {spec : OracleSpec} (t : spec.Domain) : OracleQuery spec (spec.Range t) :=
  ⟨t, id⟩

/-- Computations are the free monad over the spec. -/
abbrev OracleComp (spec : OracleSpec.{uA,uB}) : Type u → Type (max uA uB u) :=
  FreeM spec

My question is: is it possible to show .Domain and .Range in the infoview instead of the default names .A and .B in PFunctor? Similarly, print out PFunctor.Obj as OracleQuery and PFunctor.FreeM as OracleComp?

[Matej Penciak]

I'm not sure this is the most principled way of doing it, but this works:

import Lean

structure Foo where
  a : Type
  b : a

open Lean Meta PrettyPrinter Delaborator SubExpr

@[app_delab Foo.a]
def delabFooA : Delab := do
  let expr ← getExpr
  let_expr Foo.a body := expr | throwError ":("
  return ← `($(←delab body).$(mkIdent `newName))

@[app_delab Foo.b]
def delabFooB : Delab := do
  let expr ← getExpr
  let_expr Foo.b body := expr | throwError ":("
  return ← `($(←delab body).$(mkIdent `otherNewName))

example (x y : Foo) (h : x.a = y.a) : x.b = h ▸ y.b := by
  -- x y : Foo
  -- h : x.newName = y.newName
  -- ⊢ x.otherNewName = ⋯ ▸ y.otherNewName
  sorry

It feels a bit like a hack though, and there are a bunch of edge cases you'd need to deal with in the delaborator to get the behavior everywhere

[Eric Wieser]

What advantage does PFunctor provide here vs directly passing around the index types {ι : Type*} {ω : ι → Type*}?

[Eric Wieser]

(for instance, docs#Std.DHashMap and docs#DFinsupp could take a PFunctor as input, but they do not)

[Eric Wieser]

Putting types into structures is generally a way to end up in a fight with Lean's typeclass resolution

[Devon Tuma]

I guess the current reason would be that the dependent omega type can get complicated quite quickly, even just adding a few PFunctor together gives multiple eliminator calls in it. This seemed to get fairly messy in my experience, especially in reductions where you modify the oracle spec multiple times.

We did at one time have both an indexing type being passed around and also a domain type in the struct, but combined the indexing into the domain in the struct (giving essentiallyPFunctor). Maybe it would be better to instead move the domain out of the struct into the indexing being passed around.

Type class resolution errors have come up but they generally seem to have been handled by marking structs as reducible, at least for now

[Eric Wieser]

I guess once you get to eliminator calls you run into trouble with typeclass inference anyway