What effect does "instance" have in this example?

Stream: new members

[Kevin Cheung]

I was just trying things and was surprised that the following compiled without warnings or errors:

import Mathlib.Data.Nat.Defs

instance bar : (n : ℕ) → Decidable (n = 1) := fun n => n.decEq 1

I am quite confused as to what instance could possibly mean here. In particular, what is bar an instance of?

[Tom]

My understanding is that an "instance" is a specific instantiation (value) of a type (class). These get registered with the elaborator and can be automatically found later during type class synthesis and as such, typically don't need a name, e.g.

instance : Add MyType where

is effectively converted to something like

def <elaboratorGeneratedName> : Add MyType := { ...fields... }

elaborator_magic.register_instance <elaboratorGeneratedName>

E.g.

instance myTypeAdd : Add MyType where
  add x y := sorry

#reduce myTypeAdd

is { add := fun x y => sorryAx ?m.233 }

I think in this instance (ha!), it looks like your type is a function, so the instance is a value of a function type:

instance bar: (n : Nat) → Decidable (n = 1) := fun n => n.decEq 1

#reduce bar

is fun n => <snip>

You can try this by e.g. by

instance foo : Nat -> Nat := fun x => x + 1

#reduce foo

produces fun x => x.succ

So it seems instance is just a "surface level"/Elaborator syntax for the above.

Unfortunately, I'm just a noob so don't know if

1) This/using functions has any implications on instance synthesis/registration (or whatever that may mean in this case)
2) I don't know whether the explicit name for the instance is useful beyond giving a name which is more "readable" to you

[Tom]

FWIW, I think the "registration magic" looks like this

attribute [instance] ...

[Kyle Miller]

(Terminology: "elaborator" instead of "compiler". There's a compiler too, but it's for turning elaborated declarations into executable code.)

[Kevin Cheung]

I am still trying to make sense of this. So instance is basically attribute [instance] before a def? Does that mean that it can never fail?

[Kyle Miller]

Yes, instance foo ... is pretty much @[instance] def foo .... If foo isn't provided, it generates a name for you.

Could you say a bit more what you're confused about? Why did you expect it to fail?

[Kevin Cheung]

I thought an instance has to be associated with a class definition.

[Kevin Cheung]

In my example, no class was defined. So I wasn't sure what class the definition was an instance of.

[Kyle Miller]

docs#Decidable is a class, does that help?

[Kevin Cheung]

I can understand that if the part (n : Nat) wasn't there.

[Kevin Cheung]

Something like instance : Decidable (1 = 1) makes sense to me.

[Kyle Miller]

(Edit: This isn't quite right.) It turns out that (n : ℕ) → Decidable (n = 1) is a class too. So long as the resulting value for a function type is a class, then it's a class. This class is parameterized by the variable n. It applies to Decidable (0 = 1), Decidable (1 = 1), Decidable (2 = 1), etc.

[Kyle Miller]

Also, just like for normal definitions, both of these are equivalent:

instance bar (n : ℕ) : Decidable (n = 1) := n.decEq 1

instance bar : (n : ℕ) → Decidable (n = 1) := fun n => n.decEq 1

[Kevin Cheung]

So, it is a class that takes a parameter?

[Kyle Miller]

Yes. Many (most?) instances take parameters.

[Kyle Miller]

At least internally, (n : ℕ) → Decidable (n = 1) is a class, but the class "is" Decidable. Not sure if this phrasing helps at all.

[Kevin Cheung]

I guess I was confused by that Decidable takes a Prop and didn't know that Prop can be parametrized.

[Kyle Miller]

Sorry, I'm really messing this up.

[Kyle Miller]

I'm meaning to say that the class is Decidable, but (n : ℕ) → Decidable (n = 1) is a valid type for an instance.

[Kyle Miller]

It's a parameterized instance.

[Kevin Cheung]

Interesting.

[Kyle Miller]

During instance synthesis, this corresponds to the rule that Decidable (_ = 1) can always be satisfied, with any Nat in place of _

[Tom]

Kyle Miller said:

(Terminology: "elaborator" instead of "compiler". There's a compiler too, but it's for turning elaborated declarations into executable code.)

Thanks, fixed. I promised I'll start getting this right. :laughing:

[Kevin Cheung]

Thanks for the explanation. Very helpful.