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 usingPhantom & 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.

Last updated: Jan 29 2023 at 19:02 UTC