src/ProgrammingLanguage.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguage                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*   Basic assumptions about programming languages.                                                                              *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import InitialTerminal_ch2_2.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import FunctorCategories_ch7_7.
  26
  27 Require Import NaturalDeduction.
  28 Require Import NaturalDeductionCategory.
  29
  30 Require Import FreydCategories.
  31
  32 Require Import Reification.
  33 Require Import GeneralizedArrow.
  34 Require Import GeneralizedArrowFromReification.
  35 Require Import ReificationFromGeneralizedArrow.
  36
  37 Section Programming_Language.
  38
  39   Context {T    : Type}.               (* types of the language *)
  40
  41   Context (Judg : Type).
  42   Context (sequent : Tree ??T -> Tree ??T -> Judg).
  43      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
  44
  45   Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
  46
  47   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
  48
  49   Open Scope pf_scope.
  50   Open Scope nd_scope.
  51   Open Scope pl_scope.
  52
  53   Class ProgrammingLanguage :=
  54   { pl_eqv                :  @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
  55   ; pl_tsr                :> @TreeStructuralRules Judg Rule T sequent
  56   ; pl_sc                 :> @SequentCalculus Judg Rule _ sequent
  57   ; pl_subst              :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
  58   ; pl_sequent_join       :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
  59   }.
  60   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
  61
  62   Section LanguageCategory.
  63
  64     Context (PL:ProgrammingLanguage).
  65
  66     (* category of judgments in a fixed type/coercion context *)
  67     Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
  68
  69     Definition JudgmentsL          := Judgments_cartesian.
  70
  71     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
  72       unfold hom; simpl.
  73       apply nd_seq_reflexive.
  74       Defined.
  75
  76     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
  77       unfold hom; simpl.
  78       apply pl_subst.
  79       Defined.
  80
  81     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
  82       refine
  83       {| eid   := identityProof
  84        ; ecomp := cutProof
  85       |}; intros.
  86       apply MonoidalCat_all_central.
  87       apply MonoidalCat_all_central.
  88       unfold identityProof; unfold cutProof; simpl.
  89       apply nd_cut_left_identity.
  90       unfold identityProof; unfold cutProof; simpl.
  91       apply nd_cut_right_identity.
  92       unfold identityProof; unfold cutProof; simpl.
  93       symmetry.
  94       apply nd_cut_associativity.
  95       Defined.
  96
  97     Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
  98       refine {| efunc := fun x y => (nd_rule (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)) |}.
  99       intros; apply MonoidalCat_all_central.
 100       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 101       apply se_reflexive_right.
 102       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 103       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_right _ c#] _ _ (nd_id1 (b|=c0))
 104                   _ (nd_id1 (a,,c |= b,,c))  _ [#se_expand_right _ c#]).
 105       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
 106       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 107       apply se_cut_right.
 108       Defined.
 109
 110     Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
 111       eapply Build_EFunctor.
 112       instantiate (1:=(fun x y => (nd_rule (@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
 113       intros; apply MonoidalCat_all_central.
 114       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 115       apply se_reflexive_left.
 116       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 117       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_left _ c#] _ _ (nd_id1 (b|=c0))
 118                   _ (nd_id1 (c,,a |= c,,b))  _ [#se_expand_left _ c#]).
 119       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
 120       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 121       apply se_cut_left.
 122       Defined.
 123
 124     Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
 125       refine
 126         {| bin_first  := Types_first
 127          ; bin_second := Types_second
 128          |}.
 129       Defined.
 130
 131     Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
 132       admit.
 133       Defined.
 134
 135     Definition TypesEnrichedInJudgments : Enrichment.
 136       refine {| enr_c := TypesL |}.
 137       Defined.
 138
 139     Structure HasProductTypes :=
 140     {
 141     }.
 142
 143     (* need to prove that if we have cartesian tuples we have cartesian contexts *)
 144     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
 145       admit.
 146       Defined.
 147
 148   End LanguageCategory.
 149 End Programming_Language.
 150
 151 Structure ProgrammingLanguageSMME :=
 152 { plsmme_t       : Type
 153 ; plsmme_judg    : Type
 154 ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
 155 ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
 156 ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
 157 ; plsmme_smme    : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
 158 }.
 159 Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
 160 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
 161
 162 Section ArrowInLanguage.
 163   Context  (Host:ProgrammingLanguageSMME).
 164   Context `(CC:CartesianCat (me_mon Host)).
 165   Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
 166   Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
 167     (* FIXME *)
 168     (*
 169     Definition ArrowInProgrammingLanguage :=
 170       @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
 171       *)
 172 End ArrowInLanguage.
 173
 174 Section GArrowInLanguage.
 175   Context (Guest:ProgrammingLanguageSMME).
 176   Context (Host :ProgrammingLanguageSMME).
 177   Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
 178
 179   (* FIXME
 180   Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
 181   *)
 182   Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
 183
 184   Context (GuestHost:TwoLevelLanguage).
 185
 186   Definition FlatObject (x:TypesL _ _ Host) :=
 187     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 188
 189   Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
 190
 191   Section Flattening.
 192
 193     Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
 194     Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
 195     Lemma FlatteningIsNotDestructive :
 196       FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
 197       admit.
 198       Qed.
 199
 200   End Flattening.
 201
 202 End GArrowInLanguage.
 203
 204 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 205 | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 206 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
 207                           TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 208
 209 Definition OmegaLevelLanguage : Type :=
 210   { f : nat -> ProgrammingLanguageSMME
 211   & forall n, TwoLevelLanguage (f n) (f (S n)) }.
 212
 213 Implicit Arguments ND [ Judgment ].