Typeclass combinators Option, And, Or

Stream: lean4

[Tomas Skrivan]

Is is possible to somehow implement Option, Or, And for typeclasses?

For example, Option typeclass would be

class OptionTC (Class : Sort _) where
  inst : Option Class

instance (priority:=low) : OptionTC Class where
  inst := .none

instance {Class} [c : Class] : OptionTC Class where
  inst := .some c

The issue is that you can't write [c : Class] as Class is not a concrete typeclass.

My application would be to write an array that stores elements in byte array if possible or use normal array if not.

-- type that has fixed byte size
class ByteStorable (α : Type _) where
  size : Nat
  toBytes : α → (a : ByteArray) → (i : Fin (a.size - size)) → ByteArray
  fromBytes : (a : ByteArray) → (i : Fin (a.size - size)) → α

structure DataArray (α : Type _) [ByteStorable α] : Type where
  data : ByteArray
  -- ...

def MyArray (α : Type _) [b : OptionTC (ByteStorable α)] : Type :=
  match b.inst with
  | .some _ => DataArray α
  | .none => Array α

For OptionTC I can imagine generating specialized instance for every concrete class Class but this would not be possible for AddTC or OrTC as it would require an instance for every pair of classes.

[Mario Carneiro]

Yes, there is a TCOr in iris-lean and it works exactly as you would expect

[Tomas Skrivan]

Ahh a magical set_option checkBinderAnnotations false and it works as expected :)

[Mario Carneiro]

hm, maybe the error message should suggest that...