Stream: Hierarchy Builder devs & users

Topic: Implicit arguments in mixins

Xavier Allamigeon (Mar 02 2021 at 15:51):

Hi, I was playing with preorders using HB:

HB.mixin
  Record PreOrder_of_Type A := {
    ord       : rel A;
    ord_refl  : reflexive ord;
    ord_trans : transitive ord }.

HB.structure
  Definition PreOrder := { A of PreOrder_of_Type A }.

Now I want to add another mixin to get partial orders, e.g.,

HB.mixin
  Record Order_of_PreOrder A of PreOrder A := {
    ord_anti : antisymmetric (@ord A)
  }.

but of course, this doesn't work, as ord expects a PreOrder.type while here, A is just a Type. What's the idiomatic way to deal with this?

Pierre Roux (Mar 02 2021 at 16:20):

I think in dioid I just wrote something like @antisymmetric A ord

Xavier Allamigeon (Mar 02 2021 at 16:22):

Agree.

Xavier Allamigeon (Mar 02 2021 at 16:27):

But I wonder what happens if antisymmetric is a notation.

Pierre Roux (Mar 02 2021 at 16:36):

Then maybe something like @ord (PreOrder.clone A _) (haven't tried though)

Cyril Cohen (Mar 02 2021 at 16:50):

Xavier Allamigeon said:

but of course, this doesn't work, as ord expects a PreOrder.type while here, A is just a Type. What's the idiomatic way to deal with this?

You can use [the PreOrder.type of A]

Cyril Cohen (Mar 02 2021 at 16:52):

Pierre Roux said:

Then maybe something like @ord (PreOrder.clone A _) (haven't tried though)

This should work as well.

Enrico Tassi (Mar 02 2021 at 17:21):

IMO a type annotation is simpler. HB will put on A a canonical PreOrder before typing the mixin fields, but the missing piece of info is that you talk about A when you mention ord:

From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ssrbool ZArith.

HB.mixin
  Record PreOrder_of_Type A := {
    ord       : rel A;
    ord_refl  : reflexive ord;
    ord_trans : transitive ord }.

HB.structure
  Definition PreOrder := { A of PreOrder_of_Type A }.

HB.mixin
  Record Order_of_PreOrder A of PreOrder A := {
    ord_anti : antisymmetric (ord : A -> _)
  }.

Enrico Tassi (Mar 02 2021 at 17:22):

Maybe (ord : rel A) would be more polite in this specific case

Enrico Tassi (Mar 02 2021 at 17:24):

These phenomena are quite recurrent in our demos, we should probably write an FAQ

Last updated: Jan 29 2023 at 15:02 UTC