src/HaskStrongCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongCategory:                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*    Well-typed Haskell terms in a specific tyvar/covar context form a category:  Types(Haskell)                                *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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.
  19
  20 (* the category of flat Haskell terms in a specific Γ Δ context *)
  21 (*
  22 Section HaskFlat.
  23   Context (Γ:TypeEnv)(Δ:CoercionEnv Γ).
  24
  25   Lemma idmor   a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
  26   (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
  27     admit.
  28   Defined.
  29
  30       Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
  31         admit.
  32         Defined.
  33
  34       Definition HaskFlat
  35         : ECategory
  36             (SystemFC_Cat_Flat past)
  37             (Tree ??(@CoreType V))
  38             (fun a s => [(a,s)]).
  39         refine
  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)).
  45         admit.
  46         admit.
  47         admit.
  48         Defined.
  49
  50       Definition HaskFlatEnrichment : SurjectiveEnrichment.
  51         refine {| se_enr := {| enr_c := HaskFlat |} |}.
  52         admit.
  53         Defined.
  54
  55     End HaskFlat.
  56
  57     (* the category of multi-level Haskell terms (n-ary) with a given past *)
  58     Section Hask.
  59       Context (past:@Past V).
  60
  61       Lemma idmor'   a : [] ~~{SystemFC_Cat past}~~> [(a,a)].
  62         (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
  63         admit.
  64         Defined.
  65
  66       Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)].
  67         admit.
  68         Defined.
  69
  70       Definition Hask
  71         : ECategory
  72             (SystemFC_Cat past)
  73             (Tree ??(@LeveledHaskType V))
  74             (fun a s => [(a,s)]).
  75         refine
  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)).
  81         admit.
  82         admit.
  83         admit.
  84         Defined.
  85
  86       Definition HaskEnrichmentMonoidal : MonoidalEnrichment.
  87         refine {| me_enr := {| enr_c := Hask |} |}.
  88         Admitted.
  89
  90       Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment.
  91         refine {| ffme_enr := HaskEnrichmentMonoidal |}.
  92         admit.
  93         admit.
  94         admit.
  95         Defined.
  96     End Hask.
  97
  98     Section ReificationAndGeneralizedArrow.
  99       Context
 100         (past:list ((Tree ??(@LeveledHaskType V)) * V))
 101         (Σ:(Tree ??(@LeveledHaskType V)))
 102         (n:V).
 103
 104       Definition SystemFC_Reification
 105         : Reification
 106         (HaskFlatEnrichment (((Σ,n)::past)))
 107         (HaskEnrichmentMonicMonoidal  (*past*))
 108         (me_i (HaskEnrichmentMonicMonoidal (*past*))).
 109         (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*)
 110         admit.
 111         Defined.
 112 (*
 113       Definition SystemFC_GArrow :=
 114         garrow_from_reification
 115         (HaskFlatEnrichment (((Σ,n)::past)))
 116         (HaskEnrichmentMonicMonoidal (*past*))
 117         SystemFC_Reification.
 118   *)
 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 *)
 122
 123     End ReificationAndGeneralizedArrow.
 124 *)
 125
 126
 127