Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent


chronological Thread 
  • From: Noam Zeilberger <noam.zeilberger AT gmail.com>
  • To: Andreas Abel <andreas.abel AT ifi.lmu.de>
  • Cc: Thorsten Altenkirch <txa AT cs.nott.ac.uk>, Chung Kil Hur <Chung-Kil.Hur AT pps.jussieu.fr>, coq-club AT inria.fr, Agda mailing list <agda AT lists.chalmers.se>
  • Subject: [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent
  • Date: Thu, 7 Jan 2010 22:19:16 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=v6ALD9wEJNphtGV/gz8MRqI/vYMjT5OmNO7xTOnhJzAgZfkbPghzPKQo+rD0Am4X6V 2o8oXkHIONLoLRzbnheEeLCdsmaAj3Tw6QaRivKEXFIb1AegTWy+aegP109MYGbYLG7a FVav5T0efpExf/3t0PIbLiXUdWZEaFU9rKYJA=
  • Resent-date: Tue, 19 Jan 2010 15:51:39 +0100
  • Resent-date: Tue, 19 Jan 2010 15:51:39 +0100
  • Resent-from: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • Resent-message-id: <20100119145139.GE17061 AT pirogue.inria.fr>
  • Resent-to: coq-club AT inria.fr

On Thu, Jan 7, 2010 at 6:17 PM, Andreas Abel 
<andreas.abel AT ifi.lmu.de>
 wrote:
> For a pragmatic solution, I suggest to consider the problem of injective
> type constructors in a simply-typed setting and then extrapolate to a
> dependently typed setting.

In SML, as in Agda, datatype *constructors* are injective, type
*definitions* are not.  Here is an example:

type 'a ninja = unit            (* non-injective type definition *)
datatype 'a inja = Foo of unit  (* injective datatype constructor *)

(* bar1 and bar2 restrict the type argument of ninja and inja *)
fun bar1 (_ : bool ninja) = 0
fun bar2 (_ : bool inja) = 0

(* now, t1 will obviously type check... *)
val t1 = bar1 (() : bool ninja)
(* but so will t2, by expanding the definition of "int nina" ... *)
val t2 = bar1 (() : int ninja)

(* likewise, t3 wil obviously type check... *)
val t3 = bar2 (Foo() : bool inja)
(* but t4 does not! *)
val t4  = bar2 (Foo() : int inja)

(* Error: operator and operand don't agree [tycon mismatch]
  operator domain: bool inja
  operand:         int inja
  in expression:
    bar2 (Foo (): int inja) *)




Archive powered by MhonArc 2.6.16.

Top of Page