Hello,
On my journey to replace typeclasses by HB in FreeSpec, I stumbled upon an issue with the interfaces.
In FreeSpec, one wants to be able to describe abstract interfaces that can be composed together. For this purpose they introduced a Polymorphic Composite Interface. The main typeclasses used for this are these ones :
Definition interface := Type -> Type.
Class MayProvide (ix i : interface) : Type :=
{ proj_p {α} (e : ix α) : option (i α)
}.
Class Provide (ix i : interface) `{MayProvide ix i} : Type :=
{ inj_p {α} (e : i α) : ix α
; proj_inj_p_equ {α} (e : i α) : proj_p (inj_p e) = Some e
}.The best translation I came across in HB is the following one :
Definition interface : UU0 := (UU0 -> UU0).
HB.structure Definition MayProvide (i : interface) :=
{ ix of IsMayProvide i ix }.
HB.mixin Record IsProvide ( i ix : interface ) of MayProvide i ix := {
inj_p : forall {α : UU0}, i α -> ix α;
proj_inj_p_equ :
forall {α : UU0} (e : i α),
proj_p α (inj_p e) = Some e
}.
HB.structure Definition Provide (i : interface) :=
{ ix of IsProvide i ix & IsMayProvide i ix }. Where ix (the composite interface) becomes the carrier.
But now, I need to design multiple providers. In FreeSpec, we find two examples :
(* Provide multiple *)
Class Provide2 ix i1 i2 `{Provide ix i1, Provide ix i2}.(* Don't mess up the interfaces *)
Class Distinguish (ix i j : interface) `{Provide ix i, MayProvide ix j} : Prop :=
{
distinguish : forall {α} (e : i α), proj_p (i := j) (inj_p (ix := ix) e) = None
}.And I can manage to make something that types for both in HB :
HB.mixin Record IsProvide2 (i j ix : interface) of Provide i ix & Provide j ix := {
}.
HB.structure Definition Provide2 (i j : interface) :=
{ix of IsProvide2 i j ix
& Provide j ix & MayProvide j ix
& Provide i ix & MayProvide i ix
}.
(* A first description before Distinguish *)
HB.mixin Record IsCombinedProvider (i j ix : interface) of Provide i ix & MayProvide j ix & MayProvide i ix:= {
}.
HB.structure Definition CombinedProvider (i j : interface) :=
{ix of IsCombinedProvider i j ix & IsProvide i ix & IsMayProvide j ix & IsMayProvide i ix }.But, the problem arises when I want to use the first interface provided (i) for ix :
Example section :
Section t.
Variables (i j : interface) (ix : Provide2.type i j).
Variables (α : UU0) (e : i α).
Check inj_p.
(*
inj_p
: forall α0 : UU0, ?i α0 -> ?s α0
where
?i : [i : interface j : interface ix : Provide2.type i j α : UU0 e : i α |- interface]
?s : [i : interface j : interface ix : Provide2.type i j α : UU0 e : i α
|- Provide.type ?i]
*)
Check inj_p (s:=ix).
(*
inj_p
: forall α : UU0, j α -> ix α
*)
Fail Check proj_p (s:=ix) (i:=i).
(*
The command has indeed failed with message:
In environment
i, j : interface
ix : Provide2.type i j
α : UU0
e : i α
The term "ix" has type "Provide2.type i j" while it is expected to have type
"MayProvide.type i".
*)
HB.about Provide2.
(*
HB: Provide2.type is a structure (from "(stdin)", line 3)
HB: Provide2.type characterizing operations and axioms are:
HB: Provide2 is a factory for the following mixins:
- IsMayProvide
- IsProvide
- IsProvide2 (* new, not from inheritance *)
HB: Provide2 inherits from:
- MayProvide
- Provide
HB: Provide2 is inherited by:
*)
HB.about MayProvide.
(*
HB: MayProvide.type is a structure (from "(stdin)", line 19)
HB: MayProvide.type characterizing operations and axioms are:
- proj_p
HB: MayProvide is a factory for the following mixins:
- IsMayProvide (* new, not from inheritance *)
HB: MayProvide inherits from:
HB: MayProvide is inherited by:
- Provide
- CombinedProvider
- Provide2
*)
End t.Hence my questions :
- Is it that is not handled (yet?) ?
- Is the idea of having one carrier supporting multiple instances of a type against the HB philosophy ?
- Is it just something that I try to do wrongly ?
If I can help on any development or providing more information, just tell me !
Hello,
On my journey to replace typeclasses by HB in FreeSpec, I stumbled upon an issue with the interfaces.
In FreeSpec, one wants to be able to describe abstract interfaces that can be composed together. For this purpose they introduced a Polymorphic Composite Interface. The main typeclasses used for this are these ones :
The best translation I came across in HB is the following one :
Where
ix(the composite interface) becomes the carrier.But now, I need to design multiple providers. In FreeSpec, we find two examples :
And I can manage to make something that types for both in HB :
But, the problem arises when I want to use the first interface provided (
i) forix:Hence my questions :
If I can help on any development or providing more information, just tell me !