Pattern Matching on Types

Stream: new members

[Tomaz Gomes Mascarenhas]

Hi there! I am trying to implement a function that takes a type and returns a value of that type. Something like:

def f: (A : Type) → [Inhabited A] → A := λ A =>
  match A with
  | Nat  => 42
  | _    => default

but this doesn't work, Lean thinks that "Nat" is a new name that I introduced... I also tried:

def coe' : (A = B) → A → B
| rfl, a => a

def f: (A : Type) → [Decidable (Nat = A)] → [Inhabited A] → A := λ A =>
  if r: Nat = A then coe' r 42 else default

which does work, but is annoying to have to pass an instance of decidable equality for each type that I'm gonna use... also, I can use the function instantiating A to some type, even if I instantiate the decidable equality using "sorry", like this:

instance: Decidable (Nat = Bool) := isFalse sorry
#eval f Bool  -- false

it seems to me that there must be a better way to pattern match on types... does anyone know?

[Kevin Buzzard]

Type equality is poorly behaved in Lean and you can't pattern match on Type because Type is not an inductive type. You can use if then else to do what you want to do, I guess. (oh -- as you already know)

[Kevin Buzzard]

One issue is that it is not at all decidable if a given type is equal to Nat, for example Int = Nat is neither provable nor disprovable in Lean, and the default Int is not 42, so what is your function supposed to return then?

[Chris B]

Tomaz Gomes Mascarenhas said:

it seems to me that there must be a better way to pattern match on types... does anyone know?

Pattern matching uses a type's recursor, so you can't really match on types in the general way your first example tries to. The if then else example works because you're using the Decidable instance. I think what you would to do get something like the first (nonworking) example is write a new instance of Inhabited Nat. If there's something specific you're trying to do, the details might help.

[Tomaz Gomes Mascarenhas]

Kevin Buzzard said:

One issue is that it is not at all decidable if a given type is equal to Nat, for example Int = Nat is neither provable nor disprovable in Lean, and the default Int is not 42, so what is your function supposed to return then?

mm, so it is impossible to decide whether any pair of types are equal? can you think of any problems that I could get if I leave that sorry in the instance of Decidable (Nat = Bool)? Like if I try to evaluatef in some context...

[Kevin Buzzard]

I'm not an expert in this sort of nonsense but my understanding is that the only time you can prove that types are not equal in lean is if they have different cardinalities (ie there is no bijection between them). Note that this would apply in the Nat and Bool case

[Chris B]

Leaving the sorry in is just a more convoluted way of using typeclasses to solve this.

class Inhabited' (A : Type) where
  default' : A

instance {A : Type} [Inhabited A] : Inhabited' A where
  default' := Inhabited.default

instance : Inhabited' Nat where
  default' := 42

def f (A : Type) [Inhabited' A] : A := Inhabited'.default'

example : f Nat = 42 := rfl
example : f String = "" := rfl
example : f (List Char) = [] := rfl

[Chris B]

Since you're still relying on typeclasses to bootleg instances of DecidableEq in the sorry example.

[Tomaz Gomes Mascarenhas]

Chris B said:

Since you're still relying on typeclasses to bootleg instances of DecidableEq in the sorry example.

ahh, I see, yeah, I think this could work for what I'm trying to do. Thanks!

[Kevin Buzzard]

This creates a diamond with two instances of Inhabited' Nat I guess. In Lean 4 is there a way of changing priorities so that Lean will find the instance you want for Nat rather than the generic one? In Lean 3 I would not like to guess whether f Nat = 42 or not; type class inference is not designed with this situation in mind. It might even depend on which order you define the two instances.

[Chris B]

The typeclass section of TPIL 4 has some information about typeclass priorities in lean 4, I haven't done much experimentation but the example works. There's probably a more principled solution for whatever the particular use case is. I agree that you probably shouldn't rely on overlapping instance unless getting the wrong one will cause an obvious hard error.