default typeclass instances?

Stream: new members

[Kris Brown]

I'd like to define some functions which can take in any type but have some default behavior if an unexpected type is given. E.g.:

def is_int_or_nat: Π{α:Type}, α → bool
| ℤ _ := tt
| ℕ _ := tt
| _ _ := ff

This doesn't work , but is something similar possible? Typeclasses seem appropriate for this ad-hoc polymorphism, but I don't know how to define a "everything else" typeclass, something like below.

class Z_or_N_typeclass (α : Type*) :=
 (is_Z_or_N : bool := ff) -- possibly a solution involves having a default value?

instance Z_is : Z_or_N_typeclass ℤ :=
 Z_or_N_typeclass.mk tt

instance N_is : Z_or_N_typeclass ℕ :=
 Z_or_N_typeclass.mk tt

--instance everything_else : Z_or_N_typeclass (Type*) :=
-- Z_or_N_typeclass.mk ff

def test: Π{α: Type} [Z_or_N_typeclass α], α → bool
 | _ Z_or_N_fun _ := Z_or_N_fun.is_Z_or_N

[Kevin Buzzard]

I suspect this is #xy. Note that nat = int is undecidable in Lean. Your definitions don't work because the equation compiler is expecting an inductive type and universes aren't inductive types

[Kenny Lau]

@Kevin Buzzard this feels like those linear algebra assumptions "assume K is R or C"

[Mario Carneiro]

Something like your second example works more or less as is

class Z_or_N_typeclass (α : Type*) := (is_Z_or_N : bool)
open Z_or_N_typeclass (is_Z_or_N)

instance Z_is : Z_or_N_typeclass ℤ := ⟨tt⟩
instance N_is : Z_or_N_typeclass ℕ := ⟨tt⟩
@[priority 0] instance everything_else {α} : Z_or_N_typeclass α := ⟨ff⟩

#eval is_Z_or_N nat -- tt
#eval is_Z_or_N int -- tt
#eval is_Z_or_N unit -- ff

[Mario Carneiro]

This doesn't go against Kevin's observation because the actual data is in the instance; you can still get is_Z_or_N nat to return false

#eval @is_Z_or_N nat everything_else -- ff

[Mario Carneiro]

You can even associate the typeclass with a correctness proof so that you can do things like Kenny's R or C example

class Z_or_N_typeclass (α : Type*) :=
(is_Z_or_N : bool)
(valid : is_Z_or_N → α = ℤ ∨ α = ℕ)
open Z_or_N_typeclass (is_Z_or_N)

instance Z_is : Z_or_N_typeclass ℤ := ⟨tt, λ _, or.inl rfl⟩
instance N_is : Z_or_N_typeclass ℕ := ⟨tt, λ _, or.inr rfl⟩
@[priority 0] instance everything_else {α} : Z_or_N_typeclass α := ⟨ff, λ h, bool.no_confusion h⟩

[Johan Commelin]

On the other hand, I hope you will never have to prove that a certain type is not equal to nat or int...

[Mario Carneiro]

that valid field can't be a biconditional because as I showed you can use the everything_else instance with nat and int as well

[Kevin Buzzard]

I'm guessing we can't prove mynat = nat either

[Kris Brown]

Kevin was originally right that this is probably XY - I was just having difficulties doing things the moral way. I don't understand why my eval function below is wrong:

class has_relop (α : Type) :=
 (evl : relOP → α → α → bool)

class has_binop (α : Type) :=
 (evl : binOP → α → α → α)

def eval : Π{α:Type} [has_relop α] [has_binop α], Exp α → Env → α
 | _ _ _ (Exp.const x) _ := x
 | _ _ _ (Exp.binop o x y) e := has_binop.evl o (eval x e) (eval y e)
 | _ _ _ (Exp.relop o x y) e := has_relop.evl o (eval x e) (eval y e)
 | _ _ _ (Exp.getvar v) env := getEnv v env

The calls to has_binop.evl, eval, and has_relop.evl in the function all say they cannot synthesize typeclass instances for their arguments. E.g.

failed to synthesize type class instance for
eval : Π {α : Type} [_inst_1 : has_relop α] [_inst_2 : has_binop α], Exp α → Env → α,
_x : Type,
_x : has_relop _x,
_x : has_binop _x,
o : binOP,
x y : Exp _x,
e : Env
⊢ has_binop _x

[Kris Brown]

Made some fixes:

def Env:= ℤ × ℤ

inductive exVar : Type → Type
 | vx : exVar ℤ
 | vy : exVar ℤ

inductive relOP : Type
 | EQ | NEQ | LE

inductive binOP : Type
 | PLUS | MINUS

class has_relop (α : Type) :=
 (evl : relOP → α → α → bool)

class has_binop (α : Type) :=
 (evl : binOP → α → α → α)

inductive Exp : Type → Type 1
| const {α: Type } : α → Exp α
| relop {α: Type} [has_relop α]: relOP → Exp α → Exp α → Exp bool
| binop {α: Type} [has_binop α]: binOP → Exp α → Exp α → Exp α
| getvar {α: Type}  : exVar α → Exp α

def getEnv : Π{α: Type} , exVar α → Env → α
 | _  (exVar.vx) := λ env, env.1
 | _ (exVar.vy) := λ env, env.2

def eval : Π{α:Type}, Exp α → Env → α
 | _ (Exp.const x) _ := x
 | _ (Exp.relop o x y) e := has_relop.evl o (eval x e) (eval y e)
 | _ (Exp.binop o x y) e := has_binop.evl o (eval x e) (eval y e)
 | _ (Exp.getvar v) env := getEnv v env

And the sole error now is infer type failed, unknown variable __mlocal__fresh_10_435536 on Exp.relop in the definition of eval (reproducible in the Lean web editor)

[Reid Barton]

Is this really what you want to do?

[Reid Barton]

def eval : Π{α:Type}, Exp α → Env → α
 | _ (Exp.const x) _ := x
 | _ (@Exp.relop α h o x y) e := @has_relop.evl α h o (eval x e) (eval y e)
 | _ (@Exp.binop α h o x y) e := @has_binop.evl α h o (eval x e) (eval y e)
 | _ (Exp.getvar v) env := getEnv v env

[Kris Brown]

Yes! thanks for working out the root of the problem.