2
$\begingroup$

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6.10 and 7.1 about phantom types and tuples (weirdly 6.10 ends with "The rest of this section introduces the general mechanism of phantom types..." and then immediately moves on to the next chapter, but that is not my question).

In tuple.v, the [tuple of s] notation to construct a tuple from a seq is defined using a function tuple which seemingly does nothing:

Definition tuple t mkT : tuple_of :=
  mkT (let: Tuple _ tP := t return size t == n in tP).

As far as I can tell, tuple is only used to trigger unification. But mathcomp introduces more general methods to trigger unification, namely phantom types.

Is there a reason the [tuple of s] constructor is not defined as my_tuple:

Section TupleDef.
  Variables (n : nat) (T : Type).
  Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
  Canonical tuple_subType := Eval hnf in [subType for tval].

  Definition tuple t mkT : tuple_of :=
    mkT (let: Tuple _ tP := t return size t == n in tP).

  Definition my_tuple t (H : phantom _ (tval t)) := t.       (* Difference here *)
End TupleDef.

Notation "[ 'tuple' 'of' s ]" := (tuple (fun sP => @Tuple _ _ s sP))
  (at level 0, format "[ 'tuple'  'of'  s ]") : form_scope.
Notation "[ 'my_tuple' 'of' s ]" := (my_tuple (Phantom _ s)) (* and here *)
  (at level 0, format "[ 'my_tuple'  'of'  s ]") : form_scope.

Canonical nil_tuple T := Tuple (isT : @size T [::] == 0).
Canonical cons_tuple n T x (t : tuple_of n T) :=
  Tuple (valP t : size (x :: t) == n.+1).

Compute    [tuple of [:: 1;2;3]] : seq nat.
Compute [my_tuple of [:: 1;2;3]] : seq nat.                  (* and here *)

using phantom to lift the seq term to the type level and trigger unification? Is there a difference in practice? Or is tuple.v just old code that was never updated to use phantom?

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.