[TYPES] what does a negative proposition represent in type theory?

[Noam Zeilberger]

Hello Giuseppe,

On Sun, May 23, 2010 at 5:19 PM, Giuseppe Castagna <gc at pps.jussieu.fr> wrote:
> Le 21/05/2010 23:25, Noam Zeilberger a écrit :
>> Well yes you're right that there are other interpretations of negation
>> -- I wasn't sure what you were looking for!  With this clarification,
>> I think the question you are asking is really at the "extrinsic" or
>> "refinement type" level (related to intersection and union types,
>> etc.).
>> [...]
> Or, you can take the "semantic subtyping" setting where types are set of
> values, and union, intersection, containement *and* negationtypes  are
> interpreted set-theoretically.

Yes, I meant "extrinsic" in the general sense, which includes settings
like semantic subtyping.  The terminology is from Reynolds, and is
roughly what people sometimes call the "Curry view", opposed to the
"Church view".  In "The Meaning of Types: From Intrinsic to Extrinsic
Semantics" he writes:

  In an _intrinsic semantics_, only phrases that satisfy typing
judgements have meanings. Indeed, meanings are assigned to the typing
judgements, rather than to the phrases themselves, so that a phrase
that satisfies several judgements will have several meanings.
  [...]
  In contrast, in an _extrinsic semantics_, the meaning of each phrase
is the same as it would be in a untyped language, regardless of its
typing properties. In this view, a typing judgement is an assertion
that the meaning of a phrase possesses some property.

The extrinsic view is not incompatible with the intrinsic view -- it
can be seen as a refinement, adding another layer of "semantic types"
or "refinement types" to an already intrinsically-typed language.  So
with Xuhui's example, we can consider "is prime" as a property of
untyped values, or more precisely of intrinsically-typed natural
numbers -- both approaches make sense, but with the latter when we
take the complement property we get the slightly more manageable set
of non-prime naturals, rather than the set of non-prime naturals
together with all untyped values which are not natural numbers (of
course we could cut down the latter by intersection with the property
"is natural").

But in any case, my point was just that Xuhui's question was a bit
confusing, but makes sense theoretically under the view of
types-as-properties.  (This is brushing aside important questions such
as, Does it make sense to negate *any* property?, and How do you
design a decidable type system with complementation?)

Noam