typeclass as type variable

Stream: general

[Matthew Pocock]

Is it possible within lean, without metaprogramming, to have a variable that refers to an unspecified typeclass?

def weird_function (tc: ???) ...

#check weird_function (LT)
#check weird_function(GT)

So where tc would be filled in later with a typeclass (not an instance of a typeclass). I have tried a few things, but so far not stumbled over syntax that works.

[Kevin Buzzard]

Just check the type of LT and that should be what ??? is

[Alex J. Best]

Can you be more specific about what you want to do with this? A typeclass is "just" a (dependent type) so it itself has a type. I don't know any way to specify within the logic of lean that something is a class, but if you have something like

def a {m : Type -> Type} {alpha : Type} [m alpha] : sorry := sorry

then it will only ever be instantiated by the TC mechanism when m is a class

[Matthew Pocock]

Alex J. Best said:

Can you be more specific about what you want to do with this? A typeclass is "just" a (dependent type) so it itself has a type. I don't know any way to specify within the logic of lean that something is a class, but if you have something like

def a {m : Type -> Type} {alpha : Type} [m alpha] : sorry := sorry

then it will only ever be instantiated by the TC mechanism when m is a class

Thanks. I think this answers my question. I think I was fat-fingering how I was writing Type -> Type.

Cheers :D

[Alex J. Best]

Apparently lean complains about such a def by default but you can turn that off as the error message states. I'm still curious what you hope to with this though, you can't really do much without more information about the m in question

[Matthew Pocock]

I'm still interested in a systematic way to describe one type being embedded into another, and asserting that various type classes "work" consistently across the embedding.

[Eric Wieser]

I think the two approaches here are:

• Just write out the statements manually for each typeclass
• Use the category theory library which bundles {alpha : Type} [m alpha] as MCat

[Matthew Pocock]

Eric Wieser said:

• Just write out the statements manually for each typeclass

This is what I'm doing while sketching. Trivial but tedious. Probably time for me to read the metaprogramming book.

class NaturalEmbedding (α β : Type*) where
    embed : α → β
    embedded : β -> Prop

class NE_LT (α β : Type*) [ne : NaturalEmbedding α β] [ltα : LT α] [ltβ : LT β] where
    embeds_lt(a1 a2: α) : ltα.lt a1 a2 = ltβ.lt (ne.embed a1) (ne.embed a2)

class NE_Zero (α β : Type*) [ne : NaturalEmbedding α β] [zα : Zero α] [zβ : Zero β] where
    embeds_zero : ne.embed zα.zero = zβ.zero

class NE_Add (α β : Type*) [ne : NaturalEmbedding α β] [addα : Add α] [addβ : Add β] where
    embeds_add(a1 a2: α) : ne.embed (addα.add a1 a2) = addβ.add (ne.embed a1) (ne.embed a2)


instance : NaturalEmbedding ℕ ℤ where
    embed := Int.ofNat
    embedded := (. ≥ 0)

instance : NE_LT ℕ ℤ where
    embeds_lt(a1 a2: ℕ) := by simp [embed]

instance : NE_Zero ℕ ℤ where
    embeds_zero := by simp [embed]

instance : NE_Add ℕ ℤ where
  embeds_add := by
    intros a1 a2
    simp [embed]
    rfl