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 (*
  38  *  Everything in the rest of this section is just groundwork meant to
  39  *  build up to the definition of the ProgrammingLanguage class, which
  40  *  appears at the end of the section.  References to "the instance"
  41  *  mean instances of that class.  Think of this section as being one
  42  *  big Class { ... } definition, except that we declare most of the
  43  *  stuff outside the curly brackets in order to take advantage of
  44  *  Coq's section mechanism.
  45  *)
  46 Section Programming_Language.
  47
  48   Context {T    : Type}.               (* types of the language *)
  49
  50   Context (Judg : Type).
  51   Context (sequent : Tree ??T -> Tree ??T -> Judg).
  52      Notation "cs |= ss" := (sequent cs ss) : al_scope.
  53      (* Because of term irrelevance we need only store the *erased* (def
  54       * 4.4) trees; for this reason there is no Coq type directly
  55       * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
  56       * be used for productions $\Gamma$ and $\Sigma$ *)
  57
  58   (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
  59
  60   Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
  61
  62   Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
  63
  64   Open Scope pf_scope.
  65   Open Scope nd_scope.
  66   Open Scope al_scope.
  67
  68   (*
  69    *
  70    * Note that from this abstract interface, the terms (expressions)
  71    * in the proof are not accessible at all; they don't need to be --
  72    * so long as we have access to the equivalence relation upon
  73    * proof-conclusions.  Moreover, hiding the expressions actually
  74    * makes the encoding in CiC work out easier for two reasons:
  75    *
  76    *  1. Because the denotation function is provided a proof rather
  77    *     than a term, it is a total function (the denotation function is
  78    *     often undefined for ill-typed terms).
  79    *
  80    *  2. We can define arr_composition of proofs without having to know how
  81    *     to compose expressions.  The latter task is left up to the client
  82    *     function which extracts an expression from a completed proof.
  83    *
  84    * This also means that we don't need an explicit proof obligation for 4.1.2.
  85    *)
  86   Class ProgrammingLanguage :=
  87   { al_eqv                : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
  88   ; al_tsr                : TreeStructuralRules
  89   ; al_subst              : CutRule
  90   ; al_sequent_join       : SequentJoin
  91   }.
  92   Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
  93
  94   Section LanguageCategory.
  95
  96     Context (PL:ProgrammingLanguage).
  97
  98     (* category of judgments in a fixed type/coercion context *)
  99     Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule al_eqv.
 100
 101     Definition JudgmentsL          := Judgments_cartesian.
 102
 103     Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
 104       unfold hom; simpl.
 105       apply nd_rule.
 106       apply al_reflexive_seq.
 107       Defined.
 108
 109     Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
 110       unfold hom; simpl.
 111       apply al_subst.
 112       Defined.
 113
 114     Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
 115       refine
 116       {| eid   := identityProof
 117        ; ecomp := cutProof
 118       |}; intros.
 119       apply MonoidalCat_all_central.
 120       apply MonoidalCat_all_central.
 121       unfold identityProof; unfold cutProof; simpl.
 122       apply al_subst_left_identity.
 123       unfold identityProof; unfold cutProof; simpl.
 124       apply al_subst_right_identity.
 125       unfold identityProof; unfold cutProof; simpl.
 126       apply al_subst_associativity'.
 127       Defined.
 128
 129     Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
 130       (*
 131       eapply Build_EFunctor; intros.
 132       eapply MonoidalCat_all_central.
 133       unfold eqv.
 134       simpl.
 135       *)
 136       admit.
 137       Defined.
 138
 139     Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x ).
 140       admit.
 141       Defined.
 142
 143     Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
 144       refine
 145         {| bin_first  := Types_first
 146          ; bin_second := Types_second
 147          |}.
 148       Defined.
 149
 150     Definition TypesL_binoidal : BinoidalCat TypesL (@T_Branch _).
 151     admit.
 152     Defined.
 153
 154     Definition Types_PreMonoidal : PreMonoidalCat TypesL_binoidal [].
 155     admit.
 156     Defined.
 157
 158     Definition TypesEnrichedInJudgments : Enrichment.
 159       refine {| enr_c := TypesL |}.
 160       Defined.
 161
 162     Structure HasProductTypes :=
 163     {
 164     }.
 165
 166     (* need to prove that if we have cartesian tuples we have cartesian contexts *)
 167     Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
 168       admit.
 169       Defined.
 170
 171   End LanguageCategory.
 172
 173   Structure ProgrammingLanguageSMME :=
 174   { plsmme_pl   : ProgrammingLanguage
 175   ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments plsmme_pl)
 176   }.
 177   Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
 178   Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
 179
 180   Section ArrowInLanguage.
 181     Context  (Host:ProgrammingLanguageSMME).
 182     Context `(CC:CartesianCat (me_mon Host)).
 183     Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
 184     Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
 185       (* FIXME *)
 186       (*
 187       Definition ArrowInProgrammingLanguage :=
 188         @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
 189         *)
 190   End ArrowInLanguage.
 191
 192   Section GArrowInLanguage.
 193     Context (Guest:ProgrammingLanguageSMME).
 194     Context (Host :ProgrammingLanguageSMME).
 195     Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
 196
 197     (* FIXME
 198     Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
 199     *)
 200     Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
 201
 202     Context (GuestHost:TwoLevelLanguage).
 203
 204     Definition FlatObject (x:TypesL Host) :=
 205       forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
 206
 207     Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject.
 208
 209     Section Flattening.
 210
 211       Context  (F:Retraction (TypesL Host) FlatSubCategory).
 212       Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
 213       Lemma FlatteningIsNotDestructive :
 214         FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
 215         admit.
 216         Qed.
 217
 218     End Flattening.
 219
 220   End GArrowInLanguage.
 221
 222   Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 223   | NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
 224   | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
 225     TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
 226
 227   Definition OmegaLevelLanguage : Type :=
 228     { f : nat -> ProgrammingLanguageSMME
 229     & forall n, TwoLevelLanguage (f n) (f (S n)) }.
 230
 231   Close Scope temporary_scope3.
 232   Close Scope al_scope.
 233   Close Scope nd_scope.
 234   Close Scope pf_scope.
 235
 236 End Programming_Language.
 237
 238 Implicit Arguments ND [ Judgment ].