Zulip Chat Archive

Stream: maths

Topic: Typeclasses for ConvexCone

Apurva Nakade (Jul 27 2023 at 19:21):

Should we turn docs#ConvexCone.Pointed into a class? This came in another thread. This will also let me convert docs#ProperCone to a class. Both docs#ConvexCone.Pointed and docs#ProperCone have nice algebraic structures (AddCommMonoid, Module (k \ge 0), maybe more?).

Eric Wieser (Jul 27 2023 at 19:40):

I don't think it would make any sense for ProperCone to be a class

Apurva Nakade (Jul 27 2023 at 19:58):

I need the Module structure on either PointedCone or ProperCone to then define direct sums. Should I just keep using Fact Pointed?

Apurva Nakade (Jul 27 2023 at 19:59):

Or is there a less hacky way than using Fact

Anatole Dedecker (Jul 27 2023 at 20:31):

Why not have a PointedCone type?

Eric Wieser (Jul 27 2023 at 21:29):

Oh, I didn't say that ConvexCone.Pointed is a nonsensical typeclass; it's perhaps controversial, but it would certainly be one approach to what you're trying to do

Apurva Nakade (Jul 27 2023 at 22:31):

Anatole Dedecker said:

Why not have a PointedCone type?

The problem I'm facing is with typeclass inferencing. Just defining a Type will probably still keep the issue unresolved.

Apurva Nakade (Jul 27 2023 at 22:33):

I need to build a heirarchy of structures on docs#ProperCone to define direct sums and without a "Cone" typeclass the code is getting very hacky.

Eric Wieser (Jul 27 2023 at 22:41):

You might want a ConeClass typeclass to mirror how we have AddSubmonoid and AddSubmonoidClass

Notification Bot (Jul 28 2023 at 03:14):

Apurva Nakade has marked this topic as resolved.

Notification Bot (Jul 31 2023 at 15:21):

Apurva Nakade has marked this topic as unresolved.

Last updated: Dec 20 2023 at 11:08 UTC