The Coq mailing list

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

Dear Murali,

Interesting question. I must admit that I never thought about if equality of 
pair types is easily decidable or not. I would think that using Type Classes 
(see chapter 19 of the Coq reference manual), it should be easy to define a 
pair of "types with decidable equality", which has then itself a decidable 
quality. Does this solve your problem?

Otherwise the structural recursion method I showed should work equally well 
with whatever type you want, so this problem should be solved. To solve your 
Universe consistency problem, just create a binary tree type similar to your 
list type. Then you won't need to use lists as elements of a list, but can 
have an equivalent structure. In a binary tree, you can use the left child 
pointer to represent depth and the right child pointer to represent siblings 
in your record structure.

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 7:50 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem using heterogeneous lists for PHOAS

Hi Michael

Thanks for the suggestion. It solves the problem I stated in the question. 
But I have an issue using indexed types: I need to define decidable 
(syntactic) equality of the values of [type k]. If I used an indexed type 
(like [pair], or something which stores the field names also), then I can no 
longer write a simple theorem checking if two prod-values are syntactically 
equal. (I understand that using JMeq will solve this issue, but I am trying 
to keep the equality semantics simple if possible, so that I can use rewrites 
and reflexivity without any issues later). Is there any technique I can use 
to keep the syntactic equality of these terms decidable?

Thanks
Murali

On Mon, Dec 15, 2014 at 6:14 AM, Soegtrop, Michael 
<michael.soegtrop AT intel.com>
 wrote:
> 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