1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguage *)
4 (* Basic assumptions about programming languages. *)
6 (*********************************************************************************************************************************)
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.
27 Require Import NaturalDeduction.
28 Require Import NaturalDeductionCategory.
30 Require Import FreydCategories.
32 Require Import Reification.
33 Require Import GeneralizedArrow.
34 Require Import GeneralizedArrowFromReification.
35 Require Import ReificationFromGeneralizedArrow.
37 Section Programming_Language.
39 Context {T : Type}. (* types of the language *)
41 Context (Judg : Type).
42 Context (sequent : Tree ??T -> Tree ??T -> Judg).
43 Notation "cs |= ss" := (sequent cs ss) : pl_scope.
45 Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
47 Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
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
60 Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
62 Section LanguageCategory.
64 Context (PL:ProgrammingLanguage).
66 (* category of judgments in a fixed type/coercion context *)
67 Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
69 Definition JudgmentsL := Judgments_cartesian.
71 Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
73 apply nd_seq_reflexive.
76 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
81 Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
83 {| eid := identityProof
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.
94 apply nd_cut_associativity.
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]).
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]).
124 Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
126 {| bin_first := Types_first
127 ; bin_second := Types_second
131 Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
135 Definition TypesEnrichedInJudgments : Enrichment.
136 refine {| enr_c := TypesL |}.
139 Structure HasProductTypes :=
143 (* need to prove that if we have cartesian tuples we have cartesian contexts *)
144 Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
148 End LanguageCategory.
149 End Programming_Language.
151 Structure ProgrammingLanguageSMME :=
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)
159 Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
160 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
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))).
169 Definition ArrowInProgrammingLanguage :=
170 @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
174 Section GArrowInLanguage.
175 Context (Guest:ProgrammingLanguageSMME).
176 Context (Host :ProgrammingLanguageSMME).
177 Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
180 Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
182 Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
184 Context (GuestHost:TwoLevelLanguage).
186 Definition FlatObject (x:TypesL _ _ Host) :=
187 forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
189 Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
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.
202 End GArrowInLanguage.
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.
209 Definition OmegaLevelLanguage : Type :=
210 { f : nat -> ProgrammingLanguageSMME
211 & forall n, TwoLevelLanguage (f n) (f (S n)) }.
213 Implicit Arguments ND [ Judgment ].