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 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

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.

view this post on Zulip Notification Bot (Sep 01 2022 at 15:26):

abab9579 has marked this topic as resolved.

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

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

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

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

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

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

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC