src/HaskStrongCategory.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongCategory:                                                                                                           *)
   3 (*                                                                                                                               *)
   4 (*    Well-typed Haskell terms in a specific tyvar/covar context form a category                                                 *)
   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 (*
  21     (* the category of flat Haskell terms (n-ary) *)
  22     Section HaskFlat.
  23
  24       Context (past:@Past V).
  25
  26       Lemma idmor   a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
  27         (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
  28         admit.
  29         Defined.
  30
  31       Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
  32         admit.
  33         Defined.
  34
  35       Definition HaskFlat
  36         : ECategory
  37             (SystemFC_Cat_Flat past)
  38             (Tree ??(@CoreType V))
  39             (fun a s => [(a,s)]).
  40         refine
  41           {| eid   := fun a     => idmor   a
  42            ; ecomp := fun a b c => compmor a b c
  43           |}; intros; simpl in *; auto.
  44         apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
  45         apply (MonoidalCat_all_central (SystemFC_Cat_Flat past)).
  46         admit.
  47         admit.
  48         admit.
  49         Defined.
  50
  51       Definition HaskFlatEnrichment : SurjectiveEnrichment.
  52         refine {| se_enr := {| enr_c := HaskFlat |} |}.
  53         admit.
  54         Defined.
  55
  56     End HaskFlat.
  57
  58     (* the category of multi-level Haskell terms (n-ary) with a given past *)
  59     Section Hask.
  60       Context (past:@Past V).
  61
  62       Lemma idmor'   a : [] ~~{SystemFC_Cat past}~~> [(a,a)].
  63         (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
  64         admit.
  65         Defined.
  66
  67       Lemma compmor' a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat past}~~> [(a,c)].
  68         admit.
  69         Defined.
  70
  71       Definition Hask
  72         : ECategory
  73             (SystemFC_Cat past)
  74             (Tree ??(@LeveledHaskType V))
  75             (fun a s => [(a,s)]).
  76         refine
  77           {| eid   := fun a     => idmor'   a
  78            ; ecomp := fun a b c => compmor' a b c
  79           |}; intros; simpl in *; auto.
  80         apply (MonoidalCat_all_central (SystemFC_Cat past)).
  81         apply (MonoidalCat_all_central (SystemFC_Cat past)).
  82         admit.
  83         admit.
  84         admit.
  85         Defined.
  86
  87       Definition HaskEnrichmentMonoidal : MonoidalEnrichment.
  88         refine {| me_enr := {| enr_c := Hask |} |}.
  89         Admitted.
  90
  91       Definition HaskEnrichmentMonicMonoidal : MonicMonoidalEnrichment.
  92         refine {| ffme_enr := HaskEnrichmentMonoidal |}.
  93         admit.
  94         admit.
  95         admit.
  96         Defined.
  97     End Hask.
  98
  99     Section ReificationAndGeneralizedArrow.
 100       Context
 101         (past:list ((Tree ??(@LeveledHaskType V)) * V))
 102         (Σ:(Tree ??(@LeveledHaskType V)))
 103         (n:V).
 104
 105       Definition SystemFC_Reification
 106         : Reification
 107         (HaskFlatEnrichment (((Σ,n)::past)))
 108         (HaskEnrichmentMonicMonoidal  (*past*))
 109         (me_i (HaskEnrichmentMonicMonoidal (*past*))).
 110         (* refine {| reification_rstar_f := EscBrak_Functor Γ past n Σ |}.*)
 111         admit.
 112         Defined.
 113 (*
 114       Definition SystemFC_GArrow :=
 115         garrow_from_reification
 116         (HaskFlatEnrichment (((Σ,n)::past)))
 117         (HaskEnrichmentMonicMonoidal (*past*))
 118         SystemFC_Reification.
 119   *)
 120       (* I think we have to add a proof that the derived GArrow's range is in the "monoidal closure" of the reification functor;
 121        * from there we can show that -- in the case of Hask and System FC -- that range is a retract of some other subcategory
 122        * of Hask which consists of the (GArrow g => g a b) morphisms *)
 123
 124     End ReificationAndGeneralizedArrow.
 125 *)
 126
 127