polynomial.elf

% dependency: finite.elf (run with sources.cfg)

% polynomial maps (via PFPL ch14 on "generic programming")
% transformation that takes a polynomial over a type
% t, and maps a transformation over data structures
% with that shape.

poly : (ty+ -> ty+) -> type.
poly/const : poly ([t] A).
poly/id : poly ([t] t).
poly/prod : poly ([t] A t) -> poly ([t] B t)
  -> poly ([t] tprod (A t) (B t)).
poly/sum : poly ([t] A t) -> poly ([t] B t)
  -> poly ([t] tsum (A t) (B t)).


map : poly P
   -> trans A C
   -> trans (P A) (P C) -> type.
%mode map +P +T1 -T2.

map/id 
  : map poly/id T T.

map/const 
  : map poly/const (T : trans B C) id.

map/prod 
  : map 
    (poly/prod (Poly1 : poly P1) (Poly2 : poly P2)) 
    % ([t] tprod (P1 t) (P2 t)) 
    (T : trans A C) 
    (split [x] [y]
        (bind (app x T1)
          ([z] bind (app y T2)
            ([w] ret (pair z w)))))
  <- map Poly1 T (T1 : trans (P1 A) (P1 C))
  <- map Poly2 T (T2 : trans (P2 A) (P2 C)).

map/sum
  : map % ([t] tsum (P1 t) (P2 t))
    (poly/sum (Poly1 : poly P1) (Poly2 : poly P2))
    (T : trans A C)
    (case 
        % branch 1: apply T1, then inl
        ([x:value (P1 A)] 
          bind (app x T1)
          ([z] ret (inl z)))
        % branch 2: apply T2, then inr
        ([y:value (P2 A)] 
          bind (app y T2)
          ([w] ret (inr w)))
    ) 
  <- map Poly1 T T1
  <- map Poly2 T T2.

% %worlds () (map _ _ _).
% %total P (map P _ _).