The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/08/2014 10:53 AM, 
saulo2 AT gmail.com
 wrote:
> Hi,
>
> I am trying to port a defitional interpreter for a small DSL from Standard ML
> to Coq. The first problem I am facing is how to define self referential values
> in Coq. Thats what I am trying to do:
>
> Require Import String.
> Open Scope string_scope.
>
> Inductive OBJECT : Type := Object : CLASS -> list (string * OBJECT) -> OBJECT
>       with CLASS : Type := Class : list (string * CLASS) -> CLASS.
>
> Definition MediaType := Class nil.
> Print MediaType.
>
> Definition File := Class (cons ("mediaType", MediaType) nil).
> Print File.
>
> Definition User := Class (cons ("picture", File) nil).
> Print User.
>
> Definition Message := Class (cons ("sender", User) (
>      cons ("recipients", User) (
>        cons ("replies", Message) nil
>      )
>    )
> ).
> Print Message.
>
> but the Coq complier complains "Error: The reference Message was not found in
> the current environment."

What you were trying to do with Message is define a self-referential 
(cyclic) data object, which Coq won't let you do (unless you use codata 
- but you probably don't want that).

You should probably put a level of indirection between a class's 
structural definition and its use.  I would suggest defining class tags 
first, then class structures that reference those tags.  Then define a 
mapping from class tags to class structures.

This might look something like:

Inductive CLASSTAG : Type := ClassTag : string -> CLASSTAG.

Inductive OBJECT : Type := Object : CLASS -> list (string * OBJECT) -> OBJECT
     with CLASS : Type := Class : list (string * CLASSTAG) -> CLASS.

...
Definition Message := Class (cons ("sender", ClassTag "User") (
    cons ("recipients", ClassTag "User") (
      cons ("replies", ClassTag "Message") nil
    )
  )
).
...
 
Definition tag_to_class : CLASSTAG -> CLASS := ...


-- Jonathan