Zulip Chat Archive

Stream: new members

Topic: default typeclass instances?


view this post on Zulip Kris Brown (Jul 08 2020 at 05:55):

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

view this post on Zulip Kevin Buzzard (Jul 08 2020 at 06:05):

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

view this post on Zulip Kenny Lau (Jul 08 2020 at 06:14):

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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 06:16):

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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 06:19):

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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 06:24):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 06:27):

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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 06:28):

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

view this post on Zulip Kevin Buzzard (Jul 08 2020 at 06:45):

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

view this post on Zulip Kris Brown (Jul 08 2020 at 06:55):

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

view this post on Zulip Kris Brown (Jul 08 2020 at 07:17):

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)

view this post on Zulip Reid Barton (Jul 08 2020 at 10:53):

Is this really what you want to do?

view this post on Zulip Reid Barton (Jul 08 2020 at 10:55):

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

view this post on Zulip Kris Brown (Jul 08 2020 at 17:05):

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


Last updated: May 10 2021 at 18:22 UTC