1 (*********************************************************************************************************************************)
2 (* HaskStrongCategory: *)
4 (* Well-typed Haskell terms in a specific tyvar/covar context form a category: Types(Haskell) *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
14 Require Import HaskKinds.
15 Require Import HaskCoreTypes.
16 Require Import HaskLiteralsAndTyCons.
17 Require Import HaskStrongTypes.
18 Require Import HaskStrong.
20 (* the category of flat Haskell terms in a specific Γ Δ context *)
23 Context (Γ:TypeEnv)(Δ:CoercionEnv Γ).
25 Lemma idmor a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
26 (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
30 Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
36 (SystemFC_Cat_Flat past)
37 (Tree ??(@CoreType V))
40 {| eid := fun a => idmor a
41 ; ecomp := fun a b c => compmor a b c
42 |}; intros; simpl in *; auto.
43 apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
44 apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
50 Definition HaskFlatEnrichment : SurjectiveEnrichment.
51 refine {| se_enr := {| enr_c := HaskFlat |} |}.
57 (* the category of multi-level Haskell terms (n-ary) with a given past *)
59 Context (past:@Past V).
61 Lemma idmor' a : [] ~~{SystemFC_Cat past}~~> [(a,a)].
62 (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
66 Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)].
73 (Tree ??(@LeveledHaskType V))
76 {| eid := fun a => idmor' a
77 ; ecomp := fun a b c => compmor' a b c
78 |}; intros; simpl in *; auto.
79 apply (MonoidalCat_all_central (SystemFC_Cat past)).
80 apply (MonoidalCat_all_central (SystemFC_Cat past)).
86 Definition HaskEnrichmentMonoidal : MonoidalEnrichment.
87 refine {| me_enr := {| enr_c := Hask |} |}.
90 Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment.
91 refine {| ffme_enr := HaskEnrichmentMonoidal |}.
98 Section ReificationAndGeneralizedArrow.
100 (past:list ((Tree ??(@LeveledHaskType V)) * V))
101 (Σ:(Tree ??(@LeveledHaskType V)))
104 Definition SystemFC_Reification
106 (HaskFlatEnrichment (((Σ,n)::past)))
107 (HaskEnrichmentMonicMonoidal (*past*))
108 (me_i (HaskEnrichmentMonicMonoidal (*past*))).
109 (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*)
113 Definition SystemFC_GArrow :=
114 garrow_from_reification
115 (HaskFlatEnrichment (((Σ,n)::past)))
116 (HaskEnrichmentMonicMonoidal (*past*))
117 SystemFC_Reification.
119 (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor;
120 * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory
121 * of Hask which consists of the (GArrow g => g a b) morphisms *)
123 End ReificationAndGeneralizedArrow.