Zulip Chat Archive

Stream: general

Topic: Modules

Morenikeji Neri (Jul 25 2018 at 22:39):

Why is is_linear_map not a class?

Patrick Massot (Jul 25 2018 at 22:42):

I think it's for historical reasons

Morenikeji Neri (Jul 25 2018 at 22:49):

care to explain further?

Kevin Buzzard (Jul 25 2018 at 23:15):

Here's a related question -- would a PR which made it a class be appreciated? It's in algebra/module.lean -- oh -- I see that file was written back in 2015! Wow! It's a prop so there are presumably no diamond issues. It seems an ideal thing to be a class. What am I missing?

Chris Hughes (Jul 25 2018 at 23:17):

I'm guessing the reason might be something to do with the type class inference problems with modules, meaning it doesn't get inferred.

Patrick Massot (Jul 26 2018 at 07:55):

care to explain further?

I mean this was written before we started to use classes for such things, and it was not changed since then. So the relevant question is indeed Kevin's one.

Patrick Massot (Jul 26 2018 at 07:56):

And of course Chris' worry is also relevant, modules are tricky for the type class inference system.

Kevin Buzzard (Jul 26 2018 at 07:56):

I'm guessing the reason might be something to do with the type class inference problems with modules, meaning it doesn't get inferred.

What are these issues? I used modules yesterday and they worked fine....ooh! A link!

Kevin Buzzard (Jul 26 2018 at 07:57):

Wait, that link tells me nothing. I wanted to add to it but I'm hoping that someone other than me adds to it. I am adding something now.

Last updated: Dec 20 2023 at 11:08 UTC