4
$\begingroup$

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?

$\endgroup$
6
  • $\begingroup$ Can you point to some sort of a relatively complete description of Kind, or provide a description of its capabilities that situates it in the design space of possible type theories? Or to put it another way: is this a question about self-types or about Kind specifically? $\endgroup$ Jan 5, 2023 at 8:44
  • $\begingroup$ I don't know! My knowledge of this topic is basically limited to trying to read that linked blog post (and knowing some dependent type theory via Lean). Unfortunately "self-type" is hard to google and I'm not up with the literature. I'm not interested in Kind per se except that it's the only place I've seen this idea. If you can answer this question in another notation, that would be appreciated. Maybe I'm really just looking for an intro to self-types that compares it concretely to dependent types? $\endgroup$
    – user32157
    Jan 5, 2023 at 11:24
  • $\begingroup$ This sounds like a good question for the Kind developers. I don't know if any of them hang around here. $\endgroup$
    – Max New
    Jan 5, 2023 at 13:27
  • $\begingroup$ Are you looking for something in particular beyond the examples given in the blog post? I think the first example of smart constructors for Ints given there is pretty nice. $\endgroup$
    – Nathan
    Jan 5, 2023 at 19:48
  • 3
    $\begingroup$ It looks a bit related to Cedille. Also, have a look at Self Types for Dependently Typed Lambda Encodings by Aaron Stump, where the idea of self-types originates from (as far as I know). $\endgroup$ Jan 5, 2023 at 21:52

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thank you for this much more complete example! I'm still uncertain whether this cannot actually be expressed in dependent types. I don't know Agda so apologies for the pseudocode, but what about Int = (p: Int -> Set) -> ((x y : N) -> p (mkInt x y)) -> (Σ n: Int, p n)? I.e. we smuggle the thing of type Int as the first output of the function and let the second output's type depend upon that. Then mkInt is maybe something like mkInt x y p f = ((mkInt x y p f), f x y) ? I guess the infinite recursion in the fist argument is what makes this a no-go? $\endgroup$
    – user32157
    Jan 6, 2023 at 22:11
  • 1
    $\begingroup$ I think the bigger issue is the reference to Int in the definition of Int, which isn't allowed in most systems. If you take a look at the paper linked in the comments, you get around this by noting that those references to Int is erasable when all is said and done. You can, for example, do what you've written above assuming you've defined an pairs, but it doesn't exactly capture the idea of the Int, and is to me, morally equivalent to writing a sort of wrapper constructor, which is also perfectly possible. Maybe I'll update my answer when I have time to include these solutions. $\endgroup$
    – Nathan
    Jan 7, 2023 at 19:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.