Typeclasses for ConvexCone

Stream: maths

[Apurva Nakade]

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]

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

[Apurva Nakade]

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

[Apurva Nakade]

Or is there a less hacky way than using Fact

[Anatole Dedecker]

Why not have a PointedCone type?

[Eric Wieser]

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]

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]

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]

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

[Notification Bot]

Apurva Nakade has marked this topic as resolved.

[Notification Bot]

Apurva Nakade has marked this topic as unresolved.