Parametricity in Mutual Inductive Types

[roconnor]

According to the Coq manual, mutually defined inductive types must have
the same parameters for all inductive definitions.  Is this restriction
fundamental, or is there only to simplify the implemenation?

I'll try to give a simplified example of where I want to have mutually
defined inductive definitions with different parameters below.  I have a
real example in mind for the definion of a type for the syntax of a
moderately complex language.

Consider the type family of silly trees:

Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTree b -> SillyTree b -> SillyTree false.

I want to be able to pattern match on my silly trees like in the
following:

Definition sillyFunction (st:SillyTree false) : bool :=
match st with
| node a leaf leaf => a
| _ => false
end.

The above works all fine.  But now I want to capture the pair of
SillyTrees occuring in the node constructor as its own type, because I
want to reuse this notion in many places.  I try to make a mutual
inductive type:

Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair (b:bool) : Type :=
  | stp : SillyTree b -> SillyTree b -> SillyTreePair b.

but this fails because the type parameters are not all the same in the
different defintions.

One attempted solution is to make SillyTreePair a family:

Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair : bool -> Type :=
  | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair b.

however, there is a problem.  When pattern matting we get a new pattern
variable bound:

Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (stp b leaf leaf) => a (* a must equal b,
                               but pattern matching forces us to
                               provide a new pattern variable b *)
| _ => false
end.

This new variable b must always be equal to a; however we do not get such
a proof when doing normal pattern matching.

Another attempt is to use the existing product type to capture this pair
as one object.

Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, (SillyTree b * SillyTree b) -> SillyTree false.

Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (pair leaf leaf) => a
| _ => false
end.

This works, but we no longer get our own type for (SillyTree b * SillyTree
b).  In particular, I want to define coercions from SillyTreePairs, but
now I cannot do it because I'm using the general prod type.

I could define my own pair type:

Inductive TreePair (A : Type) : Type := treePair : A -> A -> TreePair A.

but I have to make it polymorphic.  I have no way to make it only hold
SillyTrees like I want it to be restricted to.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

(* find '--' patterns for my replies *)

(* According to the Coq manual,
  mutually defined inductive types
  must have the same parameters for all inductive definitions.
   Is this restriction fundamental,
  or is there only to simplify the implemenation? *)

(*-- It is fundamental, but as you did below, we can have dependent types,
   which accepts different parameters,
  and dealing is not as easy as with non dependent types *)

(* I'll try to give a simplified example of
  where I want to have mutually defined
  inductive definitions with different parameters below.
   I have a real example in mind for the definion of
  a type for the syntax of a moderately complex language. *)

(* Consider the type family of silly trees: *)
(*
Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTree b -> SillyTree b -> SillyTree false.
*)
(* I want to be able to pattern match on my silly trees like in the  
following: *)
(*
Definition sillyFunction (st:SillyTree false) : bool :=
match st with
| node a leaf leaf => a
| _ => false
end.
*)
(* The above works all fine.
   But now I want to capture the pair of
  SillyTrees occuring in the node constructor as
  its own type, because I want to reuse this notion in many places.
   I try to make a mutual inductive type: *)
(*
Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair (b:bool) : Type :=
  | stp : SillyTree b -> SillyTree b -> SillyTreePair b.

but this fails because the type parameters are not all the same in the  
different defintions.

One attempted solution is to make SillyTreePair a family:

Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, SillyTreePair b -> SillyTree false
with SillyTreePair : bool -> Type :=
  | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair b.
*)
(*-- And what about: *)
Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : SillyTreePair -> SillyTree false
with SillyTreePair : Type :=
  | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair.
(*
however, there is a problem.  When pattern matting we get a new pattern  
variable bound:

Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (stp b leaf leaf) => a (* a must equal b,
                               but pattern matching forces us to
                               provide a new pattern variable b *)
| _ => false
end.
*)
(* This new variable b must always be equal to a;
  however we do not get such a proof when doing normal pattern matching. *)
Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node (stp b leaf leaf) => b (* a must equal b,
                               but pattern matching forces us to
                               provide a new pattern variable b *)
| _ => false
end.

(* Another attempt is to use the existing product type
  to capture this pair as one object. *)
(*
Inductive SillyTree : bool -> Type :=
  | leaf : SillyTree true
  | node : forall b, (SillyTree b * SillyTree b) -> SillyTree false.
*)
(*-- that is what I did upper but in a non embedded structure, so you can  
use it
  separetely *)

(* Definition isMyTree (st:SillyTree false) : bool :=
match st with
| node a (pair leaf leaf) => a
| _ => false
end.
*)
(*
This works, but we no longer get our own type for (SillyTree b * SillyTree  
b).  In particular, I want to define coercions from SillyTreePairs, but  
now I cannot do it because I'm using the general prod type.

I could define my own pair type:

Inductive TreePair (A : Type) : Type := treePair : A -> A -> TreePair A.

but I have to make it polymorphic.
   I have no way to make it only hold SillyTrees like I want it to be  
restricted to.
*)

(* Hope it helped,

Cedric *)

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[roconnor]

On Fri, 16 Oct 2009, AUGER Cédric wrote:

> (*-- It is fundamental, but as you did below, we can have dependent types,
> which accepts different parameters,
> and dealing is not as easy as with non dependent types *)

It appears Agda can do it, so I don't understand why you say it is
fundamental.

module SillyTree where
{- my first agda program -}
data bool : Set where
   true : bool
   false : bool

mutual
   data SillyTree : bool -> Set where
     leaf : SillyTree true
     node : (b : bool) -> SillyTreePair b -> SillyTree false

   data SillyTreePair (b : bool) : Set where
     stp : SillyTree b -> SillyTree b -> SillyTreePair b

sillyFunction : SillyTree false -> bool
sillyFunction (node true (stp leaf leaf)) = true
sillyFunction _ = false

> (*-- And what about: *)
> Inductive SillyTree : bool -> Type :=
> | leaf : SillyTree true
> | node : SillyTreePair -> SillyTree false
> with SillyTreePair : Type :=
> | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair.

This is nice, but not adequate for my purposes because I want to have
SillyTreePair indexed by bool for the other uses of SillyTreePair I have
in mind.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

[muad]

I feel like I might still not understand exactly what is needed, but perhaps this is a solution?

Inductive SillyTreePair SillyTree (b:bool) : Type :=
| stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.

Inductive SillyTree : bool -> Type :=
| leaf : SillyTree true
| node : forall b, SillyTreePair SillyTree b -> SillyTree false.

Definition sillyFunction (st:SillyTree false) : bool :=
  match st with
    | node a (stp leaf leaf) => a
    | _ => false
  end.

SillyTree is making use of the fact that SillyTreePair f b is a strictly positive operator in f.

[roconnor]

On Sat, 17 Oct 2009, muad wrote:

> I feel like I might still not understand exactly what is needed, but perhaps
> this is a solution?
>
> Inductive SillyTreePair SillyTree (b:bool) : Type :=
> | stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.
>
> Inductive SillyTree : bool -> Type :=
> | leaf : SillyTree true
> | node : forall b, SillyTreePair SillyTree b -> SillyTree false.
>
> Definition sillyFunction (st:SillyTree false) : bool :=
>  match st with
>    | node a (stp leaf leaf) => a
>    | _ => false
>  end.
>
> SillyTree is making use of the fact that SillyTreePair f b is a strictly
> positive operator in f.

Yes this works, and is a varient of what I had in mind for my very last
possible solution that I didn't write out in detail.  It is just a little
sad that SillyTreePair ends up being polymorphic in the SillyTree
parameter, which means another parameter needs to be passed everywhere.

I would probably rename your SillyTreePair as preSillyTreePair and then
define (prehaps a notation) SillyTreePair := preSillyTreePair SillyTree.

Perhaps this is the best compromise, but it still isn't as nice as what
you can express in Agda.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[roconnor]

On Sat, 17 Oct 2009, roconnor@... wrote:

> On Sat, 17 Oct 2009, muad wrote:
>
>> I feel like I might still not understand exactly what is needed, but
>> perhaps
>> this is a solution?
>>
>> Inductive SillyTreePair SillyTree (b:bool) : Type :=
>> | stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.
>>
>> Inductive SillyTree : bool -> Type :=
>> | leaf : SillyTree true
>> | node : forall b, SillyTreePair SillyTree b -> SillyTree false.
>>
>> Definition sillyFunction (st:SillyTree false) : bool :=
>>  match st with
>>    | node a (stp leaf leaf) => a
>>    | _ => false
>>  end.
>>
>> SillyTree is making use of the fact that SillyTreePair f b is a strictly
>> positive operator in f.
>
> Yes this works, and is a varient of what I had in mind for my very last
> possible solution that I didn't write out in detail.  It is just a little sad
> that SillyTreePair ends up being polymorphic in the SillyTree parameter,
> which means another parameter needs to be passed everywhere.
>
> I would probably rename your SillyTreePair as preSillyTreePair and then
> define (prehaps a notation) SillyTreePair := preSillyTreePair SillyTree.

Remark: a notation didn't work in my real application because I need
`SillyTreePair' to be a target for a coercion.

> Perhaps this is the best compromise, but it still isn't as nice as what you
> can express in Agda.
>
>

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Christine Paulin-2]

Just a comment on this subject:

Until quite recently, the rule for an argument A to be a parameter of an
inductive definition Ind was that any instance of Ind in the type of a
constructor either as argument or in the conclusion should be applied to A.

The spirit was that the inductive definition was made in the context of
the variable A and then discharged. Also for the induction principle,
this is a condition for A to be treated as a parameter. This was the
reason for mutual inductive definitions to share the same parameters.

Then, taking advantadge of the separation Fix/Match (versus a general
induction principle) the condition for parameters was relaxed such that
Ind in the arguments of constructors could be freely instantiated. Here
the idea was that Ind could have been be defined as an indexed family
and then the "parametric" pattern-matching is derivable (although we
need to keep the indexed family view for the induction principle).
The derived principle is nice in principle but in order to use it you
have to give up the pattern-matching notation.

So I do not see any major theoretical reason to reject mutual inductive
definitions with different set of parameters. It is just a bit of work
to change the implementation consistently.

Christine



roconnor@... wrote:

> On Sat, 17 Oct 2009, muad wrote:
>
>> I feel like I might still not understand exactly what is needed, but
>> perhaps
>> this is a solution?
>>
>> Inductive SillyTreePair SillyTree (b:bool) : Type :=
>> | stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.
>>
>> Inductive SillyTree : bool -> Type :=
>> | leaf : SillyTree true
>> | node : forall b, SillyTreePair SillyTree b -> SillyTree false.
>>
>> Definition sillyFunction (st:SillyTree false) : bool :=
>>  match st with
>>    | node a (stp leaf leaf) => a
>>    | _ => false
>>  end.
>>
>> SillyTree is making use of the fact that SillyTreePair f b is a strictly
>> positive operator in f.
>
> Yes this works, and is a varient of what I had in mind for my very last
> possible solution that I didn't write out in detail.  It is just a
> little sad that SillyTreePair ends up being polymorphic in the SillyTree
> parameter, which means another parameter needs to be passed everywhere.
>
> I would probably rename your SillyTreePair as preSillyTreePair and then
> define (prehaps a notation) SillyTreePair := preSillyTreePair SillyTree.
>
> Perhaps this is the best compromise, but it still isn't as nice as what
> you can express in Agda.
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club