https://www.irif.fr/~gc/papers/icfp17.pdf

gradual.v

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Require Import Coq.Relations.Relations.
Require Import Coq.Compat.AdmitAxiom.

Import ListNotations.
Infix "<$>" := map (at level 65, left associativity).
Notation "k >>= f" := (flat_map f k) (at level 66, left associativity).

Definition allb {A} (f : A -> bool) (xs : list A) : bool :=
  fold_right andb true (map f xs).

Definition anyb {A} (f : A -> bool) (xs : list A) : bool :=
  fold_right orb false (map f xs).

Definition apList {A B} (fs : list (A -> B)) (xs : list A) : list B :=
  fs >>= fun f => f <$> xs.

Infix "<*>" := apList (at level 65, left associativity).

Definition null {A} (xs : list A) : bool :=
  match xs with
  | [] => true
  | _ => false
  end.

(* Subtyping decision procedure for base types. We parameterize over it here. *)
Class SubtypeDecidable (BaseType : Type) : Type :=
  { bsubDecide : list BaseType -> list BaseType -> bool
    (* `bsubDecide xs ys` is whether the intersection of xs lies within the union of ys *)
  ; BSub := fun t s => bsubDecide [t] [s] = true
  ; bsub_refl : reflexive _ BSub
  ; bsub_trans : transitive _ BSub
  }.

Section Types.

Context {BaseType : Type} `{SubtypeDecidable BaseType}.

Inductive SType : Type :=
  | SBottom : SType
  | STop : SType
  | SNot : SType -> SType
  | SArrow : SType -> SType -> SType
  | SBase : BaseType -> SType
  | SAnd : SType -> SType -> SType
  | SOr : SType -> SType -> SType.

Inductive GType : Type :=
  | GBottom : GType
  | GTop : GType
  | GAny : GType
  | GNot : SType -> GType
  | GArrow : GType -> GType -> GType
  | GBase : BaseType -> GType
  | GAnd : GType -> GType -> GType
  | GOr : GType -> GType -> GType.

Declare Scope stype_scope.
Delimit Scope stype_scope with stype.
Bind Scope stype_scope with SType.
Notation "𝟘" := SBottom : stype_scope.
Notation "𝟙" := STop : stype_scope.
Notation "¬ t" := (SNot t) (at level 75) : stype_scope.
Infix "→" := SArrow (at level 99, right associativity) : stype_scope.
Infix "∧" := SAnd (at level 85, right associativity) : stype_scope.
Infix "∨" := SOr (at level 85, right associativity) : stype_scope.
Notation "⋀ xs" := (fold_right SAnd STop xs) (at level 85) : stype_scope.
Notation "⋁ xs" := (fold_right SOr SBottom xs) (at level 85) : stype_scope.

Declare Scope gtype_scope.
Delimit Scope gtype_scope with gtype.
Bind Scope gtype_scope with GType.
Notation "𝟘" := GBottom : gtype_scope.
Notation "𝟙" := GTop : gtype_scope.
Notation "?" := GAny : gtype_scope.
Notation "¬ t" := (GNot t) (at level 75) : gtype_scope.
Infix "→" := GArrow (at level 99, right associativity) : gtype_scope.
Infix "∧" := GAnd (at level 85, right associativity) : gtype_scope.
Infix "∨" := GOr (at level 85, right associativity) : gtype_scope.
Notation "⋀ xs" := (fold_right GAnd GTop xs) (at level 85) : gtype_scope.
Notation "⋁ xs" := (fold_right GOr GBottom xs) (at level 85) : gtype_scope.

Reserved Infix "≤" (at level 70, no associativity).
Inductive Sub : SType -> SType -> Prop :=
  | sub_base : forall b c, BSub b c -> SBase b ≤ SBase c
  | sub_not_mono : forall t s, s ≤ t -> (¬t) ≤ (¬s)
  | sub_arrow_mono : forall t1 t2 s1 s2, s1 ≤ t1 -> t2 ≤ s2 -> (t1 → t2) ≤ (s1 → s2)
  | sub_bottom : forall t, 𝟘 ≤ t
  | sub_top : forall t, t ≤ 𝟙
  | sub_and_l : forall t1 t2, (t1 ∧ t2) ≤ t1
  | sub_and_r : forall t1 t2, (t1 ∧ t2) ≤ t2
  | sub_and : forall t s1 s2, t ≤ s1 -> t ≤ s2 -> t ≤ (s1 ∧ s2)
  | sub_or_l : forall t1 t2, t1 ≤ (t1 ∨ t2)
  | sub_or_r : forall t1 t2, t2 ≤ (t1 ∨ t2)
  | sub_or : forall t1 t2 s, t1 ≤ s -> t2 ≤ s -> (t1 ∨ t2) ≤ s
  | sub_trans : forall t s r, t ≤ s -> s ≤ r -> t ≤ r
where "t1 ≤ t2" := (Sub t1 t2).

Section SubDecide.

(* Either conjuncts or disjuncts depending on context, categorized by whether
it's a BaseType or an arrow, and by whether it's negated *)
Record Junct := mkJunct
  { bases : list BaseType
  ; arrows : list (SType * SType)
  ; notBases : list BaseType
  ; notArrows : list (SType * SType)
  }.

Definition unitJunct : Junct :=
  {| bases := []
  ; arrows := []
  ; notBases := []
  ; notArrows := []
  |}.

Definition mergeJuncts (j1 j2 : Junct) : Junct :=
  {| bases := bases j1 ++ bases j2
  ; arrows := arrows j1 ++ arrows j2
  ; notBases := notBases j1 ++ notBases j2
  ; notArrows := notArrows j1 ++ notArrows j2
  |}.

Definition invertJunct (j : Junct) : Junct :=
  {| bases := notBases j
  ; arrows := notArrows j
  ; notBases := bases j
  ; notArrows := notArrows j
  |}.

Fixpoint udnf (t : SType) : list Junct :=
  match t with
  | SBase b => [{| bases := [b]; arrows := []; notBases := []; notArrows := [] |}]
  | t1 → t2 => [{| bases := []; arrows := [(t1, t2)]; notBases := []; notArrows := [] |}]
  | 𝟘 => []
  | 𝟙 => [unitJunct]
  | ¬t => invertJunct <$> ucnf t
  | t1 ∨ t2 => udnf t1 ++ udnf t2
  | t1 ∧ t2 => mergeJuncts <$> udnf t1 <*> udnf t2
  end%stype
with ucnf (t : SType) : list Junct :=
  match t with
  | SBase b => [{| bases := [b]; arrows := []; notBases := []; notArrows := [] |}]
  | t1 → t2 => [{| bases := []; arrows := [(t1, t2)]; notBases := []; notArrows := [] |}]
  | 𝟘 => [unitJunct]
  | 𝟙 => []
  | ¬t => invertJunct <$> udnf t
  | t1 ∧ t2 => ucnf t1 ++ ucnf t2
  | t1 ∨ t2 => mergeJuncts <$> ucnf t1 <*> ucnf t2
  end%stype.

Definition junctDecide (jt js : Junct) : bool :=
  match bases jt ++ notBases js, arrows jt ++ notArrows js with
  | lbases, [] => bsubDecide lbases (bases js ++ notBases jt)
  | [], _ => match proof_admitted with
             (* How to decide subtyping of a bunch of arrows? Not sure. *)
             end
  | _, _ => match proof_admitted with
            (* How to decide whether base types intersect arrow types?
            This depends on the target language in some way. *)
            end
  end.

Definition subDecide (t s : SType) : bool :=
  allb id (junctDecide <$> udnf t <*> ucnf s).

End SubDecide.

Infix "≤!" := subDecide (at level 70, no associativity).

Notation "t ∈ S" := (S t) (at level 70, only parsing).

Fixpoint γ (τ : GType) : SType -> Prop :=
  match τ with
  | ? => fun _ => True
  | 𝟘 => eq 𝟘%stype
  | 𝟙 => eq 𝟙%stype
  | GBase b => eq (SBase b)
  | ¬t => eq (¬t)%stype
  | τ1 ∧ τ2 => fun t => match t with
                        | t1 ∧ t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2
                        | _ => False
                        end%stype
  | τ1 ∨ τ2 => fun t => match t with
                        | t1 ∨ t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2
                        | _ => False
                        end%stype
  | τ1 → τ2 => fun t => match t with
                        | t1 → t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2
                        | _ => False
                        end%stype
  end%gtype.

Definition lift2 (P : SType -> SType -> Prop) : GType -> GType -> Prop
  := fun τ1 τ2 => exists t1 t2, t1 ∈ γ τ1 /\ t2 ∈ γ τ2 /\ P t1 t2.

Fixpoint gradualMinimum (τ : GType) : SType :=
  match τ with
  | ? => 𝟘%stype
  | 𝟘 => 𝟘%stype
  | 𝟙 => 𝟙%stype
  | GBase b => SBase b
  | ¬t => (¬t)%stype
  | τ1 ∧ τ2 => (gradualMinimum τ1 ∧ gradualMinimum τ2)%stype
  | τ1 ∨ τ2 => (gradualMinimum τ1 ∨ gradualMinimum τ2)%stype
  | τ1 → τ2 => (gradualMaximum τ1 → gradualMinimum τ2)%stype
  end%gtype
with gradualMaximum (τ : GType) : SType :=
  match τ with
  | ? => 𝟙%stype
  | 𝟘 => 𝟘%stype
  | 𝟙 => 𝟙%stype
  | GBase b => SBase b
  | ¬t => (¬t)%stype
  | τ1 ∧ τ2 => (gradualMaximum τ1 ∧ gradualMaximum τ2)%stype
  | τ1 ∨ τ2 => (gradualMaximum τ1 ∨ gradualMaximum τ2)%stype
  | τ1 → τ2 => (gradualMinimum τ1 → gradualMaximum τ2)%stype
  end%gtype.

Notation "τ ⇓" := (gradualMinimum τ) (at level 65).
Notation "τ ⇑" := (gradualMaximum τ) (at level 65).

Infix "̃≤" := (lift2 Sub) (at level 70, no associativity).

Definition consSubDecide (σ τ : GType) : bool := σ⇓ ≤! τ⇑.

Infix "̃≤!" := consSubDecide (at level 70, no associativity).

Infix "̃≰" := (lift2 (fun s t => ~(s ≤ t))) (at level 70, no associativity).

Definition consNotSubDecide (σ τ : GType) : bool := negb (σ⇑ ≤! τ⇓).

Infix "̃≰!" := consNotSubDecide (at level 70, no associativity).

(* ??? The paper completely glances over that it treats SType as a subset of
GType in the definition of γA. γA+ restricted to SType is γApos' here. *)
Fixpoint stype2gtype (t : SType) : GType :=
  match t with
  | 𝟘 => 𝟘%gtype
  | 𝟙 => 𝟙%gtype
  | ¬t => (¬t)%gtype
  | t1 → t2 => (stype2gtype t1 → stype2gtype t2)%gtype
  | SBase b => GBase b
  | t1 ∧ t2 => (stype2gtype t1 ∧ stype2gtype t2)%gtype
  | t1 ∨ t2 => (stype2gtype t1 ∨ stype2gtype t2)%gtype
  end%stype.

Fixpoint γAneg (t : SType) : list (list (GType * GType)) :=
  match t with
  | t1 ∨ t2 => (fun T1 T2 => T1 ++ T2) <$> γAneg t1 <*> γAneg t2
  | t1 ∧ t2 => γAneg t1 ++ γAneg t2
  | _ → _ => [[]]
  | ¬t => γApos' t
  | 𝟘 => [[]]
  | 𝟙 => []
  | SBase _ => [[]]
  end%stype
with γApos' (t : SType) : list (list (GType * GType)) :=
  match t with
  | t1 ∨ t2 => γApos' t1 ++ γApos' t2
  | t1 ∧ t2 => (fun T1 T2 => T1 ++ T2) <$> γApos' t1 <*> γApos' t2
  | t1 → t2 => [[(stype2gtype t1, stype2gtype t2)]]
  | ¬t => γAneg t
  | 𝟘 => []
  | 𝟙 => [[]]
  | SBase _ => [[]]
  end%stype.

Fixpoint γApos (τ : GType) : list (list (GType * GType)) :=
  match τ with
  | τ1 ∨ τ2 => γApos τ1 ++ γApos τ2
  | τ1 ∧ τ2 => (fun T1 T2 => T1 ++ T2) <$> γApos τ1 <*> γApos τ2
  | τ1 → τ2 => [[(τ1, τ2)]]
  | ¬t => γAneg t
  | 𝟘 => []
  | 𝟙 => [[]]
  | GBase _ => [[]]
  | ? => [[(?, ?)]]
  end%gtype.

Definition dom (τ : GType) : SType :=
  ⋀ (fun S => ⋁ (fun '(ρ, _) => ρ⇑) <$> S)%stype <$> γApos τ.

Fixpoint assignments {X : Type} (xs : list X) : list (list (X * bool)) :=
  match xs with
  | [] => [[]]
  | (x :: xs) => cons <$> [(x, false); (x, true)] <*> assignments xs
  end.

Definition partitions {X : Type} (xs : list X) : list (list X * list X) :=
  (fun ys => (fst <$> filter snd ys, fst <$> filter (fun p => negb (snd p)) ys))
  <$> assignments xs.

Definition appResult (τ σ : GType) : GType := ⋁ (fun S =>
  ⋁ (fun '(Q, Qbar) => ⋀ snd <$> Qbar) <$> filter
    (fun '(Q, Qbar) => negb (null Qbar) && (σ ̃≰! ⋁ fst <$> Q)
      && negb ((σ⇑ ∧ ⋁ (fun '(ρ, _) => ρ⇑) <$> Qbar) ≤! 𝟘))
    (partitions S)
  )%gtype <$> γApos τ.

Infix "∘" := appResult (at level 90, no associativity).

Section SomeTheorems.

Local Theorem sub_and_mono t1 t2 s1 s2 : t1 ≤ s1 -> t2 ≤ s2 -> (t1 ∧ t2) ≤ (s1 ∧ s2).
Proof.
  intros p q.
  apply sub_and.
  - refine (sub_trans _ _ _ _ p).
    apply sub_and_l.
  - refine (sub_trans _ _ _ _ q).
    apply sub_and_r.
Qed.

Local Theorem sub_or_mono t1 t2 s1 s2 : t1 ≤ s1 -> t2 ≤ s2 -> (t1 ∨ t2) ≤ (s1 ∨ s2).
Proof.
  intros p q.
  apply sub_or.
  - refine (sub_trans _ _ _ p _).
    apply sub_or_l.
  - refine (sub_trans _ _ _ q _).
    apply sub_or_r.
Qed.

Local Theorem sub_refl t : t ≤ t.
Proof.
  pose proof sub_and_mono.
  pose proof sub_or_mono.
  pose proof bsub_refl.
  induction t; auto; now constructor.
Qed.

Local Theorem gradual_extrema_in_concretization τ : τ⇓ ∈ γ τ /\ τ⇑ ∈ γ τ.
Proof.
  induction τ as [ | | | | ? [] ? [] | | ? [] ? [] | ? [] ? [] ]; simpl; auto.
Qed.

Local Theorem gradual_extrema_bounds τ : forall t, t ∈ γ τ -> τ⇓ ≤ t /\ t ≤ τ⇑.
Proof.
  induction τ as [ | | | | ? IHl ? IHr | | ? IHl ? IHr | ? IHl ? IHr ]; simpl.
  - intros _ <-. repeat constructor.
  - intros _ <-. repeat constructor.
  - repeat constructor.
  - intros _ <-. repeat constructor.
    + apply sub_refl.
    + apply sub_refl.
  - intros [ | | | t1 t2 | | | ]; try contradiction.
    intros [].
    destruct (IHl t1); auto.
    destruct (IHr t2); auto.
    repeat constructor; auto.
  - intros _ <-. repeat constructor.
    + apply bsub_refl.
    + apply bsub_refl.
  - intros [ | | | | | t1 t2 | ]; try contradiction.
    intros [].
    destruct (IHl t1); auto.
    destruct (IHr t2); auto.
    split.
    + apply sub_and_mono; auto.
    + apply sub_and_mono; auto.
  - intros [ | | | | | | t1 t2 ]; try contradiction.
    intros [].
    destruct (IHl t1); auto.
    destruct (IHr t2); auto.
    split.
    + apply sub_or_mono; auto.
    + apply sub_or_mono; auto.
Qed.

Local Theorem cons_sub_reduction σ τ : σ ̃≤ τ <-> σ⇓ ≤ τ⇑.
Proof.
  unfold lift2. split.
  - intros [s [t [? []]]].
    apply (sub_trans _ s _).
    + now apply gradual_extrema_bounds.
    + apply (sub_trans _ t _).
      * assumption.
      * now apply gradual_extrema_bounds.
  - intros ?.
    exists (σ⇓), (τ⇑).
    split; try split.
    + apply gradual_extrema_in_concretization.
    + apply gradual_extrema_in_concretization.
    + assumption.
Qed.

Theorem sub_decide_agrees t s : t ≤ s <-> t ≤! s = true.
  (* Depends on the contents of junctDecide *)
Admitted.

Theorem cons_sub_decide_agrees σ τ : σ ̃≤ τ <-> σ ̃≤! τ = true.
Proof.
  transitivity (σ⇓ ≤ τ⇑).
  - apply cons_sub_reduction.
  - unfold consSubDecide.
    apply sub_decide_agrees.
Qed.

Theorem cons_not_sub_reduction σ τ : σ ̃≰ τ <-> ~(σ⇑ ≤ τ⇓).
Proof.
  unfold lift2. split.
  - intros [s [t [? [? p]]]] n.
    apply p.
    apply (sub_trans _ (σ⇑) _).
    + now apply gradual_extrema_bounds.
    + apply (sub_trans _ (τ⇓) _).
      * assumption.
      * now apply gradual_extrema_bounds.
  - intros n.
    exists (σ⇑), (τ⇓).
    split; try split.
    + apply gradual_extrema_in_concretization.
    + apply gradual_extrema_in_concretization.
    + assumption.
Qed.

Theorem cons_not_sub_decide_agrees σ τ : σ ̃≰ τ <-> σ ̃≰! τ = true.
Proof.
  transitivity (~(σ⇑ ≤ τ⇓)).
  - apply cons_not_sub_reduction.
  - unfold consNotSubDecide.
    transitivity (σ⇑ ≤! τ⇓ <> true).
    + apply not_iff_compat.
      apply sub_decide_agrees.
    + transitivity (σ⇑ ≤! τ⇓ = false).
      * apply not_true_iff_false.
      * symmetry. apply negb_true_iff.
Qed.

End SomeTheorems.

Section SomeContradictions.

Inductive PartialEvalResult : Type :=
  | EvBottom
  | EvUnknown
  | EvTop.

Local Fixpoint partialEval (t : SType) : PartialEvalResult :=
  match t with
  | 𝟘 => EvBottom
  | 𝟙 => EvTop
  | SBase _ => EvUnknown
  | _ → _ => EvUnknown
  | ¬t => match partialEval t with
          | EvBottom => EvTop
          | EvUnknown => EvUnknown
          | EvTop => EvBottom
          end
  | t1 ∧ t2 => match partialEval t1, partialEval t2 with
               | EvBottom, _ => EvBottom
               | _, EvBottom => EvBottom
               | EvUnknown, _ => EvUnknown
               | _, EvUnknown => EvUnknown
               | _, _ => EvTop
               end
  | t1 ∨ t2 => match partialEval t1, partialEval t2 with
               | EvTop, _ => EvTop
               | _, EvTop => EvTop
               | EvUnknown, _ => EvUnknown
               | _, EvUnknown => EvUnknown
               | _, _ => EvBottom
               end
  end%stype.

Local Theorem partial_eval_mono t s :
  t ≤ s -> match partialEval t, partialEval s with
           | EvBottom, _ => True
           | _, EvTop => True
           | EvUnknown, EvBottom => False
           | EvUnknown, _ => True
           | EvTop, _ => False
           end.
Proof.
  intros p.
  induction p.
  all: repeat first [ progress (simpl; auto) | destruct (partialEval _) ].
Qed.

Local Theorem top_nle_bottom : ~(𝟙 ≤ 𝟘).
Proof.
  intros n. apply (partial_eval_mono _ _ n).
Qed.

Theorem cons_sub_nontrans : ~(forall g h k, g ̃≤ h -> h ̃≤ k -> g ̃≤ k).
Proof.
  intros n.
  enough (p : 𝟙 ̃≤ 𝟘).
  - apply top_nle_bottom.
    unfold lift2 in p. simpl in p.
    now destruct p as [? [? [-> [->]]]].
  - apply (n _ ?%gtype _).
    + unfold lift2. simpl.
      exists 𝟙%stype, 𝟙%stype.
      split; auto. split; auto.
      constructor.
    + unfold lift2. simpl.
      exists 𝟘%stype, 𝟘%stype.
      split; auto. split; auto.
      constructor.
Qed.

End SomeContradictions.

End Types.

(* Have to redeclare all notations now that the section is closed *)
Declare Scope stype_scope.
Delimit Scope stype_scope with stype.
Bind Scope stype_scope with SType.
Notation "𝟘" := SBottom : stype_scope.
Notation "𝟙" := STop : stype_scope.
Notation "¬ t" := (SNot t) (at level 75) : stype_scope.
Infix "→" := SArrow (at level 99, right associativity) : stype_scope.
Infix "∧" := SAnd (at level 85, right associativity) : stype_scope.
Infix "∨" := SOr (at level 85, right associativity) : stype_scope.
Notation "⋀ xs" := (fold_right SAnd STop xs) (at level 85) : stype_scope.
Notation "⋁ xs" := (fold_right SOr SBottom xs) (at level 85) : stype_scope.
Declare Scope gtype_scope.
Delimit Scope gtype_scope with gtype.
Bind Scope gtype_scope with GType.
Notation "𝟘" := GBottom : gtype_scope.
Notation "𝟙" := GTop : gtype_scope.
Notation "?" := GAny : gtype_scope.
Notation "¬ t" := (GNot t) (at level 75) : gtype_scope.
Infix "→" := GArrow (at level 99, right associativity) : gtype_scope.
Infix "∧" := GAnd (at level 85, right associativity) : gtype_scope.
Infix "∨" := GOr (at level 85, right associativity) : gtype_scope.
Notation "⋀ xs" := (fold_right GAnd GTop xs) (at level 85) : gtype_scope.
Notation "⋁ xs" := (fold_right GOr GBottom xs) (at level 85) : gtype_scope.
Infix "≤" := Sub (at level 70, no associativity).
Infix "≤!" := subDecide (at level 70, no associativity).
Notation "τ ⇓" := (gradualMinimum τ) (at level 65).
Notation "τ ⇑" := (gradualMaximum τ) (at level 65).
Infix "̃≤" := (lift2 Sub) (at level 70, no associativity).
Infix "̃≤!" := consSubDecide (at level 70, no associativity).
Infix "̃≰" := (lift2 (fun s t => ~(s ≤ t))) (at level 70, no associativity).
Infix "̃≰!" := consNotSubDecide (at level 70, no associativity).
Infix "∘" := appResult (at level 90, no associativity).

Section Example.

Inductive BaseType :=
  | object
  | int
  | str
  | bytes
  | float.
Scheme Equality for BaseType.

Definition SBase' := @SBase BaseType.
Coercion SBase' : BaseType >-> SType.
Definition GBase' := @GBase BaseType.
Coercion GBase' : BaseType >-> GType.

Definition decideSubclass (b c : BaseType) : bool :=
  BaseType_beq b c || match b, c with
                      | _, object => true
                      | _, _ => false
                      end.

Program Instance subtype_decidable_basetype : SubtypeDecidable BaseType :=
  {| bsubDecide := fun conjs disjs =>
    anyb id (decideSubclass <$> conjs <*> disjs)
    || anyb (fun c => match c with object => true | _ => false end) disjs
  |}.
Next Obligation.
  unfold reflexive.
  intros []; simpl; auto.
Qed.
Next Obligation.
  unfold transitive, anyb.
  intros b c d.
  destruct b, d; simpl; auto; destruct c; simpl; auto.
Qed.

Eval cbn in (int → float) ∧ (str → bytes) ∘ int.
(*
     = (((float ∧ bytes ∧ 𝟙) ∨ (float ∧ 𝟙) ∨ 𝟘) ∨ 𝟘)%gtype
     : GType
*)

End Example.