The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-25 11:36 GMT+02:00 Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>:

Hi!

I would like to implement a function that takes a type and returns another type.
What I have in mind is something like this:

=====================
(* wrong code below! *)

Parameter i: Type.

Fixpoint f(A: Type) := match A with
 | (A1 -> A2) => i -> f(A1) -> f(A2)
 | A0 => i -> A0
end.
======================

I understand why this is wrong (in so many ways!).

My question is: is it possible at all to achieve this kind of type transformation in some other way? If yes, how?

You can reify your types:

Inductive TypeStruct : Type -> Type :=
 | Arrow : forall (A B : Type), TypeStruct A -> TypeStruct B -> TypeStruct (A -> B)
 | Leaf : forall (A : Type), TypeStruct A.

Fixpoint f(A:Type) (TA : TypeStruct A) :=
  match TA (* in TypeStruct A return <your output type which depends on A> *) with
  | Arrow a b ta tb => i -> (f a ta) -> (f b tb)
  | Leaf a => i -> a
  end.

 Example:

Definition Stransf : forall A B, f (A -> B) (Leaf (A->B)) -> f (A -> B) (Arrow A B (Leaf A) (Leaf B)) :=
  fun A B (g : i -> A -> B) (x : i) (h : i -> A) (y : i) =>
  g x (h y).


You may also want to keep it reified:

Parameter i: Type.
Parameter si: TypeStruct i.

Record TTS := TTS_cons { ty : Type; sty : TypeStruct ty }.

Fixpoint f(A:Type) (TA : TypeStruct A) : {T & TypeStruct T} :=
  match TA (* in TypeStruct A return <your output type which depends on A> *) with
  | Arrow a b ta tb =>
    let na := ty (f a ta) in
    let sna := sty (f a ta) in
    let nb := ty (f b tb) in
    let snb := sty (f b tb) in
    TTS_cons (i -> na -> nb)
                    (Arrow i (na -> nb) si (Arrow na nb sna snb)
  | Leaf a => TTS_cons i a si (Leaf a)
  end.

Best regards,

Bruno

--
.../Sedrikov\...