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.
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.
46 Section Programming_Language.
48 Context {T : Type}. (* types of the language *)
50 Context (Judg : Type).
51 Context (sequent : Tree ??T -> Tree ??T -> Judg).
52 Notation "cs |= ss" := (sequent cs ss) : pl_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$ *)
58 (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
60 Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
62 Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
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:
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).
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.
84 * This also means that we don't need an explicit proof obligation for 4.1.2.
86 Class ProgrammingLanguage :=
87 { pl_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2)
88 ; pl_tsr :> @TreeStructuralRules Judg Rule T sequent
89 ; pl_sc :> @SequentCalculus Judg Rule _ sequent
90 ; pl_subst :> @CutRule Judg Rule _ sequent pl_eqv pl_sc
91 ; pl_sequent_join :> @SequentExpansion Judg Rule T sequent pl_eqv pl_sc pl_subst
93 Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
95 Section LanguageCategory.
97 Context (PL:ProgrammingLanguage).
99 (* category of judgments in a fixed type/coercion context *)
100 Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
102 Definition JudgmentsL := Judgments_cartesian.
104 Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
106 apply nd_seq_reflexive.
109 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
114 Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
116 {| eid := identityProof
119 apply MonoidalCat_all_central.
120 apply MonoidalCat_all_central.
121 unfold identityProof; unfold cutProof; simpl.
122 apply nd_cut_left_identity.
123 unfold identityProof; unfold cutProof; simpl.
124 apply nd_cut_right_identity.
125 unfold identityProof; unfold cutProof; simpl.
127 apply nd_cut_associativity.
130 Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
131 refine {| efunc := fun x y => (nd_rule (@se_expand_right _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)) |}.
132 intros; apply MonoidalCat_all_central.
133 intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
134 apply se_reflexive_right.
135 intros. unfold ehom. unfold comp. simpl. unfold cutProof.
136 rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_right _ c#] _ _ (nd_id1 (b|=c0))
137 _ (nd_id1 (a,,c |= b,,c)) _ [#se_expand_right _ c#]).
138 setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
139 setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]).
143 Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x).
144 eapply Build_EFunctor.
145 instantiate (1:=(fun x y => (nd_rule (@se_expand_left _ _ _ _ _ _ _ (@pl_sequent_join PL) c x y)))).
146 intros; apply MonoidalCat_all_central.
147 intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
148 apply se_reflexive_left.
149 intros. unfold ehom. unfold comp. simpl. unfold cutProof.
150 rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ [#se_expand_left _ c#] _ _ (nd_id1 (b|=c0))
151 _ (nd_id1 (c,,a |= c,,b)) _ [#se_expand_left _ c#]).
152 setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
153 setoid_rewrite (@ndr_comp_left_identity _ _ pl_eqv [b |= c0]).
157 Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
159 {| bin_first := Types_first
160 ; bin_second := Types_second
164 Definition Types_PreMonoidal : PreMonoidalCat Types_binoidal [].
168 Definition TypesEnrichedInJudgments : Enrichment.
169 refine {| enr_c := TypesL |}.
172 Structure HasProductTypes :=
176 (* need to prove that if we have cartesian tuples we have cartesian contexts *)
177 Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
181 End LanguageCategory.
182 End Programming_Language.
184 Structure ProgrammingLanguageSMME :=
187 ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
188 ; plsmme_rule : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
189 ; plsmme_pl : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
190 ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
192 Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
193 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
195 Section ArrowInLanguage.
196 Context (Host:ProgrammingLanguageSMME).
197 Context `(CC:CartesianCat (me_mon Host)).
198 Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
199 Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
202 Definition ArrowInProgrammingLanguage :=
203 @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
207 Section GArrowInLanguage.
208 Context (Guest:ProgrammingLanguageSMME).
209 Context (Host :ProgrammingLanguageSMME).
210 Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
213 Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
215 Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
217 Context (GuestHost:TwoLevelLanguage).
219 Definition FlatObject (x:TypesL _ _ Host) :=
220 forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
222 Definition FlatSubCategory := FullSubcategory (TypesL _ _ Host) FlatObject.
226 Context (F:Retraction (TypesL _ _ Host) FlatSubCategory).
227 Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
228 Lemma FlatteningIsNotDestructive :
229 FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
235 End GArrowInLanguage.
237 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
238 | NLevelLanguage_zero : forall lang, NLevelLanguage O lang
239 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
240 TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
242 Definition OmegaLevelLanguage : Type :=
243 { f : nat -> ProgrammingLanguageSMME
244 & forall n, TwoLevelLanguage (f n) (f (S n)) }.
246 Implicit Arguments ND [ Judgment ].