Dot notation for structs with an explicit instance argument

Stream: new members

[pandaman]

Is it possible to make the following dot notation work? Adding type class argument to all field access clutters the code. Thanks!

class C where
  α : Type

structure S [C] where
  val : C.α

def inst1 : C where
  α := Int

def ok (s1 : @S inst1) := @S.val inst1 s1
/-
failed to synthesize
  C
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
-- def bad (s1 : @S inst1) := s1.val

[Aaron Liu]

What is the context you need this in?

[pandaman]

I have an algorithm and data structures abstracted with a type class and want to prove relationship between two particular instances applied to the algorithm.

[Aaron Liu]

Do the two instances have the same type?

[Kyle Miller]

Usually you'd make def inst1 into an instance.

Is there anything about C that can distinguish between the different instances that you want? Using typeclasses that have multiple conflicting instances can cause confusing behavior.

[pandaman]

I'd like to do something like this. There will be two (or more) instances. I'd like to build my theory using a richer instance (i.e., HistoryStrategy below) and transport the results to the "real" instance (i.e., SumStrategy below) using some correspondence lemmas.

class Strategy where
  α : Type
  empty : α
  push : α → Nat → α

structure Accum [σ : Strategy] where
  val : σ.α
  count : Nat

-- I'd like to use an instance here so `[@specialize]` works
@[specialize]
def alg [σ : Strategy] (accum : Accum) : List Nat → Accum
  | [] => accum
  | x :: xs => alg (⟨σ.push accum.val x, accum.count + 1⟩) xs

def HistoryStrategy : Strategy where
  α := Array Nat
  empty := #[]
  push a n := a.push n

def SumStrategy : Strategy where
  α := Nat
  empty := 0
  push n m := n + m

def Correspondence (a₁ : @Accum HistoryStorategy) (a₂ : @Accum SumStrategy) : Prop :=
  a₁.val.sum = a₂.val ∧ a₁.count = a₂.count -- error here

example {a₁ : @Accum HistoryStrategy} {a₂ : @Accum SumStrategy} (h : Correspondence a₁ a₂) : Correspondence (@alg HistoryStrategy a₁ xs) (@alg SumStrategy a₂ xs) := sorry

[pandaman]

The errors are not exactly the same I encountered in this example, but I think the cause is the same (multiple instances). It looks like not using instance parameter in Accum (like Accum (σ : Strategy)) fixes some issues, so I'll try it.

[Aaron Liu]

Are you sure you want Strategy to be a typeclass? If so, you can write notation with
notation (name := alg_of) "alg[" s "]" => @alg s

PS. You can specialize a parameter that is not an instance with @[specialize σ]. See docs#Lean.Compiler.LCNF.SpecParamInfo.

[Robin Arnez]

A good heuristic for when something should or shouldn't be a class is whether you usually want at most one instance or not. As an example, Add is a class because there is usually one particular interpretation of addition for a type. In your case, you have at least two Strategys, so you probably don't want a class or you're going to run into a lot of weird instance problems.

[pandaman]

I see this comment in specialize.cpp. Is specialization for non-class and non-function arguments supported in the old compiler?

/* IMPORTANT: We currently do NOT specialize Fixed arguments.
   Only FixedNeutral, FixedHO and FixedInst.
   We do not have good heuristics to decide when it is a good idea to do it.
   TODO(Leo): allow users to specify that they want to consider some Fixed arguments
   for specialization.
*/

[pandaman]

My end goal is to have my algorithm run fast (for one particular Strategy that will be used in the hot loop). At the moment, I specialize them by hand (1, 2). If the old compiler doesn't support specializing Strategy and specialization is needed for perf, I'll probably just keep the two definitions (it's more maintenance, though)...

[Aaron Liu]

Did you try @[specialize argName]?

[Aaron Liu]

(I have no idea if this works or not)

[pandaman]

(I have no idea if this works or not)

I don't see no alg generated at algHistory, so no.

class Strategy where
  α : Type
  empty : α
  push : α → Nat → α

structure Accum (σ : Strategy) where
  val : σ.α
  count : Nat

@[specialize σ]
def alg (σ : Strategy) (accum : Accum σ) : List Nat → Accum σ
  | [] => accum
  | x :: xs => alg σ (⟨σ.push accum.val x, accum.count + 1⟩) xs

def HistoryStrategy : Strategy where
  α := Array Nat
  empty := #[]
  push a n := a.push n

def SumStrategy : Strategy where
  α := Nat
  empty := 0
  push n m := n + m

set_option trace.compiler.ir.result true in
def algHistory accum xs := alg HistoryStrategy accum xs

[pandaman]

Fortunately, I just took a benchmark and the algorithm without specialization runs as fast as that with specilization, so I can just ignore them here:stuck_out_tongue_wink: Thank you for the suggestions anyway!

[Aaron Liu]

I figured out a hack

class Strategy where
  α : Type
  empty : α
  push : α → Nat → α

structure Accum (σ : Strategy) where
  val : σ.α
  count : Nat

@[specialize σ]
def alg (σ : Unit → Strategy) (accum : Accum (σ ())) : List Nat → Accum (σ ())
  | [] => accum
  | x :: xs => alg σ (⟨(σ ()).push accum.val x, accum.count + 1⟩) xs

def HistoryStrategy : Strategy where
  α := Array Nat
  empty := #[]
  push a n := a.push n

def SumStrategy : Strategy where
  α := Nat
  empty := 0
  push n m := n + m

set_option trace.compiler.ir.result true in
def algHistory accum xs := alg (fun _ ↦ HistoryStrategy) accum xs