Search code examples
typeclasscoq

Specialize `Map` typeclass into `PartialMap` typeclass

I've defined a pair of typeclasses called Map and PartialMap, with the obvious rules for such data structures. In particular, they differ only in whether they range over some V or option V.

It is clear to me that PartialMap is essentially a special case of Map. However, I'm not sure how to encode that.

Class Map M K V: Type := {
  get: M K V -> K -> V;
  set: M K V -> K -> V -> M K V;
  map_get_set_idem: forall (m: M K V) (k: K) (v: V), get (set m k v) k = v;
  map_get_set_comm: forall (m: M K V) (k1 k2: K) (v: V), ~(k1 = k2) -> get (set m k1 v) k2 = get m k2;
}.

Class PartialMap M K V: Type := {
  pget: M K V -> K -> option V;
  pset: M K V -> K -> option V -> M K V;
  pmap_pget_pset_idem: forall (m: M K V) (k: K) (v: option V), pget (pset m k v) k = v;
  pmap_pget_pset_comm: forall (m: M K V) (k1 k2: K) (v: option V), ~(k1 = k2) -> pget (pset m k1 v) k2 = pget m k2;
}.
Solution

  • Turns out that parameterizing M by K and V is totally superfluous.

    Class Map M K V: Type := {
  get: M -> K -> V;
  set: M -> K -> V -> M;
  map_get_set_idem: forall m k v, get (set m k v) k = v;
  map_get_set_comm: forall m k1 k2 v, ~(k1 = k2) -> get (set m k1 v) k2 = get m k2;
}.

Class PartialMap M K V: Type := {
  PartialMapIsMap :> Map M K (option V)
}.