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 GeneralizedArrows.
  34 Require Import GeneralizedArrowFromReification.
  35
  36 Section Programming_Language.
  37
  38   Context {T    : Type}.               (* types of the language *)
  39
  40   Context (Judg : Type).
  41   Context (sequent : Tree ??T -> Tree ??T -> Judg).
  42      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
  43
  44   Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
  45
  46   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
  47
  48   Open Scope pf_scope.
  49   Open Scope nd_scope.
  50   Open Scope pl_scope.
  51
  52   Class ProgrammingLanguage :=
  53   { pl_eqv                :  @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
  54   ; pl_tsr                :> @TreeStructuralRules Judg Rule T sequent
  55   ; pl_sc                 :> @SequentCalculus Judg Rule _ sequent
  56   ; pl_subst              :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
  57   ; pl_sequent_join       :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
  58   }.
  59   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
  60
  61   Section LanguageCategory.
  62
  63     Context (PL:ProgrammingLanguage).
  64
  65     (* category of judgments in a fixed type/coercion context *)
  66     Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
  67
  68     Definition JudgmentsL          := Judgments_cartesian.
  69
  70     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
  71       unfold hom; simpl.
  72       apply nd_seq_reflexive.
  73       Defined.
  74
  75     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
  76       unfold hom; simpl.
  77       apply pl_subst.
  78       Defined.
  79
  80     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
  81       refine
  82       {| eid   := identityProof
  83        ; ecomp := cutProof
  84       |}; intros.
  85       apply MonoidalCat_all_central.
  86       apply MonoidalCat_all_central.
  87       unfold identityProof; unfold cutProof; simpl.
  88       apply nd_cut_left_identity.
  89       unfold identityProof; unfold cutProof; simpl.
  90       apply nd_cut_right_identity.
  91       unfold identityProof; unfold cutProof; simpl.
  92       symmetry.
  93       apply nd_cut_associativity.
  94       Defined.
  95
  96     Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
  97       refine {| efunc := fun x y => (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y) |}.
  98       intros; apply MonoidalCat_all_central.
  99       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 100       apply se_reflexive_right.
 101       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 102       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (se_expand_right _ c) _ _ (nd_id1 (b|=c0))
 103                   _ (nd_id1 (a,,c |= b,,c))  _ (se_expand_right _ c)).
 104       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
 105       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 106       apply se_cut_right.
 107       Defined.
 108
 109     Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
 110       eapply Build_EFunctor.
 111       instantiate (1:=(fun x y => ((@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
 112       intros; apply MonoidalCat_all_central.
 113       intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
 114       apply se_reflexive_left.
 115       intros. unfold ehom. unfold comp. simpl. unfold cutProof.
 116       rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (se_expand_left _ c) _ _ (nd_id1 (b|=c0))
 117                   _ (nd_id1 (c,,a |= c,,b))  _ (se_expand_left _ c)).
 118       setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
 119       setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
 120       apply se_cut_left.
 121       Defined.
 122
 123     Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
 124       refine
 125         {| bin_first  := Types_first
 126          ; bin_second := Types_second
 127          |}.
 128       Defined.
 129
 130     Definition Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a.
 131       admit.
 132       Defined.
 133
 134     Definition Types_cancelr   : Types_first [] <~~~> functor_id _.
 135       admit.
 136       Defined.
 137
 138     Definition Types_cancell   : Types_second [] <~~~> functor_id _.
 139       admit.
 140       Defined.
 141
 142     Definition Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a.
 143       admit.
 144       Defined.
 145
 146     Definition Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b.
 147       admit.
 148       Defined.
 149
 150     Instance Types_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
 151         { pmon_assoc    := Types_assoc
 152         ; pmon_cancell  := Types_cancell
 153         ; pmon_cancelr  := Types_cancelr
 154         ; pmon_assoc_rr := Types_assoc_rr
 155         ; pmon_assoc_ll := Types_assoc_ll
 156         }.
 157         admit. (* pentagon law *)
 158         admit. (* triangle law *)
 159         admit. (* assoc_rr/assoc coherence *)
 160         admit. (* assoc_ll/assoc coherence *)
 161         Defined.
 162
 163     Definition TypesEnrichedInJudgments : Enrichment.
 164       refine {| enr_c := TypesL |}.
 165       Defined.
 166
 167     Structure HasProductTypes :=
 168     {
 169     }.
 170
 171     (* need to prove that if we have cartesian tuples we have cartesian contexts *)
 172     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
 173       admit.
 174       Defined.
 175
 176   End LanguageCategory.
 177 End Programming_Language.
 178
 179 Structure ProgrammingLanguageSMME :=
 180 { plsmme_t       : Type
 181 ; plsmme_judg    : Type
 182 ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
 183 ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
 184 ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
 185 ; plsmme_smme    : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
 186 }.
 187 Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
 188 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
 189
 190 Section ArrowInLanguage.
 191   Context  (Host:ProgrammingLanguageSMME).
 192   Context `(CC:CartesianCat (me_mon Host)).
 193   Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
 194   Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
 195     (* FIXME *)
 196     (*
 197     Definition ArrowInProgrammingLanguage :=
 198       @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
 199       *)
 200 End ArrowInLanguage.
 201
 202 Section GArrowInLanguage.
 203   Context (Guest:ProgrammingLanguageSMME).
 204   Context (Host :ProgrammingLanguageSMME).
 205   Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
 206
 207   (* FIXME
 208   Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
 209   *)
 210   Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
 211
 212   Context (GuestHost:TwoLevelLanguage).
 213
 214   Definition FlatObject (x:TypesL _ _ Host) :=
 215     forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 216
 217   Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
 218
 219   Section Flattening.
 220
 221     Context  (F:Retraction (TypesL _ _ Host) FlatSubCategory).
 222     Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
 223     Lemma FlatteningIsNotDestructive :
 224       FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
 225       admit.
 226       Qed.
 227
 228   End Flattening.
 229
 230 End GArrowInLanguage.
 231
 232 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 233 | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 234 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
 235                           TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 236
 237 Definition OmegaLevelLanguage : Type :=
 238   { f : nat -> ProgrammingLanguageSMME
 239   & forall n, TwoLevelLanguage (f n) (f (S n)) }.
 240
 241 Implicit Arguments ND [ Judgment ].