## Stream: math-comp users

### Topic: ✔ Way to make sense of phantoms (and mixins)

#### abab9579 (Sep 01 2022 at 07:23):

There are loads of definitions using`Phantom` & `phantom`, which I find quite hard to comprehend.
What is the go-to way to understand what they are?
For instance, for LModule there is

``````Module Lmodule.

Structure mixin_of (R : ringType) (V : zmodType) : Type := Mixin {
scale : R → V → V;
_ : ∀ a b v, scale a (scale b v) = scale (a × b) v;
_ : left_id 1 scale;
_ : right_distributive scale +%R;
_ : ∀ v, {morph scale^~ v: a b / a + b}
}.

Section ClassDef.

Variable R : ringType.

Record class_of V := Class {
base : Zmodule.class_of V;
mixin : mixin_of R (Zmodule.Pack base)
}.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c.

Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0)) :=
fun bT b & phant_id (Zmodule.class bT) b ⇒
fun m & phant_id m0 m ⇒ Pack phR (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.

End ClassDef.
``````

What is happening here?

#### Pierre Roux (Sep 01 2022 at 08:25):

This is a mechanism to infer structures, for instance being able to write `lmodType R` instead of `lmodType [ringType of R]` (the canonical instance of ring on R will be automatically found thanks to the phantom mechanism). The technical details are explained in a comment around the definition here https://github.com/coq/coq/blob/05037368dbb38c58dc0f3297b47ad8ce96be4a18/theories/ssr/ssreflect.v#L320-L339 (this part of ssreflect is integrated in Coq since a few years) or in Section 6.10.1 in the MathComp book (https://math-comp.github.io/mcb/). Note that in the midterm, all this is likely to be replaced by the reversible coercion mechanism recently introduced in Coq https://coq.github.io/doc/master/refman/addendum/implicit-coercions.html#reversible-coercions

#### abab9579 (Sep 01 2022 at 08:26):

Oh. Maybe I should wait before trying with phantom business? How long would it take for the mechanism to catch up?

#### Pierre Roux (Sep 01 2022 at 08:33):

Probably a few years (until MathComp requires Coq >= 8.16), I wouldn't wait.

#### abab9579 (Sep 01 2022 at 08:34):

Wow, years. I see, I should get accustomed to the phantom business then.

#### Notification Bot (Sep 01 2022 at 15:26):

abab9579 has marked this topic as resolved.

#### Ana de Almeida Borges (Sep 01 2022 at 19:15):

I've been using mathcomp for a while and don't really understand phantoms at all. My rule of thumb is that if I see a phantom, I did something unidiomatic at some point and should reconsider my code. (The only exception is if I `Set Printing All` in order to debug some error message, in which case phantoms are only to be expected.)

#### Ana de Almeida Borges (Sep 01 2022 at 19:17):

A possible exception to my rule would be if I needed to build something in mathcomp style that would benefit from phantoms. But since I'm only using the library, my strategy seems to work.

#### Enrico Tassi (Sep 01 2022 at 19:25):

Well, I still hope that we will release MC 2.0 before Christmas (especially thanks to your hard work @Pierre Roux ) and that branch can be a fresh start. MC 2.0 will use HB, which takes care of the phantom business, while MC 1.x will continue to live in maintenance mode.

@abab9579 unless you have a lot of backward compat constraints on Coq, I would not spend a lot of time on understanding how `Definition pack` works, since that will be automatically generated (it already is in PR 733 on MC).

FTR, also the paper "CS for the working Coq user" explains the phantom device, IIRC, in one of the last sections.

#### Enrico Tassi (Sep 01 2022 at 19:27):

But you seem to make progress very fast, given what you ask, so if you like gory details... phantoms can give you a black belt right away ;-)

#### Enrico Tassi (Sep 01 2022 at 19:28):

And I totally agree with Ana, unless you want to declare a new interface (a new structure) then you should be able to survive without phantoms.

#### abab9579 (Sep 01 2022 at 23:30):

Thank you, ana de almeida borges and enrico tassi! And yes, I exactly want to declare a new structure so that I can use it alike `linear`. Perhaps I might be able to work with reversible coercion mechanism for this case?

#### abab9579 (Sep 04 2022 at 08:18):

Oh wait, is the `HB` you talking about this? `https://github.com/math-comp/hierarchy-builder`
It certainly looks promising!

Last updated: Jul 23 2024 at 20:01 UTC