bad Nix recursion schemes draft

recursion-schemes.nix

{ lib, libSuper }:

let
  # lib imports {{{1
  inherit (lib.trivial) #{{{2
    comp
    flow
  ;
  inherit (lib.recursionSchemes) #{{{1
    # vMu- vMu_ v-Mu v_Mu # (mod)
    #   Mu-Fix Mu_Fix vMu-Fix vMu_Fix
    vAnn- vAnn_ v-Ann v_Ann # (mod)
      Ann-Ann Ann_Ann vAnn-Ann vAnn_Ann
    # vAttr- vAttr_ v-Attr v_Attr # (mod)
    liftAnn # (mod)
    vCoAnn- vCoAnn_ v-CoAnn v_CoAnn # (mod)
      CoAnn-Pure CoAnn_Pure vCoAnn-Pure vCoAnn_Pure
      CoAnn-CoAnn CoAnn_CoAnn vCoAnn-CoAnn vCoAnn_CoAnn
    # vCoAttr- vCoAttr_ v-CoAttr v_CoAttr # (mod)
    liftCoAnn # (mod)
    attribute # (mod)
    forget # (mod)
    vHole- vHole_ v-Hole v_Hole # (mod)
      Hole-Hole Hole_Hole vHole-Hole vHole_Hole
  ;
in {

  # Base {{{2
  # https://hackage.haskell.org/package/fixplate-0.1.8/docs/Data-Generics-Fixplate-Base.html

  # # type Mu f {{{3
  # /* The fixed-point type.
  # 
  #    Type:
  #      Fix = { unFix :: f (Mu f); } -> Mu f;
  #  */
  # Mu-Fix = { unFix } @ x: x;
  # Mu_Fix = unFix: { inherit unFix; };
  # vMu-Fix = Fix: { unFix } @ x: Fix x;
  # vMu_Fix = Fix: { unFix }: Fix unFix;
  # 
  # v-Mu = vMu-Fix;
  # v_Mu = vMu_Fix;
  # vMu- = { Fix }: v-Mu Fix;
  # vMu_ = { Fix }: v_Mu Fix;

  # Annotations {{{3
  # type Ann f a b {{{4
  /* The type of annotations.

     Type:
       Ann = { attr :: a; unAnn :: f b; } -> Ann f a b;
   */
  Ann-Ann = { attr, unAnn } @ x: x;
  Ann_Ann = attr: unAnn: { inherit attr unAnn; };
  vAnn-Ann = Ann: { attr, unAnn } @ x: Ann x;
  vAnn_Ann = Ann: { attr, unAnn }: Ann attr unAnn;

  v-Ann = vAnn-Ann;
  v_Ann = vAnn_Ann;
  vAnn- = { Ann }: v-Ann Ann;
  vAnn_ = { Ann }: v_Ann Ann;

  # # type Attr f a {{{4
  # /* The annotated fixed-point type. Equivalent to `CoFree f a`.
  # 
  #    Type: Attr f a = Mu (Ann f a)
  #  */
  # v-Attr = Attr: v-Mu ({ unFix } @ x: v-Ann (Attr x) unFix);
  # v_Attr = Attr: v_Mu (unFix: v_Ann (Attr unFix) unFix);
  # vAttr- = { Attr }: v-Attr Attr;
  # vAttr_ = { Attr }: v_Attr Attr;

  # liftAnn {{{4
  /* Lifting natural transformations to annotations.

     Type: (f e -> g e) -> Ann f a e -> Ann g a e
   */

  # comp a (comp b c) = comp (comp a b) c
  # structure: a b (c d e) = a (b c d) e
  # values: comp a comp b c = comp comp a b c

  # comp (comp comp comp) a b c d e = a b (c d e)
  # comp (comp comp comp) comp a comp b c = 

  # (((comp comp) comp) comp) = (comp (comp comp))

  # -> 0 1 1
  # a b c = a b c
  # 0 -> 0 1 2
  # comp a b c = a (b c)
  # 0 1 -> 0 1 1 2
  # (comp comp) a b c d = comp (a b) c d = a b (c d)
  # 0 1 1 -> 0 1 2 2
  # ((comp comp) comp) a b c d = comp a (b c) d = a (b c d)
  # 0 1 2 -> 0 1 1 1 2
  # (comp (comp comp)) a b c d e = (comp comp) (a b) c d e = a b c (d e)
  # 0 1 1 1 = 0 1 2 -> 0 1 1 1 2
  # (((comp comp) comp) comp) = (comp (comp comp))
  # 0 1 2 1 -> 0 1 2 3
  # ((comp (comp comp)) comp) a b c d = comp a b (c d) = a (b (c d))
  # 0 1 2 2 -> 0 1 1 2 2
  # (comp ((comp comp) comp)) a b c d e = ((comp comp) comp) (a b) c d e =
  #   a b (c d e)
  # 0 1 2 3 -> 0 1 1 1 1 3
  # (comp (comp (comp comp))) a b c d e f = (comp (comp comp)) (a b) c d e f =
  #   a b c d (e f)
  # 0 1 1 2 -> 0 1 2 1 2
  # ((comp comp) (comp comp)) a b c d e = (comp comp) a (b c) d e =
  #   a (b c) (d e)
  # 0 1 2 3 4 = 0 1 2 1 -> 0 1 2 3
  # ((((comp comp) comp) comp) comp) = ((comp (comp comp)) comp)
  # comp comp (comp comp) comp a b c d e = comp (comp comp comp) a b c d e =
  #   
  # comp comp comp comp comp comp a b c d e =
  #   comp (comp comp) comp comp a b c d e = comp comp (comp comp) a b c d e =
  #   comp (comp comp a) b c d e = comp comp a (b c) d e =
  #   comp (a (b c)) d e = a (b c) (d e)
  # comp comp comp comp comp comp comp a b c d e =
  #   comp (comp comp) comp comp comp comp a b c d e =
  #   comp comp (comp comp) comp comp a b c d e =
  #   comp (comp comp comp) comp a b c d e = comp comp comp (comp a) b c d e =
  #   comp (comp (comp a)) b c d e = comp (comp a) (b c) d e =
  #   comp a (b c d) e = a (b c d e)
  # flow g f x y z = f (g x) y z
  # flow g flow f x y z = flow (g f) x y z = x (g f) y z
  # flow g flow f flow x y z = flow (g f) flow x y z = flow (g f x) y z =
  #   y (g f x z)
  # flow flow flow g flow f x y z = flow (flow g) flow f x y z =
  #   flow (flow g f) x y z = x (flow g f y) z = x (f (g y)) z
  liftAnn = trafo: v_Ann (attr: comp (Ann_Ann attr) trafo);
  # trafo: ann: v_Ann (attr: unAnn: Ann_Ann attr (trafo unAnn)) ann =
  # trafo: ann: flow (attr: unAnn: Ann_Ann attr (trafo unAnn)) v_Ann ann =
  # trafo: flow (attr: unAnn: Ann_Ann attr (trafo unAnn)) v_Ann =
  # trafo: flow (attr: unAnn: flow trafo (Ann_Ann attr) unAnn) v_Ann =
  # trafo: flow (attr: flow trafo (Ann_Ann attr)) v_Ann =
  # trafo: flow (attr: flow Ann_Ann (flow trafo) attr) v_Ann =
  # trafo: flow (flow Ann_Ann (flow trafo)) v_Ann =
  # trafo: flow (flow flow (flow Ann_Ann) trafo) v_Ann =
  # trafo: flow ((flow flow (flow Ann_Ann)) trafo) v_Ann =
  liftAnn = trafo: v_Ann (attr: unAnn: Ann_Ann attr (trafo unAnn));

  # Co-annotations {{{3
  # type CoAnn f a b {{{4
  /* The categorical dual of `Ann`.

     Type:
       Pure = { coAttr :: a; } -> CoAnn f a b
       CoAnn = { unCoAnn :: f b; } -> CoAnn f a b
   */
  CoAnn-Pure = { coAttr } @ x: x;
  CoAnn_Pure = coAttr: { inherit coAttr; };
  vCoAnn-Pure = Pure: { coAttr } @ x: Pure x;
  vCoAnn_Pure = Pure: { coAttr }: Pure coAttr;

  CoAnn-CoAnn = { unCoAnn } @ x: x;
  CoAnn_CoAnn = unCoAnn: { inherit unCoAnn; };
  vCoAnn-CoAnn = CoAnn: { unCoAnn } @ x: CoAnn x;
  vCoAnn_CoAnn = CoAnn: { unCoAnn }: CoAnn unCoAnn;

  v-CoAnn = Pure: CoAnn: { coAttr ? null, unCoAnn ? null } @ x:
    (if x ? coAttr then vCoAnn-Pure Pure else vCoAnn-CoAnn CoAnn) x;
  v_CoAnn = Pure: CoAnn: { coAttr ? null, unCoAnn ? null } @ x:
    (if x ? coAttr then vCoAnn_Pure Pure else vCoAnn_CoAnn CoAnn) x;
  vCoAnn- = { Pure, CoAnn }: v-CoAnn Pure CoAnn;
  vCoAnn_ = { Pure, CoAnn }: v_CoAnn Pure CoAnn;

  # # type CoAttr f a {{{4
  # /* Categorical dual of `Attr`. Equivalent to `Free f a`.
  # 
  #    Type: CoAttr f a = Mu (CoAnn f a)
  #  */
  # v-CoAttr = CoAttr: v-Mu ({ unFix } @ x: v-CoAnn (Attr x) unFix);
  # v_CoAttr = CoAttr: v_Mu (unFix: v_CoAnn (CoAttr unFix) unFix);
  # vCoAttr- = { CoAttr }: v-CoAttr CoAttr;
  # vCoAttr_ = { CoAttr }: v_CoAttr CoAttr;

  # liftCoAnn {{{4
  /* Lifting natural transformations to annotations.

     Type: (f e -> g e) -> CoAnn f a e -> CoAnn g a e
   */
  liftCoAnn = trafo: v-CoAnn {
    Pure = { attr }: CoAnn_Pure attr;
    CoAnn = { unCoAnn }: CoAnn_CoAnn (trafo unCoAnn);
  };

  # Annotated trees {{{3

  # attribute {{{4
  /* The attribute of the root node.

     Type: Attr f a -> a
   */
  # attribute = v_Mu (v_Ann (attr: _unAnn: attr));
  attribute = v_Ann (attr: _unAnn: attr);

  # forget {{{4
  /* A function forgetting all the attributes from an annotated tree.

     Type: (Functor f) => Attr f a -> Mu f
   */
  forget = tFunctor:
    # v_Attr (unFix: _attr: unAnn: Mu_Fix (fFunctor.map forget unAnn));
    v_Ann (_attr: unAnn: (fFunctor.map forget unAnn));

  # Holes {{{3

  # type Hole {{{4

  Hole-Hole = { } @ x: x;
  Hole_Hole = { };
  vHole-Hole = Hole: { } @ x: Hole x;
  vHole_Hole = Hole: { }: Hole;

  v-Hole = vHole-Hole;
  v_Hole = vHole_Hole;
  vHole- = { Hole }: v-Hole Hole;
  vHole_ = { Hole }: v_Hole Hole;

  # Morphisms {{{2
  # https://hackage.haskell.org/package/fixplate-0.1.8/docs/Data-Generics-Fixplate-Morphisms.html

  # Classic ana/cata/para/hylo-morphisms {{{3
  # cata {{{4
  /* A *catamorphism* is the generalization of right fold from lists to trees.

     Type: (Functor f) => (f a -> a) -> Mu f -> a
   */
  cata = fFunctor: f:
    # let cataF = v_Mu (unFix: f (fFunctor.map cataF unFix)); in
    let cataF = x: f (fFunctor.map cataF x); in
    cataF;

  #}}}1

}
# vim:fdm=marker:fdl=1