The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hi Bruno,

You can solve your problem by using one level of indirection. Instead
of writing f : Type -> Type, you can define a type "code", together
with a function denote : code -> Type:

Inductive code :=
| Arrow : code -> code -> code (* Function type *)
| (*... other types *)...

Fixpoint denote (c : code) : Type :=
match c with
| Arrow c1 c2 => denote c1 -> denote c2
| (* ... *)
end.

having done that, you can then define f directly on "code". You'll
have to restrict your universe of types to do this, but this should be
enough for many applications.

Best,

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?
>
> Best regards,
>
> Bruno



-- 
Arthur Azevedo de Amorim