calculus/Calculus/Lambda/Omega/Explicit/lib/Functor.cloe

   1 Functor_Fmap
   2  (F:* -> *) (X:*) (Y:*)
   3  = (X -> Y) -> F X -> F Y
   4
   5 Functor_Class
   6  (F:* -> *) (Data:*)
   7  =  (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
   8  -> Data
   9 Functor_Polytype
  10  (F:* -> *) : *p
  11  = (Data:*) -> Functor_Class F Data -> Data
  12 Functor
  13  (F:* -> *) : *m
  14  = Monotype (Functor_Polytype F)
  15
  16 functor
  17  (F:* -> *)
  18  (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
  19  : Functor F
  20  = monotype (Functor_Polytype F)
  21      (λ(Data:*) (functor_class:Functor_Class F Data) -> functor_class fmap)
  22 unFunctor
  23  (F:* -> *) (Data:*)
  24  (functor_class:Functor_Class F Data)
  25  (functor:Functor F)
  26  : Data
  27  = polytype (Functor_Polytype F) functor Data functor_class
  28
  29 Functor_fmap
  30  (F:* -> *) (functor:Functor F) (X:*) (Y:*)
  31  : Functor_Fmap F X Y
  32  = unFunctor F (Functor_Fmap F X Y)
  33     (λ(fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y) -> fmap X Y)
  34     functor