Zulip Chat Archive

Stream: general

Topic: combining classes


view this post on Zulip Reid Barton (Dec 13 2018 at 04:24):

If I have class C t extends A t, B t. I guess it doesn't mean that anything which is an instance of A and B is automatically an instance of C? Does it make sense to write an instance for C to make that true?

view this post on Zulip Reid Barton (Dec 13 2018 at 04:26):

hmm, it seems not to be a good idea.

view this post on Zulip Mario Carneiro (Dec 13 2018 at 05:08):

no, it means that a C t is an A t and a B t

view this post on Zulip Mario Carneiro (Dec 13 2018 at 05:08):

so that instance would be a loop

view this post on Zulip Reid Barton (Dec 13 2018 at 05:12):

So is it a bad idea to define this class C in the first place then?

view this post on Zulip Mario Carneiro (Dec 13 2018 at 05:30):

It has the same concerns as any other class introduction

view this post on Zulip Reid Barton (Dec 13 2018 at 05:36):

I can't use C as a shorthand for A + B though

view this post on Zulip Reid Barton (Dec 13 2018 at 05:37):

because I don't see any way to arrange that there is an instance of C whenever there is one of both A and B

view this post on Zulip Reid Barton (Dec 13 2018 at 05:38):

In GHC, this works because GHC doesn't have these weird backwards instances "try to get A from C"

view this post on Zulip Reid Barton (Dec 13 2018 at 05:38):

In particular, I'm looking at https://github.com/leanprover/mathlib/blob/master/category_theory/fully_faithful.lean#L52

view this post on Zulip Johan Commelin (Dec 13 2018 at 05:54):

Right, so I've only been proving that things are fully_faithful but I never put it as an assumption. It's a bit awkard.

view this post on Zulip Reid Barton (Dec 13 2018 at 05:55):

I guess that works, to an extent

view this post on Zulip Johan Commelin (Dec 13 2018 at 06:29):

@Reid Barton But you would also want the type class system to try to deduce that F is full by searching for an instance that F is fully_faithful (which you say GHC wouldn't do). So the search must go both ways. We really need a smarter system, that wouldn't run into these trivial loops.

view this post on Zulip Mario Carneiro (Dec 13 2018 at 06:30):

GHC would require that you prove F is full before proving it is fully_faithful, so it doesn't have to do the search

view this post on Zulip Andrew Ashworth (Dec 13 2018 at 07:39):

The smarter you make type class search, the more memory it will use... I'm sure you could use high power search techniques like contraction hierarchies, along with keeping visited nodes in memory so you could detect loops... I suspect/speculate it hasn't been done because 90% of CS users would riot over the unnecessary resource usage in large projects that do not need these features. Maybe I'm completely off-base.

view this post on Zulip Andrew Ashworth (Dec 13 2018 at 07:41):

It would definitely be interesting to benchmark different algorithms over a large code-base though - those would be interesting results.

view this post on Zulip Johan Commelin (Dec 13 2018 at 07:44):

I understand.

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 07:45):

Mathematicians seem to me to be a class of users who are constantly running into these issues with the type class system though.

view this post on Zulip Johan Commelin (Dec 13 2018 at 07:45):

Lean 4 will give us the possibility to swap out the type class search algorithm...

view this post on Zulip Johan Commelin (Dec 13 2018 at 07:45):

So then everyone can be happy.

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 07:46):

You made group a class and we thought "Oh I get it, a locally analytic topological vector space must be a class" and then it turns out that it's harder than that

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 07:48):

@Reid Barton in a given use case you could try adding the loopy instance with priority 0, and then hope that this discouragement is enough in practice. It feels like any code you ship should come with a warning though.

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 07:50):

The system would be likely to loop rather than fail so for buggy code where it should error with a failure you'll instead perhaps get a more obscure error

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 07:53):

Johan I guess I made one explicit example of where we weren't happy very clear to Sebastian the other day -- type class inference failing to unify two terms of a subsingleton type -- so he knows we want more here. Loops are another issue. We definitely want them. "Defeq loops" should be fine but even they can cause problems because the system doesn't abort. "Oh look we've been here before -- let's press on"

view this post on Zulip Gabriel Ebner (Dec 13 2018 at 09:16):

Haskell has this nice constraint kinds extension, which allows you to define aliases for combinations of type classes:

type Stringy a = (Read a, Show a) -- Read and Show are type classes
type C t = (A t, B t) -- Reid's example

In principle, there is no fundamental reason why we couldn't do something like this in Lean as well. @Johan Commelin I wouldn't count on customizing type class inference.

view this post on Zulip Johan Commelin (Dec 13 2018 at 09:18):

Ooh, too bad. I thought I heard at some point that it would be possible...


Last updated: May 14 2021 at 00:42 UTC