Telescopically parameterised blocks

Stream: new members

[ziman]

Hi, I'm trying to formalise a theory where you pick a number n, which stands for the number of agents in the model, as well as equally numerous items in the model, and then you make further definitions that depend on all of these. In Agda, I'd do something like the following:

module Module (n : N) where
  Agent : Set
  Agent = Fin n

  Item : Set
  Item = Fin n

  module TheoryAboutUtilities (utility : Agent -> Item -> Nat) where
    {- here I can use `n`, `Agent`, `utility`, etc. -}
    record Constant where
      field
        const : Nat
        .pf : forall (a : Agent) (i : Item) -> utility a i ≡ const

Notice that in utility, as well as .pf, I could just refer to the type of agents as Agent, and the system understands that it's the type of agents in the context of the broader scope that contains n. (BTW, normally I'd newtype the definition of Agent but let's keep it simple here.)

However, in Lean, I have not been able to find an equivalent construction. The closest I could find is variable but that does not abstract away all the dependent context, and I have to write the following

variable (n : Nat)
def Agent (n : Nat) : Type := Fin n
def Item (n : Nat) : Type := Fin n
variable (utility : Agent n -> Item n -> Nat)

Here's the first difference: I can't just refer to the types of agents and items, I have to explicitly repeat the parameter n and have to be constantly aware of the entire context of their definition at all usage sites. It gets worse, though:

structure Constant where
  const : Nat
  pf : (a : Agent n) -> (i : Item n) -> utility a i = const

This definition is buggy because I forgot to add (n : Nat) to Constant, which means that the n will be universally quantified at pf instead, which is not what I wanted to express.

So for me it's a question of convenience (having to write all these parameters), abstraction (why should I care how Agent is defined, I just want the type and build further abstractions on top of it), and correctness (easy to make a mistake that's well-typed but means something else). I suppose this might also have consequences for universe levels (parameters vs. indices), too?

Can I avoid all this and get Agda-style parameters for entire blocks/sections in Lean?

[Kyle Miller]

This feature used to exist in Lean 3, but in Lean 4 it was decided to be too complex, and many use cases can be expressed better using typeclasses.

You mention "why should I care how Agent is defined?" Maybe that suggests that Agent can be an abstract type to begin with? You could add [Fintype Agent] or [Finite Agent] if you want to add the assumption the type is finite, the choice depending on how much computation you might want to do.

[Kyle Miller]

You could express that they have the same cardinality using docs#Equiv, and then the Constant structure wouldn't be peering through the abstraction boundary.

[ziman]

I'll experiment with that, thank you!