joining typeclasses

Stream: new members

[ooovi]

Hello!

I'm in a situation where I'm making a lot of arguments about types that are members of a number of typeclasses and have some other common properties. Currently, I spell all of them out in all my type signatures. I was thinking to make a type class that contains all the properties I need, but I fail to make instance inference work. Am I walking in the wrong direction?

Here's what I tried. So I make a typeclass for my (exemplary) properties:

class MeFinClass (type : Type*) (N : Nat) where
  fin : Fintype type
  card : Fintype.card type = N

Next, I want inference of the Fintype instance for type:

instance hm [t : MeFinClass α N] : Fintype α where
  elems := t.fin.elems
  complete := t.fin.complete

but I get in trouble:

cannot find synthesization order for instance @hm with type
  {α : Type u_1} → {N : ℕ} → [t : MeFinClass α N] → Fintype α
all remaining arguments have metavariables:
  MeFinClass α ?N

I don't understand what that means, and maybe I should do a different thing alltogether?

[Matt Diamond]

I suspect this is a case where you need to mark N as an outParam or a semiOutParam, but I'm not sure which (see docs#outParam and docs#semiOutParam)

the idea is that it lets you tell Lean the order in which typeclass params should be resolved... so in this case we're telling Lean "don't worry about N until you figure out what α is, and then just use whatever N you find first"

[Matt Diamond]

it looks like either of them work here, but I don't know enough to tell you which is the "correct" one

[Matt Diamond]

btw when I say mark it as an outParam I mean something like this:

import Mathlib

class MeFinClass (type : Type*) (N : outParam Nat) where
  fin : Fintype type
  card : Fintype.card type = N

instance hm [t : MeFinClass α n] : Fintype α where
  elems := t.fin.elems
  complete := t.fin.complete

[Eric Wieser]

Or the shorter

class MeFinClass (type : Type*) (N : outParam Nat) extends Fintype type where
  card : Fintype.card type = N

which avoids needing to write the instance manually

[Matt Diamond]

ah, there's always a better solution :)

[ooovi]

Sweet, thank you both! Quick follow-up, I read somewhere that multiple inheritance is also possible for typeclasses using the same syntax as for structures, but the following won't work:

class MeeFinClass (type : Type*) (N : outParam Nat) extends (Fintype type), (DecidableEq type) where
  card : Fintype.card type = N

gives complaints about the second extended class:

expected structure

[Ruben Van de Velde]

Try without the parentheses

[Eric Wieser]

DecidableEq is not a structure

[Eric Wieser]

This works:

import Mathlib

class MeeFinClass (type : Type*) (N : outParam Nat) extends Fintype type where
  [toDecidableEq : DecidableEq type]
  card : Fintype.card type = N

attribute [instance] MeeFinClass.toDecidableEq