[Agda] Agda with the excluded middle is inconsistent ?

[Thorsten Altenkirch]

> 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