What types can be written in Kind but not Lean?

Question

The Kind programming language has a sufficiently powerful type system to support proving theorems like in Lean, Coq, Idris, or Agda. I've seen it said that Kind has an even more powerful type system that goes beyond what these other languages support. Since Kind is a work-in-progress, I've struggled to find documentation. In one blog post, they say:

Self-types can be described briefly. The dependent function type, ∀ (x : A) -> B(x) allows the type returned by a function call, f(x), to depend on the value of the argument, x. The self-dependent function type, ∀ f(x : A) -> B(f,x) allows the type returned by a function call, f(x), to also depend on the value of the function, f. That is sufficient to encode all the inductive datatypes and proofs present in traditional proof languages, as well as many other things.

Later, that blog post gives an 'expanded' version of an inductive type representing the natural numbers:

// Natural numbers                            
Nat: Type
  self(P: Nat -> Type) ->
  (zero: P(Nat.zero)) ->
  (succ: (pred: Nat) -> P(Nat.succ(pred))) ->
  P(self)

However, I do not understand this self notation so the example is unenlightening.

The basic description that in Kind, the type of the result of a function can depend upon the value of the result of the function is interesting. I can picture one form of this in Lean and similar type systems, where the function returns a Sigma type, so that the type of the result's second part can depend upon the result's first part.

What are concrete, simple examples of types that can only be expressed using these self-types? What are concrete, simple examples of a value of those types?

My attempt at answering this: I can maybe imagine that a function f has type ∀ x: Nat -> (f(x) == f(x)), but I can't imagine how you could make a value of this type. Can this example type be written in Kind? Are there any values of that type?

Answer 1

I'm by no means an expert (never heard of Kind until this post), but I'll give this a shot. I mostly want to explain my intuition of the first example from the given blog post (which is covered in depth in the paper linked in the comments) in a bit more space. So not exactly an answer, but hopefully in the right direction.

First observation: we can write $\lambda$-encodings of pairs in the nondependent setting fairly straightforwardly. In Agda:

NatPair : Set₁
NatPair = (c : Set) → (ℕ → ℕ → c) → c

mkNatPair : ℕ → ℕ → NatPair
mkNatPair x y _ f = f x y

With this encoding, our constructor is not an atomic term, but a regular function, so we can instead define the constructor to pre-normalize our terms if we want to think of these pairs are integers.

Int : Set₁
Int = (c : Set) → (ℕ → ℕ → c) → c

mkInt : (x y : ℕ) → Int
mkInt pos zero _ f = f pos zero
mkInt zero neg _ f = f zero neg
mkInt (suc pos) (suc neg) = mkInt pos neg

test : mkInt 5 3 ≡ mkInt 3 1
test = refl

The problem occurs exactly when we try to generalize this to the dependent setting. If we tried to do this naively in Agda, it might look a bit like

mutual
  {-# TERMINATING #-} -- since we can't actually write Int in our type
  Int : Set₁
  Int = (p : Int → Set) → ((x y : ℕ) → p (mkInt x y)) → ⊥ -- a placeholder

  mkInt : (x y : ℕ) → Int
  mkInt x y p f = ?

The question is: what do we want $\bot$ to be? Since we're encoding integers essentially by an induction principle, we want it to be p applied to whatever it is that I'm trying to say is of type Int. This is why we need self to refer to whatever thing I am trying to type as an Int.

So in Kind, when we write

Int: Type
  self(P: Int -> Type) ->
  (prf: (pos:Nat) -> (neg:Nat) -> P(Int.new(pos,neg))) ->
  P(self)

Int.new(pos: Nat, neg: Nat): Int
  (P, prf) prf(pos, neg)

self refers to the thing of type Int you are currently looking at, and this might be read as: a term is of type Int if, given a property on Ints, and a proof that the property holds for all Ints, the property holds on this Int.

Once we have this, we can do exactly what we did in the above example, but in the dependent setting (as is done in the blog post). Hope this helps.