coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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) *)
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, (continued)
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Dan Doel
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
David Wahlstedt
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent,
Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Thorsten Altenkirch
- [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent, Noam Zeilberger
Archive powered by MhonArc 2.6.16.