The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Coq User a écrit :
> 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.*)
Here is a solution, but it will probably be a pain in the neck to use it.

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