Understanding the core syntax

[skybrian]

I glossed over it at first, but I've realized that I don't understand the core syntax, and in particular how self-dependent function calls work. In A quick recap of self types in kind, I don't understand the desugared example:

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

It seems like here we are defining a new symbol, Nat. Its type is "Type". Is that a reference to something or is it just an unevaluated symbol?

There is a syntax note: "self(x: A) -> B" is a self-forall (self-dependent function type)

But I still don't know how to interpret the code. Is self a keyword, a parameter name, or something else? Is the part in parentheses a lambda parameter? If so, what does P represent and what is the body?

Does a function type have a body and what does it mean? I don't know how to interpret the following two lines, other than they must somehow correspond to two constructors in the base syntax.

What does P(self) do here? It looks like a function application, but I don't know why it's there.

This is supposed to be compiled to "raw lambdas" but I don't think I can parse it well enough even to be certain where the lambdas are. I'm not sure if the definition of 'Nat' is made of lambdas or not.

[rigille]

I think it's best to forget about the type definition at first and focus on how the lambdas look. There are two ways to define a Nat. The first is

Nat.zero: Nat
  (P, z, s) z

a lambda that takes three arguments and returns the second. The other option is

Nat.succ(pred: Nat): Nat
  (P, z, s) s(pred)

which is a lambda that takes three arguments and returns the third one applied to pred. So in any case a natural number is a lambda that takes three arguments. And in the following code

Test: _
  let apply_zero = Nat.zero(?a, ?b, ?c)
  let apply_succ = Nat.succ(Nat.zero)(?d, ?e, ?f)
  "hi"

we would have apply_zero == ?b and apply_succ == ?f(Nat.zero). For instance

Test: _
  let apply_zero = Nat.zero(?a, false, (pred) true)
  let apply_succ = Nat.succ(Nat.zero)(?d, false, (pred) true)
  "hi"

would make apply_zero == false and apply_succ == ((pred) true)(Nat.zero) == true. What about the first parameter? It's never returned, so what is it for? It's called motive and it tells Kind what are the types of the other two parameters. In our example we could fill it like this.

Test: _
  let apply_zero = Nat.zero((n) Bool, false, (pred) true)
  let apply_succ = Nat.succ(Nat.zero)((n) Bool, false, (pred) true)
  "hi"

since we're returning a Bool in both cases. Another way to write this is

Test: _
  let apply_zero =
    case Nat.zero {
      zero: false
      succ: true
    }: Bool
  let apply_succ =
    case Nat.succ(Nat.zero) {
      zero: false
      succ: true
    }: Bool
  "hi"

That's right! A case is just syntax sugar for those function applications. Let's go back to the previous example and add a little twist to it.

Test: _
  let apply_zero = Nat.zero(
    (n) case n {
      zero: Bool
      succ: String
    },
    false,
    (pred) "hello"
  )
  let apply_succ = Nat.succ(Nat.zero)((n) Bool, false, (pred) true)
  "hi"

Now we're using the motive say we'll return a Bool in the zero branch and a String in the succ branch. That's perfectly legal. Let's rewrite a bit more

my_motive(n: Nat): Type
  case n {
    zero: Bool
    succ: String
  }

my_foo(n: Nat): my_motive(n)
  n(
    my_motive,
    false,
    (pred) "hello"
  )

Now we can relate each part of my_foo to the definition of Nat. self refers to n, P refers to my_motive, zero refers to false (which has type my_motive(Nat.zero) == Bool), succ refers to (pred) "hello" (which has type (pred: Nat) -> my_motive(Nat.succ(pred)) == Nat -> String), finally P(self) is the return type of my_foo and that's my_motive(n).

[skybrian]

Okay, I’m starting to understand.

It sounds like a value of an algebraic type that has n constructors will be a function that has n+1 arguments. These arguments are basically callbacks. A case statement is implemented by calling its value, passing in callbacks for what should be done in each case.

In this example, there is a ‘z’ callback which is constant because the zero constructor takes zero arguments, and an ‘s’ callback that takes one argument because the succ constructor takes one argument. This is because a branch in a case statement does a pattern-match against the corresponding constructor. It needs whatever values were passed to the constructor on creation.

The first callback, the ‘motive’, determines the return type of the case statement.

However, it’s unclear to me when the motive will be used?

For example, it seems like the ‘destroy’ function in the example should only be called with a natural number, so only the ‘z’ and ‘s’ callbacks will be used?

Perhaps there is a trick here: you could call destroy(Nat, n) instead of destroy(n) and you get back destroy’s return type?

Is this generally true of Kind functions?

[skybrian]

Also, getting back to my first question about the syntax: since Kind uses currying to implement functions with multiple arguments, can there be ‘self’ parameter corresponding to each argument?

So could you could have a two argument function:

self1(Nat) -> self2(Nat) -> Nat

This function would take two numbers along with self1, a function of two arguments, and self2, a function of one argument.

[rigille]

It sounds like a value of an algebraic type that has n constructors will be a function that has n+1 arguments. These arguments are basically callbacks. A case statement is implemented by calling its value, passing in callbacks for what should be done in each case.

Exactly.

For example, it seems like the ‘destroy’ function in the example should only be called with a natural number, so only the ‘z’ and ‘s’ callbacks will be used?

That's correct. The motive is never used for computation, indeed it's erased at runtime. It's only used for type-checking and it's purpose is to allow each branch to return a value of a different type, like in the my_foo example. The type-checker runs my_motive to determine what the return type should be. That's useful for programming, because it allows you to do anything you could do in a weakly typed language without giving up safety. However it's even more useful for theorem proving.

Consider the double negation example from THEOREMS.md.

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: refl
    false: refl
  }: Bool.not(Bool.not(b)) == b

just like List<Bool> and List<Nat> are different types, so are Equal<Bool>(true, true) (returned in the true branch) and Equal<Bool>(false, false) (returned in the false branch). If both branches were required to return values of the same type you wouldn't be able to prove that theorem. That's one reason why you can't prove interesting theorems in traditional functional programming languages.

[rigille]

as for the syntax

self1(Nat) -> self2(Nat) -> Nat

isn't valid, but

self1(a: Nat) -> self2(b: Nat) -> Nat

is indeed valid. The type of that expression is Type. One example of value with type self1(a: Nat) -> self2(b: Nat) -> Nat is the lambda (x) (y) x + y. The name a in (a: Nat) references the first parameter of what's being typed, in our lambda example that's x. b references y. On the other hand the name self1 refers to the whole term being typed: (x) (y) x+y. self2 refers to (y) x+y. In theory you could have a type that looks like this

self1(a: Nat) -> self2(b: Nat) -> f(self1, a, self2, b)

but I can't think of an example where this would be useful yet.