How to encode the Int type with algebraic datatypes in a pure functional language like Kind-Lang?

A simple way to encode an Int type would be to make a pair of a Nat and a sign. For example:

Int: Type
  Pair<Bool, Nat>

There is a problem with that definition, though: it includes two zeros (-0 and +0), so, in order to have an isomorphism to the conventional Int set, we need to consider the number to be incremented by 1 when the sign is negative. So, for example, {false, 2} represents -3, {false, 3} represents -4, and so on.

Agda uses a similar encoding, which instead of a Bool, has a constructor for each sign. We can port it as:

// Int.pos(n) represents +n
// Int.neg(n) represents -(n + 1)
type Int {
  pos(n: Nat)
  neg(n: Nat)
}

Both representations work, but using them to write algorithms and prove theorems is complex and error-prone. For example, here is add for Int:

Int.negate(a: Int): Int
  case a {
    pos: case a.nat {
      zero: Int.pos(Nat.zero)
      succ: Int.neg(a.nat.pred)
    }
    neg: Int.pos(Nat.succ(a.nat))
  }

Int.add(a: Int, b: Int): Int
  case a b {
    pos pos: Int.pos(Nat.add(a.nat, b.nat))
    neg neg: Int.neg(Nat.succ(Nat.add(a.nat, b.nat)))
    pos neg: if b.nat <? a.nat
      then Int.pos((a.nat - b.nat) - 1)
      else Int.neg(b.nat - a.nat)
    neg pos: Int.add(Int.pos(b.nat), Int.neg(a.nat))
  }

A better alternative, often used in cubical languages, is to represent Int as a quotient. So, for example, in Agda, we can write this:

data Int : Set where
  mkInt : (pos neg : Nat) -> Int
  canon : (pos neg : Nat) -> mkInt (suc pos) (suc neg) = mkInt pos neg

This way, we represent integers as a pair of two nats, and the integer is represented by the first natural number subtracting the second natural number. So, for example, mkInt 5 2 represents 3, and mkInt 2 5 represents -3. The problem with this encoding is that it has many ways to represent the same Int. For example, 2 can be represented as mkInt 2 0, mkInt 3 1, mkInt 4 2 and so on. As such, this type wouldn't be isomorphic to integers. Thanks to the second argument, though, it is, as we extend the set with a quotient that identifies identical terms.

In Kind, we don't have direct quotients, but, as a consequence of Self encodings being used to represent datatypes under the hoods, we are able to build constructors that compute, or smart-constructors. These constructors are like conventional constructors, except that, under some conditions, they aren't "stuck". Instead, the compute to reach a canonical form. That way, we can encode the Int type in a similar way to the encoding above, plus a rule that causes mkInt (succ i) (succ j) reduce to mkInt i j, until one size is zero. So, we could write:

type Int {
  new(pos: Nat, neg: Nat) with {
    zero zero: new(zero, zero)             // stuck, thus canonical
    zero succ: new(zero, succ(neg.pred))   // stuck, thus canonical
    succ zero: new(succ(pos.pred), zero)   // stuck, thus canonical
    succ succ: Int.new(pos.pred, neg.pred) // non-stuck, thus computes
  }
}

Sadly, the syntax above isn't implemented in Kind yet, but we can build Int (and similar types) directly by manually writing their self encodings:

Int: Type
  int<P: Int -> Type> ->
  (new: (pos: Nat) -> (neg: Nat) -> P(Int.new(pos, neg))) ->
  P(int)

Int.new(pos: Nat, neg: Nat): Int
  (P, new)
  case pos {
    zero: new(Nat.zero, neg)                     
    succ: case neg {
      zero: new(Nat.succ(pos.pred), Nat.zero)
      succ: Int.new(pos.pred, neg.pred)(P, new)
    }!
  }: P(Int.new(pos, neg))

This definition works and allow us to have much simpler algorithms and proofs. For example, here is Int.add for this new type:

Nat.add(n: Nat, m: Nat): Nat
  case n {
    zero: m
    succ: Nat.succ(Nat.add(n.pred, m))
  }

Int.add(a: Int, b: Int): Int
  open a
  open b
  Int.new(Nat.add(a.pos, b.pos), Nat.add(a.neg, b.neg))

Note it just reuses Nat.add. Compared to quotients, proofs on this Int are even simpler, since mkInt 3 1 and mkInt 2 0 become equal by definition.

two_is_two: mkInt 3 1 == mkInt 2 0
  refl