2017-11-26 17 views
2

私はMapPartialMapと呼ばれる一対のタイプメスを定義しました。特に、それらは、Vまたはoption Vを超えているかどうかでのみ異なります。`PartialMap` typeclassに` Map`型を特化する

PartialMapは、本質的にはMapという特殊なケースです。しかし、私はそれをどのようにエンコードするのか分かりません。

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; 
}. 

答えて

0

KによってMVをパラメータ化することは全く不必要であることが判明しました。

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) 
}. 
関連する問題