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?