The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Murali,

I am also a beginner, so I might be wrong in what I say, but let me comment 
on your problem.

First I don't think you can make a heterogenous list and then use this list 
as an element type for the list. This should results in Universe errors, as 
you alreay observed. But since a list of lists is more or less equivalent to 
a tree, you can use a tree like data structure to describe your type.

Second it is a bit tricky to do structural recursion on your Kind type, 
because you need to recurse over the Struct and the lists. I couldn't even 
get this to work with mutual recursion, but with so called internal recursion 
(see 
http://www.di.ens.fr/~zappa/teaching/coq/ecole11/summer/lectures/lec9.pdf) it 
works as below. Here I used simpel pairs to construct the type. You might 
want to use something more eloborate to make the structure clearer, but as I 
said before, I think it needs to be a tree like structure, not a list like 
structure. It should e.g. be possible to keep the record filed names in the 
types.

Require Import String.
Require Import List.
Open Scope string_scope.

Inductive Kind: Set :=
| Bool: Kind
| Struct: list (string * Kind) -> Kind.

Fixpoint type (k : Kind) : Type :=
  match k with
  | Bool => bool
  | Struct list => let fix typeaux l : Type :=
    match l with
    | nil => unit
    | (name,elem)::tail => ((type elem)*(typeaux tail))%type
    end in typeaux list
  end.

Example ex1 := Struct (("a",Bool)::("b",Bool)::nil).
Example ex2 := Struct (("s",ex1)::("t",ex1)::nil).
Eval compute in type ex2.
(* = (bool * (bool * unit) * (bool * (bool * unit) * unit))%type : Type *)

Hope it helps.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Murali Vijayaraghavan
Sent: Monday, December 15, 2014 6:47 AM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Problem using heterogeneous lists for PHOAS

Hi all,

I am a novice in using Coq, so I apologize in advance if the answer to my 
question is too trivial or has been answered before (I just got to know about 
this mailing list recently).

So, I am trying to adopt the PHOAS method
(http://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf) to define a 
language.

I have a kind definition as follows (containing booleans and C-structure-like 
objects):

Inductive Kind: Set :=
| Bool: Kind
| Struct: list (string * Kind) -> Kind.

I use heterogeneous lists whose definition is:

Section ilist.
  Variable A : Type. (* The indexing type. *)
  Variable B : A -> Type. (* The type of indexed elements. *)

  Inductive ilist : list A -> Type :=
  | icons : forall a As, B a -> ilist As -> ilist (a :: As)
  | inil : ilist nil.
End ilist.

Now, I am trying to convert an element of the Kind into a Coq-native type 
(like bool, or a heterogeneous list). I need heterogeneous lists because a 
structure can contain other structures as in its elements.

In order to do this, I tried writing the following function [type]:

Fixpoint type (k: Kind): Type :=
  match k with
    | Bool => bool
    | Struct attrs => ilist (fun a => snd a)
                            (map (fun a => (fst a, type (snd a))) attrs)
  end.

This gives me Universe-inconsistency error. From my naive understanding of 
Coq-universes, this error seems reasonable, since I am trying to create a 
type which is quantified by elements, and these elements can in turn contain 
the same type. But I am not sure if this explanation is correct.

I tried another variant of the same function:

Fixpoint type (k: Kind): Type :=
  match k with
    | Bool => bool
    | Struct attrs => ilist (fun a => type (snd a)) attrs
  end.

This gives me the recursive call error: [Recursive call to type has principal 
argument equal to "snd a" instead of "attrs"]. My understanding of this error 
is that Coq is not able to figure out the decreasing argument of type, since 
I am applying it on some argument, instead of on [attrs] directly.

This brings to my question: is there any way to write what I wanted to, which 
is, convert values of my [Kind] into Coq-native types. I am open to using 
some other [Type] instead of [ilist], if that can solve my problem.

Thanks
Murali