The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

In addition to the option of providing an object which interprets to a
type, you could also use typeclasses to achieve something which looks
similar:

Parameter i : Type.

Class FTransform (A:Type) : Type :=
f : Type.

(* Make A argument to f explicit, but keep the instance argument implicit. *)
Arguments f A [FTransform].

Instance FTransformBase (A:Type) : FTransform A | 5 :=
i -> A.

Instance FTransformArrow (A B:Type) `{!FTransform A} `{!FTransform B} :
  FTransform (A -> B) | 3 :=
i -> f A -> f B.

This isn't actually a function of only a type, but in fact it's a
function of an instance argument constructed automatically via an
eauto like procedure.  The | 5 and | 3 provide precedence levels
(higher numbers mean lower precedence).  So now:

Eval compute in (f (nat -> nat -> nat)).
=>
     = i -> (i -> nat) -> i -> (i -> nat) -> i -> nat
     : Type
-- 
Daniel Schepler

On Fri, Jul 25, 2014 at 2:36 AM, Bruno Woltzenlogel Paleo
<bruno.wp AT gmail.com>
 wrote:
> 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