LtacIsFun.v

Ltac fold_args b a r :=
  lazymatch a with
  | unit => exact r
  | b => exact (r -> r)
  | (?c + ?d)%type => exact (ltac:(fold_args b c r) * ltac:(fold_args b d r))%type
  | (b * ?c)%type => exact (r -> ltac:(fold_args b c r))
  | (?c * ?d)%type => exact (c -> ltac:(fold_args b d r))
  | ?a => exact (a -> r)
  end.

Ltac uncurry a :=
  match a with
  | ?a * ?b -> ?c => exact (a -> ltac:(uncurry (b -> c)))
  | ?a => exact a
  end.

(** [fold_type INPUT CANON_FORM OUTPUT] : compute the type of the fold function
    of the type <<INPUT>>, whose canonical form (in terms of [prod] and [sum])
    is <<CANON_FORM>>. The result type of the fold function is <<OUTPUT>>. *)

Ltac fold_type b a r := exact (ltac:(uncurry (ltac:(fold_args b a r) -> r))).

Definition fold_list_type (α β : Type) : Type :=
  ltac:(fold_type (list α) (unit + α * list α)%type β).

(**
<<
fold_list_type = fun α β : Type => β -> (α -> β -> β) -> β
     : Type -> Type -> Type
>> *)