[Agda] Agda with the excluded middle is inconsistent ?

[Chung Kil Hur]

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