coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <Cedric.Auger AT lri.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] CoInductive Type Instantiation
- Date: Wed, 29 Jul 2009 20:46:38 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Coq User a écrit :
Here is a solution, but it will probably be a pain in the neck to use it.
In the (very simplified) example below some coinductive types are defined for a Parent and Child relationship. How can a Parent or Child be instantiated since they both co-refer to each other? Can it be done as in object oriented programming where a Parent would be defined with a 'null' child first and similarly the Child be defined with 'null' and later the fields be updated to refer to each other? How?
Require Import String.
CoInductive Parent:Set :=
| Build_Parent (fatherOrMother:string)(child:Child)
with
Child:Set :=
| Build_Child (father:Parent)(mother:Parent).
(*Functions for Parent fields.*)
Definition fatherOrMother:Parent -> string := (fun p:Parent =>
match p with
| (Build_Parent fm ch) => fm
end).
Definition child:Parent -> Child := (fun p:Parent =>
match p with
| (Build_Parent fm ch) => ch
end).
(*Functions for Child*)
Definition father:Child -> Parent := (fun p:Child =>
match p with
| (Build_Child f m) => f
end).
Definition mother:Child -> Parent := (fun p:Child =>
match p with
| (Build_Child f m) => m
end).
(*Instantiate a Parent*)
Definition father:Parent := Build_Parent "father"
(
(Build_Child ( (*Father ??? How to refer to the same father Instance being defined here???*)) ((*Mother*)))
).
(*Same problem if we try to instantiate the Child first.*)
CoFixpoint father2 : Parent :=
Build_Parent "father" (Build_Child father2 mother2)
with mother2 : Parent :=
Build_Parent "mother" (Build_Child father2 mother2).
Forget OOprogramming in Coq, and above all forget those tricks, you are in a purely functionnal language you CANNOT do side effects,
you can define Monads as in Haskell, or "emulate" the memory with a list (or a map), which is probably a bad idea, for example
have a positive map:
parents:
1 -> ("father", 1)
10 -> ("mother", 1)
childs:
1 -> (1, 10)
--
Cédric AUGER
Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
- [Coq-Club] CoInductive Type Instantiation, CoqUser CoqUser
- <Possible follow-ups>
- [Coq-Club] CoInductive Type Instantiation, CoqUser CoqUser
- [Coq-Club] CoInductive Type Instantiation,
Coq User
- Re: [Coq-Club] CoInductive Type Instantiation, Cedric Auger
Archive powered by MhonArc 2.6.16.