Data types with Negation

Sunday 15th January 2023

Back in April and June last year, at MSFP and at TYPES, I gave talks about some work I've done on trying to understand what it would mean to allow negation in data type definitions.

The gist of the talk is: what if we could define a predicate for even numbers like this in Agda (or Coq or Idris or Lean):

data Even : Nat → Set where
  zero : Even 0
  suc  : ∀ {n} → not (Even n) → Even (suc n)

So 0 is even, and suc n is even if n isn't.

But if we get this to work, then what would this declaration mean?

data Liar : Set where
  liar : not Liar → Liar

I think that data types with negation will be useful for describing the sequences of decisions taken by back tracking algorithms. For example, a PEG parser's ordered choice A / B means “try A, and if that doesn't work try B”. We need some kind of negation to capture the meaning of “if that doesn't work”.

The solution I have at the moment is a proof relevant version of the well founded semantics of logic programs with negation, which is related to the stable model semantics used in Answer Set Programming. The key step is to replace the 3-valued logic used in the well founded semantics with Chu spaces.

I'm still working out the best way to present the theory, and what reasoning principles these data types have, but these slides are the best presentation I have so far.