The Coq mailing list

[Murali Vijayaraghavan <vmurali AT csail.mit.edu>]

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