Kombinators for scaling simple trait and/or combinators to n-way product/sum combinators.

Kombinators.v

Inductive choice a b :=
| C1 : a -> choice a b
| C2 : b -> choice a b.

Notation " a ++ b " := (choice a b).

Module Type TRAIT.
  Parameter t : Type -> Type.
  Parameter and : forall {a b}, t a -> t b -> t (a * b).
  Parameter or : forall {a b}, t a -> t b -> t (a ++ b).
  Parameter convert : forall {a b}, (a -> b) -> (b -> a) -> t a -> t b.
  Parameter unit : t unit.
End TRAIT.

Module Type PRODUCT_COMBINATORS.
  Declare Module T : TRAIT. 
  Parameter p : Type -> Type -> Type -> Type.
  Parameter define : forall {r x z}, x -> p r x z -> T.t r.
  Parameter element : forall {a f r x}, (r -> f) -> T.t f -> p r a x -> p r (f -> a) (f * x).
  Parameter done : forall {r}, p r r unit.
End PRODUCT_COMBINATORS.

Module Type SUM_COMBINATORS.
  Declare Module T : TRAIT.
  Parameter p : Type -> Type -> Type -> Type -> Type.  
  Parameter define : forall {t u y}, (u -> t) -> p u t y y -> T.t u.
  Parameter element : forall {c t u x y}, (c -> u) -> T.t c -> p u t x y -> p u ((c -> y) -> t) (c ++ x) y.
  Parameter done : forall {c u y}, (c -> u) -> T.t c -> p u ((c -> y) -> y) c y.
End SUM_COMBINATORS.          




Module ProductCombinators (T : TRAIT) : PRODUCT_COMBINATORS with Module T := T.

  Module T := T.

  Inductive part (r x z : Type) : Type :=
  | P : (r -> z) -> (x -> z -> r) -> T.t z -> part r x z.

  Definition p r x z := part r x z.

  Definition define {r x z} (e : x) (p : p r x z) : T.t r :=
    match p with
      | P f g t => T.convert (g e) f t
    end.
  
  Definition element {a f r x} (proj : r -> f) (tf : T.t f) (pt : p r a x) : p r (f -> a) (f * x) :=
    match pt with
      | P g h tr =>
          P _ _ _
            (fun rr => (proj rr, g rr))
            (fun c fx => h (c (fst fx)) (snd fx))
            (T.and tf tr)
    end.
  
  Definition done {r} : p r r unit :=
    P r r unit (fun rr => tt) (fun rr tt => rr) T.unit.
  
End ProductCombinators.




Module SumCombinators (T : TRAIT) : SUM_COMBINATORS with Module T := T.

  Module T := T.

  Inductive part (u t x y : Type) : Type :=
  | pd : T.t x -> (x -> u) -> ((x -> y) -> (t -> y)) -> part u t x y.

  Definition p u t x y := part u t x y.

  Definition done {c u y} (inj : c -> u) (tc : T.t c) : p u ((c -> y) -> y) c y :=
    pd _ _ _ _ tc inj (fun h t => t h).

  Definition define {t u y} (ev : u -> t) (pt : p u t y y) : T.t u :=
    match pt with
      | pd tr xu f => T.convert xu (fun u => f (fun x => x) (ev u)) tr
    end.

  Definition element {c t u x y} (inj : c -> u) (tc : T.t c) (pt : p u t x y)
    : p u ((c -> y) -> t) (choice c x) y :=
    match pt with
      | pd tr xu f =>
          pd _ _ _ _
             (T.or tc tr)
             (fun ch =>
                match ch with
                  | C1 x => inj x
                  | C2 x => xu x
                end)
             (fun g h =>
                f (fun x => g (C2 _ _ x)) (h (fun x => g (C1 _ _ x))))
    end.

End SumCombinators.




Module Examples (T : TRAIT).

  Module P := ProductCombinators(T).
  Module S := SumCombinators(T).

  Section TraitExamples.
    Variable x y : Type.
    Variable xT : T.t x.
    Variable yT : T.t y.

    Notation "a $ b" := (a b) (at level 100, right associativity).

    Record P :=
      MakeP { PX : x; PY : y }.
    
    Definition pTrait : T.t P :=
      P.define MakeP
               $ P.element PX xT
               $ P.element PY yT
               $ P.done.

    Inductive U :=
    | U1 : x -> U
    | U2 : y -> U.

    Definition uTrait : T.t U :=
      S.define (fun u k1 k2 =>
                  match u with
                    | U1 x1 => k1 x1
                    | U2 x2 => k2 x2
                  end)
               $ S.element U1 xT
               $ S.done U2 yT.
  End TraitExamples.

End Examples.