Stream: math-comp users

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

view this post on Zulip 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?

view this post on Zulip 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 (this part of ssreflect is integrated in Coq since a few years) or in Section 6.10.1 in the MathComp book ( Note that in the midterm, all this is likely to be replaced by the reversible coercion mechanism recently introduced in Coq

view this post on Zulip 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?

view this post on Zulip Pierre Roux (Sep 01 2022 at 08:33):

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

view this post on Zulip 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