D.Dot.examples.syn.list

Encoding covariant lists.

Here, the main lemma is listTyp, saying that hlistModV hx0 (the code shown in the paper) has type hlistModT hx0 in a context offering a boolean implementation. Subsequent examples demonstrate how to link lists with the boolean implementation we provide, and how to use lists.

From D Require Import tactics.
From D.Dot Require Import syn unstampedness_binding.
From D.Dot Require Import old_unstamped_typing old_unstamped_typing_derived_rules.
From D.Dot.examples Require Import ex_utils scala_lib hoas.

Import DBNotation hoasNotation.

Implicit Types (L T U : hty) (Γ : list ty).

Definition htrueTm (bool : hvl) := htskip (bool @: "true").
Definition hfalseTm (bool : hvl) := htskip (bool @: "false").

Lemma trueTyp Γ Γ'' : Γ'' ++ boolImplT :: Γ u⊢ₜ
  htrueTm (hx (length Γ'')) : hx (length Γ'') @; "Boolean".
Proof.
  have ? : length Γ'' < length (Γ'' ++ boolImplT :: Γ) by rewrite app_length /=; lia.
  apply (iT_ISub (i := 1) (T1 := ▶: hx (length Γ'') @; "Boolean"));
    rewrite /= plusnO; tcrush.
    eapply iT_ISub_nocoerce.
  - eapply iT_Mu_E'; first eapply iT_Var'; try by [rewrite lookup_app_r ?Nat.sub_diag|]; stcrush.
  - ltcrush.
Qed.

Lemma falseTyp Γ Γ'' : Γ'' ++ boolImplT :: Γ u⊢ₜ
  hfalseTm (hx (length Γ'')) : hx (length Γ'') @; "Boolean".
Proof.
  have ? : length Γ'' < length (Γ'' ++ boolImplT :: Γ) by rewrite app_length /=; lia.
  apply (iT_ISub (i := 1) (T1 := ▶: hx (length Γ'') @; "Boolean"));
    rewrite /= plusnO; tcrush.
  eapply iT_ISub_nocoerce.
  - eapply iT_Mu_E'; first eapply iT_Var'; try by [rewrite lookup_app_r ?Nat.sub_diag|]; stcrush.
  - ltcrush.
Qed.

Interface of the list module.


(* sci stands for scala.collection.immutable, following the example in WadlerFest DOT. *)
Definition hlistTGen (bool sci : hpath) L U : hty := μ: self, {@
  type "A" >: L <: U;
  val "isEmpty" : →: bool @; "Boolean";
  val "head" : →: self @; "A";
  val "tail" : →: hTAnd (sci @; "List") (type "A" >: <: self @; "A" )
}.

The list type itself.

Definition hlistT bool sci := hlistTGen bool sci .

This ▶: Later is needed because
  • hnilT types a value member "nil" (which can't use skips), and
  • this value member has abstract type sci @; "List", and
  • when we initialize "nil", sci has type ▶:(type "List" >: ... <: ..., so we can't deduce anything about sci@;"List", only something about ▶:(sci@; "List").
Definition hnilT sci := hTAnd (▶: sci @; "List") (typeEq "A" ).

∀(x: {A})∀(hd: x.A)∀(tl: sci.List∧{A <: x.A})sci.List∧{A <: x.A}
Definition hconsT sci : hty :=
  ∀: x : (tparam "T"),
    x @; "T" →:
    (hTAnd (sci @; "List") (type "A" >: <: x @; "T")) →:
    hTAnd (sci @; "List") (type "A" >: <: x @; "T").

mod stands for module.
Definition hlistModTBody bool sci : hty := {@
  type "List" >: <: hlistT bool sci;
  val "nil" : hnilT sci;
  val "cons" : hconsT sci
}.
Definition hlistModT bool : hty := μ: sci, hlistModTBody bool sci.

Implementation of the list module.

Definition hnilV bool : hvl := ν: self, {@
  type "A" = ;
  val "isEmpty" = λ: _, htrueTm bool;
  val "head" = λ: _, hloopTm;
  val "tail" = λ: _, hloopTm
}.

(*
  λ(x: {A})λ(hd: x.A)λ(tl: sci.List∧{A <: x.A}) let result = ν(self) {
    A = x.A; isEmpty = bool.false; head = hd; tail = tl } in result *)

Program Definition hconsV bool : hvl :=
  λ: x hd tl, ν: self, {@
    type "A" = x @; "T";
    val "isEmpty" = λ: _, hfalseTm bool;
    val "head" = λ: _, hd;
    val "tail" = λ: _, tl
  }.

Definition hlistModV (bool : hvl) : hvl := ν: self, {@
  type "List" = hlistT bool self;
  val "nil" = hnilV bool;
  val "cons" = hconsV bool
}.

Auxiliary types, needed in derivations of typing judgments.

Definition hconsTResConcr bool sci U := hlistTGen bool sci U U.

Definition hconsTConcr (bool sci : hpath) : hty :=
  ∀: x: tparam "T",
    x @; "T" →:
      hTAnd (sci @; "List") (type "A" >: <: x @; "T") →:
      (hconsTResConcr bool sci (x @; "T")).

Definition hlistModTConcrBody bool sci : hty := {@
  typeEq "List" $ hlistT bool sci;
  val "nil" : hnilT sci;
  val "cons" : hconsTConcr bool sci
}.

Definition hlistModTConcr bool : hty := μ: sci, hlistModTConcrBody bool sci.

Lemmas for proof that hlistModV has type hlistModT.

Example nilTyp Γ : (▶: hlistModTConcrBody hx1 hx0)%ty :: boolImplT :: Γ u⊢ₜ
  hnilV hx1 : hnilT hx0.
Proof.
  apply (iT_ISub_nocoerce $ hlistTGen hx1 hx0 ).
  - evar (T : ty).
    set L := (▶: hlistModTConcrBody hx1 hx0)%ty.
    have := !! trueTyp Γ [; T; L].
    have := !! loopTyp ( :: T :: L :: boolImplT :: Γ).
    rewrite {}/T/= ⇒ Ht Hl.
    tcrush; apply (iT_ISub_nocoerce ); tcrush.
  - tcrush; last mltcrush.
    ettrans; first eapply iSub_Add_Later; stcrush.
    asideLaters.
    eapply iSub_Sel'; tcrush. varsub.
    asideLaters.
    ltcrush.
Qed.

Example consTyp Γ : (▶: hlistModTConcrBody hx1 hx0)%ty :: boolImplT :: Γ u⊢ₜ
  hconsV hx1 : hconsTConcr hx1 hx0.
Proof.
  epose proof falseTyp Γ [_; _; _; _; _; _] as Ht; cbn in Ht.
  tcrush; clear Ht.
Typecheck returned head:
  by varsub; eapply (iSub_Sel' (hx4 @; "T")); tcrush; varsub; ltcrush.
Typecheck returned tail. Recall cons starts with
λ: x hd tl, ν: self, ....
Hence, x.A is the type argument to cons, and tl has type List & {A = x.A}.
Since cons constructs a new object, hconsTConcr types it against a *copy* of the list body, whose element type self.A is a copy of x.A. Hence, we must show that tl has type List & {A = self.A}. It suffices to show that List & {A = x.A} <: List & {A = self.A}:
  varsub.
It suffices to show that x.A <: self.A:
  tcrush; lNext.

We do it using iSub_Sel' on self.A, and looking up A on self's type.
  eapply iSub_Sel', (path_tp_delay (i := 0)); wtcrush. varsub; ltcrush.
Qed.

Ltac norm := cbv; hideCtx.
Lemma consTSub Γ : (hlistModTConcrBody hx1 hx0 : ty) :: boolImplT :: Γ u⊢ₜ
  hconsTConcr hx1 hx0, 0 <: hconsT hx0, 0.
Proof.
  tcrush; rewrite !iterate_S !iterate_0; hideCtx; last mltcrush.
  eapply iSub_Sel', (path_tp_delay (i := 0)); wtcrush; varsub; by ltcrush.
Qed.

Example listTypConcr Γ : boolImplT :: Γ u⊢ₜ hlistModV hx0 : hlistModTConcr hx0.
Proof.
  have Hn := nilTyp Γ.
  (* Without the call to iD_Val, Coq would (smartly) default to iD_All *)
  have := consTyp Γ ⇒ /(iD_Val "cons") Hc /=.
  tcrush.
Qed.

Proof that hlistModV has type hlistModT.

Example listTyp Γ : boolImplT :: Γ u⊢ₜ hlistModV hx0 : hlistModT hx0.
Proof.
  have Hv := listTypConcr Γ.
  have Hsub := consTSub Γ.
  eapply iT_ISub_nocoerce; first exact Hv; ltcrush.
Qed.

Link lists with booleans.


(*
Naive attempt; this fails, because the return type mentions a local variable.
Inferring return types that avoid mentioning local variables is called the
avoidance problem, a term going back to the ML module literature. *)

(*
Definition hclListV :=
  hlett: bool := pureS boolImplV in:
  hlistModV bool.

Example clListTyp Γ : Γ u⊢ₜ hclListV : hlistModT hx0.
  eapply iT_Let. apply boolImplTyp.
  Fail rewrite (_ : shift (hclose (hlistModT hx0)) = hlistModT hx0); last done.
  Fail apply listTyp.
Abort. *)


Definition hclListV' (hbody : hvl hvl htm) :=
  hlett: bool := pureS boolImplV in:
  hlett: list := hlistModV bool in:
    hbody bool list.

Have clListV' take an open de BruijN tm.
Definition clListV' (body : tm) := hclListV' (λ _ _, pureS body).

Example clListTyp' Γ (T : ty) body
  (Ht : shift (hlistModT hx0 : ty) :: boolImplT :: Γ u⊢ₜ body : shift (shift T)) :
  Γ u⊢ₜ clListV' body : T.
Proof.
  eapply iT_Let; first apply boolImplTyp.
  eapply iT_Let; first apply listTyp.
  all: tcrush.
Qed.

Example clListTypNat Γ :
  Γ u⊢ₜ clListV' (hvint 1) : 𝐙.
Proof. apply clListTyp'. tcrush. Qed.

This typing lemma generalizes over an arbitrary body hbody, taken as open HOAS terms. To close it, we must turn it into a concrete term exactly as hclListV' would, which exposes implementation details I'd rather not.
Example clListTyp'2 Γ (T : ty) hbody
  (Ht : (hlistModT hx1 : ty) :: boolImplT :: Γ u⊢ₜ hbody (hxm 1) (hxm 2) 2 : shift (shift T)) :
  Γ u⊢ₜ hclListV' hbody : T.
Proof.
  eapply iT_Let; first apply boolImplTyp.
  eapply iT_Let; first apply listTyp.
  all: tcrush.
Qed.

Example clListTypNat2 Γ :
  Γ u⊢ₜ hclListV' (λ _ _, hvint 1) : 𝐙.
Proof. apply clListTyp'2. tcrush. Qed.

Link lists with booleans and with a client using the list API.

Definition hheadCons (list : hvl) :=
  htskip $ htskip (
    (hAnfBind $ htskip
      (htyApp (list @: "cons") "T" 𝐙
        $: 0
        $: htskip (list @: "nil")))
    @: "head" $: 0).
(* Invoking a method from an abstract type (here, list @; "List" needs a skip. *)

Program Example hheadConsTyp Γ :
  hlistModT hx1 :: boolImplT :: Γ u⊢ₜ hheadCons (hxm 2) 2 : 𝐙.
Proof.
  hideCtx; set Γ' := Γ0.
  have HL : Γ' u⊢ₜ x0 : hlistModTBody hx1 hx0 by apply: iT_Mu_E'; first var; stcrush.

  (* The result of "head" has one more later than the list. *)
  eapply (iT_ISub (i := 2) (T1 := ▶: ▶: 𝐙)).
  asideLaters. tcrush.
  eapply (iT_All_E (T1 := )); last (eapply iT_ISub_nocoerce); tcrush.
  have Hnil : Γ' u⊢ₜ (hxm 2 @: "nil") 2 : hnilT hx0
    by tcrush; eapply iT_ISub_nocoerce; ltcrush.
  have Hsnil : Γ' u⊢ₜ htskip (hxm 2 @: "nil") 2
    : hTAnd (hx0 @; "List") (typeEq "A" ). {
    eapply (iT_ISub (i := 1)), Hnil.
    by tcrush; [lThis | lNext; apply iSub_AddI; tcrush].
  }
  have Hcons : Γ' u⊢ₜ (hxm 2 @: "cons") 2 : hconsT hx0. {
    tcrush.
    eapply iT_ISub_nocoerce; by [| ltcrush].
  }

  (* Here we produce a list of later nats, since we produce a list of p.A where p is the
  "type" argument and p : { A <: Nat} so p.A <: ▶: Nat. *)

  set U := (type "A" >: <: ▶: 𝐙)%HS.
  set V := (hTAnd (hlistT hx1 hx0) U).
  apply AnfBind_typed with (T := V); stcrush; first last.
  {
    eapply iT_ISub_nocoerce; first
      eapply (iT_Mu_E' (T1 := (val "head" : →: hx0 @; "A")%HS));
      [ | done | tcrush ..].
      - varsub; asideLaters; lThis; ltcrush.
      - by apply (iSel_SubL (L := )), (path_tp_delay (i := 0)); wtcrush; varsub; ltcrush.
  }
  eapply (iT_ISub (i := 1) (T1 := hTAnd (hx0 @; "List") U)).
  (******)
  (* We seem stuck here. The problem is that *we* wrote
  x.List & { A <: Nat }, and that's <: (▶: ListBody) & { A <: Nat }, and we have no
  rule to deal with that Later *in the syntax* *yet*.
  But we know that (▶: ListBody) & { A <: Nat } <: (▶: ListBody) & ▶: { A <: Nat }.
  Next, Distr_TLater_And gets us to
  (▶: (ListBody & { A <: Nat }), and we're back in business!
   *)

  {
    ettrans; last apply iLater_Sub; stcrush.
    ettrans; [|apply: iAnd_Later_Sub_Distr; stcrush].
    tcrush; [lThis | lNext].
    eapply iSel_Sub; tcrush.
    eapply iT_ISub_nocoerce; ltcrush.
  }

  eapply iT_All_E, Hsnil.
  eapply (iT_All_E (T1 := 𝐙)); last tcrush.
  (* Perform avoidance on the type application. *)
  eapply tyApp_typed with (T := 𝐙%HS); first done; intros; ltcrush; cbv -[Γ'].
  by eapply iSub_Sel', (path_tp_delay (i := 0)); try (typconstructor; var); wtcrush.
  by lNext.
  lNext; by eapply iSel_Sub, (path_tp_delay (i := 0)); try (typconstructor; var); wtcrush.
Qed.

Example clListTypNat3 Γ :
  Γ u⊢ₜ hclListV' (λ bool, hheadCons) : 𝐙.
Proof. apply clListTyp'2, hheadConsTyp. Qed.