The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

> I agree we are in desperate need for a practical semantics for  
> inductive families.

Not sure what practical means but what is the problem with the one in  
our LICS paper?
http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf

> With regard to what the criteria should be for legal data types or  
> legal injective data types, I did not fully understand your  
> proposal.  The reason why parameters to data types (as opposed to  
> indices) can be arbitrarily large is that in a "Section" (Coq- 
> terminology) with
>
>  Hypothesis X : very_large_type.
>
>  data List : Set where
>    ...
>
> one can close the section and abstract over all hypotheses,  
> including X, which will be added as a parameter to List:
>
>  data List (X : very_large_type) : Set
>
> Thus, example J is not accepted by accident.  The ability to  
> abstract freely is crucial.  It does not lead to inconsistencies  
> since the typing of constructors ensures that elements of X are  
> never stored in Lists.
>
> Surely, Vec
>
>  data Vec (A : Set) : Nat -> Set where
>    vnil  : Vec A zero
>    vcons : A -> Vec A n -> Vec A (suc n)
>
> should be injective in both arguments, but I would not deduce this  
> from size considerations.  In this case it holds even if Vec would  
> be just a definition
>
>  Vec A zero    = 1
>  Vec A (suc n) = A * Vec n
>
> because the cartesian product is injective.

How do you prove that cartesian product is injective? Or List?

Cheers,
Thorsten

>  Inferring injectivity from the definition is a very conservative  
> approach, and you may have a more liberal proposal in mind which I  
> would be interested to learn more about.  Yet, I do not think it can  
> be realized with the predicativity restriction, since Set and Set ->  
> Set are both part of the same universe Set1, hence, need to be  
> distinguished otherwise in order to separate the good (Vec) from the  
> bad (I, J).  Probably that size check would be more like the  
> positivity test for data types.
>
> Cheers,
> Andreas
>
> P.S.:  I would have expected that
>
>  data I : (Set -> Set) -> Set where
>
> is not even a well-formed inductive family in Agda, since the index  
> (Set -> Set) is too large.  But since there are no constructors, it  
> goes through...
>
>
> Chung Kil Hur a écrit :
> > ----- Original Message ----- From: "Andrew Pitts" <Andrew.Pitts AT cl.cam.ac.uk 
> > >
> > To: "Agda mailing list" 
> > <agda AT lists.chalmers.se>
> > Cc: "Andrew M Pitts" 
> > <andrew.pitts AT cl.cam.ac.uk>
> > Sent: Sunday, January 10, 2010 3:34 PM
> > Subject: Re: [Agda] Agda with the excluded middle is inconsistent ?
> > > I have been following this thread with interest. What is needed most
> > > is a simple yet expressive (and fixed!) core type theory with an
> > > easily understandable (by users) semantics: we should not have to
> > > "discover" the _logical_ consequences of  an implementation---it's a
> > > bit like saying the meaning of my programming language is given by  
> > > my
> > > compiler.
> > >
> > > The rest of this message is speculation without reference to such a
> > > semantics. :-)
> > >
> > > Personally, my bet is that the version of Agda2 that allows one to
> > > prove that type constructors are injective up to intensional  
> > > equality
> > > is inconsistent, without  the need for any form of excluded middle
> > > postulate.
> > >
> > > I say this not because I think that the injectivity up to  
> > > intensional
> > > equality of type constructors is in itself contradictory---indeed I
> > > believe it is quite a natural property to ask for....so long as the
> > > universe in which the type constructor is valued is sufficiently
> > > large. For example, in the presence of injectivity, allowing Set to
> > > contain a (Set -> Set)-indexed family of mutually distinct names for
> > > the empty set
> > >
> > > data I : (Set -> Set) -> Set where
> > >
> > > seems dangerous because Set is "too small"; whereas allowing it in  
> > > Set1
> > >
> > > data I1 : (Set -> Set) -> Set1 where
> > >
> > > seems uncontentious. So I would advocate applying the same
> > > predicativity/size considerations to (injective) type constructors  
> > > as
> > > Agda currently applies to data constructors. Another example: Agda2
> > > allows
> > >
> > > data J (f : Set -> Set) : Set where
> > >   unit : J f
> > >
> > > almost by accident, since it doesn't allow
> > >
> > > data K : (f : Set -> Set) -> Set where
> > >   unit :  (f : Set -> Set) -> K f
> > >
> > > because of predicativity restrictions on data constructors. I would
> > > prefer to rule out both declarations while still allowing injective
> > > type constructors like
> > >
> > > data J1 (f : Set -> Set) : Set1 where
> > >   unit : J1 f
> > >
> > > or
> > >
> > > data K1 : (f : Set -> Set) -> Set1 where
> > >   unit :  (f : Set -> Set) -> K1 f
> > >
> > > Best wishes,
> > >
> > > Andy
> > Hi, I agree with Andy and I think the injectivity of type  
> > constructors is useful.
> > As long as Andy's idea, or a similar idea, is proven to be  
> > consistent, that can be used in reasoning about heterogeneous  
> > equality.
> > There are two well-known notions of heterogeneous equalitay: JMeq  
> > and eq_dep.
> > The definitions are as follows:
> > Inductive JMeq (A:Set) (a:A) : forall (B : Set), B -> Prop :=
> >   | refljm : JMeq A a A a .
> > Inductive eq_dep (U:Set) (Sig: U -> Set) (x: U) (a: Sig x) : forall  
> > (y : U), Sig y -> Prop :=
> >  | refldep : eq_dep U Sig x a x a .
> > Now, assume that you have the following heterogeneous eqaulities.
> >   (1) JMeq (Vector n) l (Vector m) l'    (2) eq_dep nat Vector n l  
> > m l' From (1), you can get the equation
> >     Vector n = Vector m
> > but, not n = m as you don't have the injectivity of Vector.
> > On the contrary, from (2), you can get the equation
> >     n = m
> > So, without the injectivity of Vector, the equation (1) does not  
> > have the same information as the equation (2).
> > But, the notion of JMeq is more homogeneous, general and convinient  
> > than that of eq_dep.
> > So, if you can enusre that some of your type constructors are  
> > injective, you can freely use JMeq instead of eq_dep for the data  
> > types.
> > Indeed, I have developed a library, called Heq, to support  
> > reasoning about heterogeneous (or, extensional) equality in  
> > Coq ,and going to be officially released in a few days.
> > This library basically supports both the notions of JMeq and  
> > eq_dep, but in a different uniform way.
> > For JMeq, if you add the injectivity of your type constructors to  
> > the database, the proof search engine uses the information.
> > Without the injectivity, the proof search engine does not do  
> > anything useful for JMeq.
> > The reason why I support for JMeq (though the extra code I added  
> > for supporting JMeq is several lines) is that I believed the  
> > injectivity until I find the inconsistency.
> > Anway, if we can somehow add the injectivity of some inductive type  
> > constructors, it is a quite useful thing for reasoning about  
> > heterogeneous equality.
> > Best wishes,
> > Chung-Kil Hur
> > Preuves, Programmes et Systèmes
> > ------------------------------------------------------------------------
> > _______________________________________________
> > Agda mailing list
> > Agda AT lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> http://www.tcs.informatik.uni-muenchen.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda AT lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda