coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <sedrikov AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Function that transforms types
- Date: Fri, 25 Jul 2014 12:13:55 +0200
2014-07-25 11:36 GMT+02:00 Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>:
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.
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\...
- [Coq-Club] Function that transforms types, Bruno Woltzenlogel Paleo, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Arthur Azevedo de Amorim, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Cedric Auger, 07/25/2014
- Re: [Coq-Club] Function that transforms types, Daniel Schepler, 07/25/2014
Archive powered by MHonArc 2.6.18.