Zulip Chat Archive

Stream: general

Topic: how does type class inference work?


view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:09):

class foo (A : Type) :=
(blah : )

class bar (A : Type) extends foo A :=
(blah2 : bool)

class baz (A : Type) extends foo A .

instance : bar  := {blah := 4, blah2 := tt}

example : bar  := by apply_instance -- works

example : baz  := by apply_instance -- fails

Why doesn't this work?

view this post on Zulip Mario Carneiro (Dec 10 2018 at 09:25):

why would it work? You declared an instance of bar but not baz

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:30):

I can figure out how to make an instance of baz, that's why I can believe it would work. All the fields are there. This is my problem -- I don't know what the type class inference system is _doing_.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:31):

Oh sorry there's a typo -- I meant to write

example : foo ℤ := by apply_instance -- works

I didn't declare an instance of foo but it found it anyway.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:32):

I literally do not know what it can and cannot do.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:32):

All I know is that it can do less than me, because I can solve baz.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:33):

class baz (A : Type) extends foo A .
this creates an instance baz.to_foo

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:33):

if you want to make baz from foo then you would need to use { .. infer_instance }

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:33):

Well, maybe I should just create an instance baz.from_foo

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:34):

or maybe foo.to_baz would be more appropriate.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:35):

congratulations, you've thrown yourself into a loop

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:37):

class foo (A : Type) :=
(blah : )

class bar (A : Type) extends foo A :=
(blah2 : bool)

class baz (A : Type) extends foo A .

instance : bar  := {blah := 4, blah2 := tt}

example : foo  := by apply_instance -- works

-- type class inference is so stupid, why doesn't it just guess this.
instance foo.to_baz (A : Type) [foo A] : baz A := by refine {}

example : foo  := by apply_instance -- fails? WTF?

example : baz  := by apply_instance -- still fails

I broke everything.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:37):

I don't understand why everything is broken. Everything is defeq, right?

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:38):

you now have foo.to_baz and baz.to_foo

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:38):

so the machine gets stuck forever

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:39):

example (A : Type) (H : foo A) : H = baz.to_foo A := rfl

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:40):

I don't understand why it gets stuck forever. What is it doing? I am pretty convinced it's not playing the "let's see how many instances I can make from this instance, for no reason whatsoever" game. I ask the type class inference system to produce me a term of a typeclass, it should just try and try until it finds one and then stop.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:40):

Of course I completely understand that I have made a loop. What I don't understand is why this even matters.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:40):

oh it is playing that game

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:40):

It is??

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:40):

wait no it isn't

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:41):

But your response makes me think that you can write some simple thing which will make it play this game.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:41):

well you want it to figure out baz. then it goes like "hey I can make this from foo". then it goes like "hey I can make this from baz". ad nauseam

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:41):

so maybe priority is the answer

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:42):

Do you know where it starts? At the top or the bottom?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:42):

It says "Hmm, I want to make an instance of baz A". Now does it say "OK so how do we make instances of baz A? or does it say "OK what other typeclasses can I make with A"? Hmm, I guess it must be the former.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:43):

it is the former

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:43):

So the type class system looks through all instances and tries to find one whose head term is baz?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:44):

Say it finds ten such things. What does it do now?

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:44):

apply each one

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:44):

(but mind you, it uses depth-first search)

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:44):

"Head term" -- is that the right phrase? I mean "a term which is a function baz [something]

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:44):

What is depth-first search?

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:45):

depth-first search = dig this hole as deep as possible until you find gold or you are blocked by a stone, and then move on to the next hole

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:45):

Is this the one where it finds the first instance of baz A and finds that it needs moo A and it checks for a term of type moo A and temporarily forgets all about the other nine ideas about baz and just looks for moo stuff?

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:46):

breadth-first search = dig this hole 1 cm, go to next hole and dig 1cm, and so on until you run out of holes, and then go back to the first hole and dig 1cm, etc

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:46):

Is this the one where it finds the first instance of baz A and finds that it needs moo A and it checks for a term of type moo A and if it can't find that it forgets all about the other nine ideas about baz and just looks for moo stuff?

precisely

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:46):

How does it conclude that it is blocked by a stone?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:47):

Can this only happen when there are literally no instances which have the right head term or whatever the phrase is?

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:47):

yes

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:48):

so for example there is no instance that produces ordered_canonical_discrete_ordered_field or whatever the flying that is

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:48):

because it's the highest structure

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:49):

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

Does this segfault for you?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:50):

I am trying to do some simple experiments.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:50):

no it doesn't

view this post on Zulip Sebastian Ullrich (Dec 10 2018 at 09:52):

Can this only happen when there are literally no instances which have the right head term or whatever the phrase is?

No, it's sufficient that no instance of the target class can be unified with the target

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:53):

Hmm, thanks, I'll restart VS Code.

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:54):

@Sebastian Ullrich what's the difference?

view this post on Zulip Patrick Massot (Dec 10 2018 at 09:54):

The head symbol could match but not the rest

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:55):

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

class H111 (A : Type) extends H11 A .

class H121 (A : Type) extends H12 A .

instance H1.to_H11 (A : Type) [H1 A] : H11 A := by refine {}

instance H11.to_H111 (A : Type) [H11 A] : H111 A := by refine {}

instance : H121 unit := by refine {}

instance : H111 unit := by apply_instance

That seems to have gone really well.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:56):

I am trying to get into trouble. I am trying to get max class inference thingy error

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:57):

but you didn't create any loop...

view this post on Zulip Kenny Lau (Dec 10 2018 at 09:57):

oh wait you did

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:57):

Right, H1 and H11 loop

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 09:57):

but I managed to get past the loop and up to H111

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:06):

Kevin, in your case there exactly one instance to try at each step, and it clearly succeeds without ever risking a loop:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : H111 unit := @H11.to_H111 ?x_1 ?x_2
[class_instances] (1) ?x_2 : H11 unit := @H1.to_H11 ?x_3 ?x_4
[class_instances] (2) ?x_4 : H1 unit := @H12.to_H1 ?x_5 ?x_6
[class_instances] (3) ?x_6 : H12 unit := @H121.to_H12 ?x_7 ?x_8
[class_instances] (4) ?x_8 : H121 unit := unit.H121

You can simply draw the instance graph and see it

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:24):

I want to make it get stuck in a loop

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:25):

To find H111 it suffices to find H1. Can I make it look for H1 by going back to H12?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:26):

Oh I see, that instance is not even there.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:27):

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

class H111 (A : Type) extends H11 A .

class H121 (A : Type) extends H12 A .

instance H1.to_H11 (A : Type) [H1 A] : H11 A := by refine {}

instance H11.to_H111 (A : Type) [H11 A] : H111 A := by refine {}

instance H1.to_H12 (A : Type) [H1 A] : H12 A := by refine {}

instance H12.to_H121 (A : Type) [H12 A] : H121 A := by refine {}

instance : H121 unit := by refine {}

instance : H111 unit := by apply_instance -- max depth reached

Bingo.

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:27):

So whatever is type class inference thinking here? Why go back to H12 when we have been there already?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:30):

set_option trace.class_instances true
instance : H111 unit := by apply_instance -- max depth reached

gives random stuff such as

[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one

Who said anything about nat?

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 10:31):

I'm glad the type class inference system's job isn't finding its way out of mazes.

view this post on Zulip Mario Carneiro (Dec 10 2018 at 10:33):

usually one writes a depth first search with a search stack to prevent loops like this

view this post on Zulip Patrick Massot (Dec 10 2018 at 10:33):

The nat thing is related to my question to Sebastian about shortcut. It has nothing to do with your problem, it's something Lean solves for itself in its meta-work

view this post on Zulip Mario Carneiro (Dec 10 2018 at 10:33):

I'm not sure why typeclass inference doesn't have one

view this post on Zulip Mario Carneiro (Dec 10 2018 at 10:34):

then again, this wouldn't prevent problems with loops that look different the second time around

view this post on Zulip Mario Carneiro (Dec 10 2018 at 10:34):

i.e. the same instances are being used but the instantiations are different

view this post on Zulip Kevin Buzzard (Dec 10 2018 at 11:07):

OK this is great. I have to interview a bunch of people now but I will probably be back later on with more dumb questions. This has been a great start. Thanks to all.

view this post on Zulip Joe Hendrix (Dec 10 2018 at 19:20):

Conceptually, Lean could require one to prove instance backchaining is well-founded. Haskell has static checks to ensure this, but those can be bypassed via language pragma.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:07):

I'm coming back to this; I'm trying to understand the details of type class inference better, because mathematicians are better at doing type class inference than Lean.

What's going on here?

import algebra.pi_instances -- prod.add_group defined here

example : add_group () := by apply_instance
example : add_group ( × ) := by apply_instance
example : add_group ( ×  × ) := by apply_instance
example : add_group ( ×  ×  × ) := by apply_instance
example : add_group ( ×  ×  ×  × ) := by apply_instance -- fails

#check prod.add_group

view this post on Zulip Mario Carneiro (Apr 20 2019 at 11:09):

I'm pretty sure if you look at the instance trace it will be 5 orders of magnitude longer than you think it should be

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:12):

import algebra.pi_instances -- prod.add_group defined here

set_option trace.class_instances true
-- set_option class.instance_max_depth 39 -- a fix

example : add_group () := by apply_instance -- needs class.instance_max_depth 7
example : add_group ( × ) := by apply_instance -- needs 15
example : add_group ( ×  × ) := by apply_instance -- needs 23
example : add_group ( ×  ×  × ) := by apply_instance -- needs 31
example : add_group ( ×  ×  ×  × ) := by apply_instance -- default is 32

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:12):

Yeah, my search through the tree is a lot more efficient than Lean's.

view this post on Zulip Johan Commelin (Apr 20 2019 at 11:13):

Can't we have set_option class_instance.backend Kevin?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:13):

It could send me a notification on Zulip and I'll suggest some hints.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:14):

OK it is time for me to understand the output of trace.class_instances.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:14):

Here's Lean trying to prove the trivial statement that Z^4 is a group:

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:15):

https://gist.github.com/kbuzzard/94813d4b0a01f896f740c91b2d971cd8

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:15):

Let's start at the top.

[class_instances] (0) ?x_0 : add_group (ℤ × ℤ × ℤ × ℤ) := @prod.add_group ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_3 : add_group ℤ := @prod.add_group ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @pi.add_group ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @subtype.add_group ?x_12 ?x_13 ?x_14 ?x_15
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @additive.add_group ?x_16 ?x_17
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @add_comm_group.to_add_group ?x_18 ?x_19
[class_instances] (2) ?x_19 : add_comm_group ℤ := @prod.add_comm_group ?x_20 ?x_21 ?x_22 ?x_23

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:15):

What does (0), (1) and (2) mean?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:16):

It seems to me that Lean has _very_ quickly decided that prod.add_group is a good idea.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:16):

Why?

view this post on Zulip Keeley Hoek (Apr 20 2019 at 11:16):

The number is the depth of the search so-far,
and I think it found it just trying in some random order, respecting priorities

view this post on Zulip Keeley Hoek (Apr 20 2019 at 11:17):

So for example there are multiple (1)s because the first few things at that depth which it tries were rejected, before it found something the could possibly work (it didn't give a failed is_def_eq) there

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:17):

Obviously prod.add_group is a good first move. But then its next move is an attempt to prove add_group Z using pi.add_group which is equally obviously a completely stupid move.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:19):

So I believe we are doing a depth-first search here, and my understanding is that the (n) is telling us the depth we're allowed to go before...what? Before giving up?

view this post on Zulip Mario Carneiro (Apr 20 2019 at 11:20):

The pi.add_group is not a horrible move; it is quickly discarded without an expensive subproof

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:20):

Before giving up going down that hole and turning back, presumably, rather than giving up and saying maximum class-instance resolution depth has been reached?

view this post on Zulip Mario Carneiro (Apr 20 2019 at 11:21):

the (n) is just telling you what depth we are at currently, AFAIK it's not (directly) connected to a timeout

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:21):

Why is it discarded? Because the "head terms" don't match? Is that the correct phrase? Is the "head term" of int just int, and the "head term" of pi.add_group is something else?

view this post on Zulip Mario Carneiro (Apr 20 2019 at 11:21):

yes

view this post on Zulip Mario Carneiro (Apr 20 2019 at 11:22):

lean knows that pi bla bla != int

view this post on Zulip Rob Lewis (Apr 20 2019 at 11:22):

To make things extra confusing, there are two notions of depth in type class search -- iirc, the max_depth option is not controlling the maximum number that you see in the trace, it's something to do with the backtracking depth. But I might be misremembering the details. Johannes wrote something about this last month.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:22):

pi.add_group :
  Π {I : Type u_1} {f : I  Type u_2} [_inst_1 : Π (i : I), add_group (f i)], add_group (Π (i : I), f i)

For this to work, indeed int would have to be Pi ....

view this post on Zulip Rob Lewis (Apr 20 2019 at 11:23):

https://github.com/johoelzl/tc-log-parser

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:23):

So is my observation "clearly this won't work" exactly what Lean is doing here? It has a big list of a whole bunch of definitions all tagged with the instance tag, and it looks at all of the instances of the form X -> add_group Y or add_group Y and then tries them all in a random order?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 11:24):

oh crap, chores beckon. Back in 30 minutes. I want to understand why we're using up 8 levels for each extra int.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 12:42):

https://github.com/johoelzl/tc-log-parser

Has anyone talked to Sebastian or Leo about this issue?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 12:45):

#print notation × -- _ ×:35 _:34 := prod #1 #0 -- \times is right associative!

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 12:51):

[class_instances] (1) ?x_3 : add_group ℤ := @prod.add_group ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq

That fails because int isn't prod ?x ?y for any choices of ?x and ?y. But

[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36
[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36

That's a different failure, right? Lean figured that if it could find a term of type linear_nonneg_ring ℤ then it would be done, but it does not even write

[class_instances] (4) ?x_36 : linear_nonneg_ring ℤ := ...

--- why not?

How do I find every instance of X1 -> X2 -> ... -> Xn -> linear_nonneg_ring x in Lean's type class inference system? Here n can be 0.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:04):

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : inhabited ℕ := @quotient_add_group.inhabited ?x_1 ?x_2 ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @quotient_group.inhabited ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @parser.inhabited ?x_11
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @array.inhabited ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @d_array.inhabited ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @vector.inhabited ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @finset.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @multiset.inhabited ?x_22
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := int.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @unique.inhabited ?x_23 ?x_24
[class_instances] (1) ?x_24 : unique ℕ := punit.unique
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @psigma.inhabited ?x_1 ?x_2 ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sigma.inhabited ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @set.inhabited ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := tactic.rcases_patt_inverted.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := tactic.rcases_patt.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := punit.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := occurrences.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := environment.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := expr.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := level.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := format.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := options.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := option.inhabited ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := name.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sum.inhabited_right ?x_11 ?x_12 ?x_13
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sum.inhabited_left ?x_14 ?x_15 ?x_16
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @subtype.inhabited ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := string.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := char.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := list.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := nat.inhabited

Even though, when I make a term of type inhabited ℕ as an instance, Lean by default calls it nat.inhabited -- even though this, Lean doesn't think to look for nat.inhabited as the answer when it's trying to solve inhabited ℕ using type class inference?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:08):

...
[class_instances] (0) ?x_0 : inhabited Prop := string.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := char.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := list.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := nat.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @prod.inhabited ?x_22 ?x_23 ?x_24 ?x_25
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := true.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := bool.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @pi.inhabited ?x_26 ?x_27 ?x_28
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @fun.inhabited ?x_29 ?x_30 ?x_31
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := prop.inhabited

You are so dumb Lean! What did you think it was going to be called??

view this post on Zulip Keeley Hoek (Apr 20 2019 at 13:08):

Hahaha!

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:09):

36 failures before it hit upon that one

view this post on Zulip Keeley Hoek (Apr 20 2019 at 13:09):

:D

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:17):

Actually that's a really good point. With a proper indexing lean could just guess the name and skip the search

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:19):

The answer to your earlier question is #print instances linear_nonneg_ring

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:19):

There are no instances of linear_nonneg_ring, so it probably performed the (empty) search and that's why you don't see it

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:20):

Thanks. I just learnt about #print instances from re-reading TPIL.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:21):

OK so I tried to explain type class inference to my 16 year old son and basically I realised that I had to abstract it before I could explain it. How does this sound?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:22):

We have 1000 puzzles, P1 up to P1000. We also have a bunch of techniques: each technique is of the form "if you can solve this finite set of puzzles, you can also solve that puzzle". For example if you can solve P1 and P3 and P10, you can also solve P11.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:23):

A degenerate example of a technique is "if you can solve no puzzles at all, then you can solve P1"

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:23):

The question is: "solve puzzle 53"

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:23):

(using only the techniques you have).

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:24):

My son suggested first solving all the puzzles which need no input; I guess that's all the instances which are just of the form ring int or whatever.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:25):

Now is this the point where I need to understand what a prolog-like search is?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:26):

If this were an IOI problem, I would be told how many puzzles there were and how many techniques.

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:26):

Each technique is an instance in Lean I guess.

view this post on Zulip Chris Hughes (Apr 20 2019 at 13:26):

Actually that's a really good point. With a proper indexing lean could just guess the name and skip the search

How much easier is checking whether a bunch of strings matches prop.inhabited than checking whether a bunch of Types matches inhabited Prop?

Also, I'm surprised that the error is failed is_def_eq. Doesn't type class inference care about syntactic equality?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:26):

Oh -- my son is asking if there can be loops!

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:30):

It's much easier to check whether prop.inhabited is what we want, because we don't have to linearly search through instances, we can just jump straight to the def by name

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:31):

It uses defeq with a really strict unfold predicate

view this post on Zulip Mario Carneiro (Apr 20 2019 at 13:32):

so that it can handle reducible defs and beta reduction

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:34):

I thought that the whole point of wrapper types was that you absolutely did not want Lean to solve has_add my_int by noticing that my_int was defined to be int and solving has_add int

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 13:35):

I told my son that in Lean and mathlib they try to avoid loops. We don't want P6 -> P7 and P7 -> P6.

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:00):

We don't, unless we do

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:00):

Most types are not marked reducible for exactly this reason

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:01):

but reducible types are transparent to typeclass inference, which can be convenient if you want to inherit all the typeclasses from the original

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:02):

There are lots of implementations of prolog

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:02):

Why doesn't Leo just use one of these and get it to solve typeclass problems for him?

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:02):

prolog is quite a bit better at this than lean

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:03):

there are mechanisms for controlling the search, avoiding backtracking and ordering rules, etc

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:04):

I don't really know if typeclass search is actually an issue in practice, but I guess one day it might become an issue

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:05):

I guess my students having hard-to-debug code because they accidentally coerced an int to a nat is an issue

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:06):

I am completely confused by this still. Why does Lean try to solve [has_zero nat] in lots of ways and then have [has_neg nat] fail every time?

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:06):

That's my understanding of what was going on there

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:07):

Lots of different but defeq solutions to 0 and 1

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 14:07):

And then a possibly expensive add and a failing neg

view this post on Zulip Mario Carneiro (Apr 20 2019 at 14:49):

My view on this is that typeclass inference needs a major rewrite, we can do much better than what we have today

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:14):

well, you can definitely add a bunch of heuristics

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:14):

if you like slides and python-ish pseudocode, http://aima.eecs.berkeley.edu/slides-pdf/chapter05.pdf

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:15):

is the CS undergrad overview of backtracking

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:17):

with accompanying pdf: http://aima.cs.berkeley.edu/newchap05.pdf

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 15:27):

Thanks Andrew. Part of me wants to go back to college and do an UG degree in computer science, except skipping all the hardware stuff

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 15:28):

But I guess I know now that I can learn this stuff from references; I just need to be pointed in the right direction.

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:51):

abusing type class inference to solve the n-queens problem in lean: https://gist.github.com/Kha/2cdd2df8bd318019bea75f1ea87ae4a0

view this post on Zulip Andrew Ashworth (Apr 20 2019 at 15:51):

I always thought this example was cute

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 15:54):

equation type mismatch, term
  ``(0)
has type
  expr ff
but is expected to have type
  expr

:-(

view this post on Zulip Mario Carneiro (Apr 20 2019 at 15:56):

replace the triple backtick with single


Last updated: May 08 2021 at 04:14 UTC