Typeclass resolution with type functions

Stream: lean4

[Juan Pablo Romero]

I have a function that removes a trailing Unit on tuples:

class Simplify (A : Type) where
  apply: Type

instance : Simplify (A × B × Unit) := ⟨A × B⟩
instance : Simplify (A × Unit) := ⟨A⟩
instance : Simplify Unit := ⟨Unit⟩

example : Simplify.apply Unit = Unit := rfl
example : Simplify.apply (Int × Unit) = Int := rfl
example : Simplify.apply (String × Int × Unit) = (String × Int) := rfl

But I'm having problems using it when the given type is calculated by another function:

def ArgTypes (s : String) : Type := toType s.toList
  where
    toType : List Char -> Type
      | [] => Unit
      | '%' :: 'd' :: rest => Int × toType rest
      | '%' :: 's' :: rest => String × toType rest
      | _ :: rest => toType rest

example : ArgTypes "abc" = Unit := rfl
example : ArgTypes "%s is %d" = (String × Int × Unit) := rfl
example : ArgTypes "%s is %d - %d" = (String × Int × Int × Unit) := rfl

#check Simplify.apply (ArgTypes "abc")

-- failed to synthesize instance
--  Simplify (ArgTypes "abc")

Looks like the resolution mechanism does not evaluate the argument?

[Marcus Rossel]

(deleted)

[Floris van Doorn]

Correct, type classes don't unfold (non-reducible) definitions.
This is something that is probably better to do with metaprogramming.
What is your use case?

[Tomas Skrivan]

The typeclass inference does not see through function marked with def, they need to be transparent i.e. marked with abbrev or with @[reducible].

Here is a simple example for creating nth power of a type TypePower α n = α × ... × α

abbrev TypePower (α : Type) : Nat → Type
  | 0 => Unit
  | 1 => α
  | n+2 => α × TypePower α (n+1)

def TypePower' (α : Type) : Nat → Type
  | 0 => Unit
  | 1 => α
  | n+2 => α × TypePower' α (n+1)

example : ToString (TypePower Nat 2) := by infer_instance  -- succeeds
example : ToString (TypePower' Nat 2) := by infer_instance -- fails

[Tomas Skrivan]

Here is a modification of your example that works:

class Simplify (A : Type) where
  apply: Type

instance : Simplify (A × B × Unit) := ⟨A × B⟩
instance : Simplify (A × Unit) := ⟨A⟩
instance : Simplify Unit := ⟨Unit⟩

example : Simplify.apply Unit = Unit := rfl
example : Simplify.apply (Int × Unit) = Int := rfl
example : Simplify.apply (String × Int × Unit) = (String × Int) := rfl

def ArgTypes (s : String) : Type := toType s.toList
  where
    toType : List Char -> Type
      | [] => Unit
      | '%' :: 'd' :: rest => Int × toType rest
      | '%' :: 's' :: rest => String × toType rest
      | _ :: rest => toType rest


@[reducible] -- `abbrev` is just a shorthand for `reducible` attribute
def ArgTypes' : List Char → Type
  | [] => Unit
  | '%' :: 'd' :: rest => Int × ArgTypes' rest
  | '%' :: 's' :: rest => String × ArgTypes' rest
  | _ :: rest => ArgTypes' rest

abbrev ArgTypes'' (s : String) : Type := ArgTypes' s.data


example : ArgTypes "abc" = Unit := rfl
example : ArgTypes "%s is %d" = (String × Int × Unit) := rfl
example : ArgTypes "%s is %d - %d" = (String × Int × Int × Unit) := rfl

#check Simplify.apply (ArgTypes "abc") -- fails because ArgTypes and String.toList are not `abbrev`
#check Simplify.apply (ArgTypes' ['a', 'b', 'c'])
#check Simplify.apply (ArgTypes' "abc".toList) -- fails because String.toList is not `abbrev`
#check Simplify.apply (ArgTypes' "abc".data)
#check Simplify.apply (ArgTypes'' "abc")

[Tomas Skrivan]

I didn't study your example properly but it looks like that your Simplify class is dealing exactly with the problem that naive implementation of TypePower produces α × ... × α × Unit

abbrev TypePowerNaive (α : Type) : Nat → Type
  | 0 => Unit
  | n+1 => α × TypePowerNaive α n

abbrev TypePowerCorrect (α : Type) : Nat → Type
  | 0 => Unit
  | 1 => α
  | n+2 => α × TypePowerCorrect α (n+1)

example : TypePowerNaive Nat 2 = (Nat × Nat × Unit) := by rfl
example : TypePowerCorrect Nat 2 = (Nat × Nat) := by rfl

[Juan Pablo Romero]

@Tomas Skrivan Ahh, I see. the inner function toType needed to be marked as reducible as well. Nice.