Stream: math-comp users

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

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: Feb 02 2023 at 13:03 UTC