A clever definition of the integers

[wkolowski]

I tried to define the integers using smart constructors described in this blog post but in a different way, more akin to the usual definition of the natural numbers.

ZZ : Type
  self(P : ZZ -> Type) ->
  (z : P(zero)) ->
  (s : (prev : ZZ) -> P(succ(prev))) ->
  (p : (next : ZZ) -> P(pred(next))) ->
  P(self)

zero : ZZ
  (P, z, s, p) z

succ (k : ZZ) : ZZ
  case k {
    z: (P, z, s, p) s(zero)
    s: (P, z, s, p) s(k)
    p: k.next
  }
  
pred(k : ZZ) : ZZ
  case k {
    z: (P, z, s, p) p(zero)
    s: k.prev
    p: (P, z, s, p) p(k)
  }

We have three constructors: zero, successor and predecessor, and we want to use smart constructors so that successor and predecessor are inverses. However, I can't get it to work. The hard cases are the successor of a successor and the predecessor of a predecessor. I get the following type error:

ZZ: Type
pred: (k:ZZ) ZZ
succ: (k:ZZ) ZZ
zero: ZZ

Type mismatch.
- Expected: P((P) (z) (s) (p) p(k))
- Detected: P(pred(k))
With context:
- k: ZZ
- k.next: ZZ
- P: (:ZZ) Type
- z: P(zero)
- s: (prev:ZZ) P(succ(prev))
- p: (next:ZZ) P(pred(next))
Inside 'Integer.kind':
  19 |   case k {
  20 |     z: (P, z, s, p) p(zero)
  21 |     s: k.prev
  22 |     p: (P, z, s, p) p(k)
  23 |   }

Type mismatch.
- Expected: P((P) (z) (s) (p) s(k))
- Detected: P(succ(k))
With context:
- k: ZZ
- k.prev: ZZ
- P: (:ZZ) Type
- z: P(zero)
- s: (prev:ZZ) P(succ(prev))
- p: (next:ZZ) P(pred(next))
Inside 'Integer.kind':
  11 | succ (k : ZZ) : ZZ
  12 |   case k {
  13 |     z: (P, z, s, p) s(zero)
  14 |     s: (P, z, s, p) s(k)
  15 |     p: k.next
  16 |   }

Any ideas as to whether such recursive smart constructors are even possible, or is it just me doing something wrong?

[rigille]

You're on the right path, this was discussed in the telegram group recently while @MaiaVictor was trying to implement rationals. Whether this is possible or not is an open problem.