Is it possible to make this typeclass parameter implicit ?

Stream: lean4

[Frederic Peschanski]

I am working on a Lean4 development involving a typeclass that looks like this:

class Model (CTX) (M) where
  ctx : CTX
  prop : M → Prop

A Model is some type M depending on a context.
Here is an example of a context :

structure ExCtx where
  param : Nat
  param_Ax : param > 0

A typical "Model" is dependent on a context,
such as the following one :

structure ExModel (ctx : ExCtx) where
  value : Nat

Now I can instantiate the typeclass :

instance: Model ExCtx (ExModel ctx) where
  ctx := ctx
  prop m := m.value < ctx.param

Since ctx is of type ExCtx I tried to make the typeclass parameter CTX
implicit, e.g. doing :

class Model {CTX} (M) where
  ...

But this doesn't work, is is always necessary to explicit the CTX paramer, e.g.
this does not work :

instance: Model (ExModel ctx) where
  ctx := ctx
  prop m := m.value < ctx.param

I tried several things like relying on typeclass resolution (introducing a HasContext class), tyring to exploit an outParam ... but failed to find a simple solution.

[r.z. Almi.]

Frederic Peschanski said:

structure ExCtx where
  param : Nat

why Nat ?

[Eric Wieser]

Frederic Peschanski said:

A typical "Model" is dependent on a context,

Are you willing to strengthen this to "every model must be a function from the context"?

[Frederic Peschanski]

Eric Wieser said:

Are you willing to strengthen this to "every model must be a function from the context"?

Yes, the context could by an empty struct anyways ...

[Frederic Peschanski]

r. Almi. said:

why Nat ?

It's just an example, the context can be an arbitrary structure (and so is a model, except that it depends on a context)

[Tomas Skrivan]

Why using outParam does not work for you? I would just mark CTX with it. Using outParam make CTX implicit argument in functions Model.ctx and Model.param.

class Model (CTX : outParam (Type _)) (M : Type _) where
  ctx : CTX
  prop : M → Prop

class Model' (CTX : Type _) (M : Type _) where
  ctx : CTX
  prop : M → Prop

#check Model.ctx -- `CTX` is implicit argument
#check Model'.ctx -- `CTX` is NOT implicit argument



structure ExCtx where
  param : Nat
  param_Ax : param > 0

structure ExModel (ctx : ExCtx) where
  value : Nat

instance (ctx : ExCtx) : Model ExCtx (ExModel ctx) where
  ctx := ctx
  prop m := m.value < ctx.param

def exModelCtx (ctx : ExCtx) := Model.ctx (ExModel ctx)
def exModelProp {ctx : ExCtx} (m : ExModel ctx) := Model.prop m

[Frederic Peschanski]

Tomas Skrivan said:

instance (ctx : ExCtx) : Model ExCtx (ExModel ctx) where
  ctx := ctx
  prop m := m.value < ctx.param

What I would like to avoid is the repeatition of ExCtx in such a class instantiation,
i.e. writing the following instead :

instance (ctx : ExCtx) : Model (ExModel ctx) where
  ctx := ctx
  prop m := m.value < ctx.param

I can manage this with some metaprogramming but I wanted to know if there was
something possible at the typeclass level

[Tomas Skrivan]

Then maybe something like this?

class Model {CTX : Type _} (M : CTX → Type _) where
  prop : (ctx : CTX) → M ctx → Prop

structure ExCtx where
  param : Nat
  param_Ax : param > 0

structure ExModel (ctx : ExCtx) where
  value : Nat

instance : Model ExModel where
  prop ctx m := m.value < ctx.param

def exModelProp {ctx : ExCtx} (m : ExModel ctx) := Model.prop ctx m

[Tomas Skrivan]

This feels wrong as this requires to show that any context ctx and any model m satisfied the condition Model.prop ctx m but I do not understand your application so it might be ok.