The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Benjamin Pierce wrote:
> If you add to the simply typed lambda-calculus a type Dynamic with an 
> introduction rule analogous to your constructor plus a 'typecase' 
> construct for eliminating Dynamics, you can write non-terminating 
> programs.  But it's not clear to me whether injectivity gives you that 
> much power.

Indeed, I'm using this type to model Turing-complete programming 
languages, and it's clear that any "computational" way of getting at the 
contents of a dynamic package can't work.  But the theorem I'm asking 
about is in Prop, so we know it can never affect computations in Set or 
(non-Prop) Type, which gives me some hope that it might be a consistent 
axiom.


> > > On Mon, Jun 9, 2008 at 3:37 PM, Adam Chlipala <adamc AT hcoop.net 
> > > <mailto:adamc AT hcoop.net>> wrote:
> > >
> > >     Does anyone know if it would be consistent with (impredicative
> > >     Set) CIC to assert the injectivity of the [Dyn] constructor below
> > >     as an axiom?
> > >
> > >     Inductive dynamic : Set :=
> > >      | Dyn : forall T, T -> dynamic.