[Agda] Agda with the excluded middle is inconsistent ?

[Andreas Abel]

Andy,

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

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.  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/