Logic in Kind

In the previous chapters, we saw many examples of factual statements (propositions) and ways to present evidence of their truth (proofs). In particular, we extensively worked with equality propositions in the form e1 = e2, implications (p -> q), and quantified propositions (x -> P(x)). In this chapter, we will see how Kind can be used to perform other familiar forms of logical reasoning.

Before diving into the details, let's talk a little about the status of mathematical statements in Kind. Remember that Kind is a typed language, which means that every meaningful expression in its world has an associated type. Logical statements are no exception: any statement we try to prove in Kind has a type, namely Type, the type of propositions. We can see this with the type Boolean:

Bool: Type
Bool.true  : Bool
Bool.false : Bool

In the Bool type we have Bool.true and Bool.false. To create the Bool type, we declare that it is a type (Type) and then that Bool.true and Bool.false are of type Bool. Seeing how it is done, it becomes much simpler. We are often intimidated by the "functional" name, but Kind is a very friendly language, we will see more about this later on.

Another possible example is Nat, the natural numbers. Natural numbers are all non-negative integers. That is, they start with the number zero and go to infinity, but do not have decimal values. Therefore, 3 is a natural number, but 3.14 is not, just as -3 is not. So we know that the natural number is made up of zero and its successors. Let's see how this is in Kind:

Nat: Type
Nat.zero             : Nat
Nat.succ (pred: Nat) : Nat

We notice that the construction is similar to Booleans, but there is an extra element in Nat.succ, which is "(pred: Nat)", and this is because, while in the other we had only two return options (True or False), now we have an infinity of numbers that the code needs to understand, and there must be a way for the code to stop running (we will see more about this throughout this study), since code that never stops running is code that will never give us the result.

However, in any case, we notice that the structure of Nat is basically the same as Bool, which shows us that we can create any type, as long as we follow the same structure. Let's create the juice type:

Juice : Type
Juice.laranja : Juice
Juice.caju    : Juice

Orange juice has two constructors, Juice.laranja and Juice.caju. This type is fictitious, it did not exist until now, but now we can use it as a type and this shows us that, thanks to Kind's design, we can create an infinity of types, since every type is a function.

Understanding the construction of types will prevent some syntax errors from occurring.

to review, our element Juice is of type Type and Juice.orange is of type Juice. Thus, in layman's terms, the element is to the right of the colon and the type is to the left:

element : Type

As previously mentioned, even types are functions, so we can have a function as a type. For example:

Problem : Equal Bool Bool.true Bool.true

We can see that we have an element called "Problem" and it is of type "(Equal Bool Bool.true Bool.true)". We have seen this structure several times in the past chapters, and it is now easy to understand that this function is a type and, just as we don't write it, we cannot simply copy the function to the constructors of this type.

Suco: Type
Suco.laranja : Type

Juice is of type Type, but Juice.orange is not of type Type, it is of type Juice.

But be aware that all syntactically well-formed propositions have type Type in Kind, regardless of whether they are true or not. Simply being a proposition is one thing; being demonstrable is another thing!

In fact, propositions do not just have types: they are first-class objects that can be manipulated in the same way as other entities in the world of Kind. So far, we have seen a primary location where propositions can appear: in the type signatures of functions.

Plus_2_2_is_4 : Equal (Plus 2n 2n) 4n
Plus_2_2_is_4 = Equal.refl

But propositions can be used in many other ways. For example, we can give a name to a proposition as a value in its own right, just as we gave names to expressions of other types.

Plus_fact : Type
Plus_fact = Equal (Plus 2n 2n) 4n

Later, we can use this name in any situation where a proposition is expected - for example, in a function declaration.

Plus_fact_is_true : Plus_fact
Plus_fact_is_true = Equal.refl

We can also write parameterized propositions - that is, functions that take arguments of some type and return a proposition. For example, the following function takes a number and returns a proposition asserting that this number is equal to three:

Is_three (n: Nat) : Type
Is_three n = Equal Nat n 3n

In Kind, functions that return propositions are said to define properties of their arguments. For example, here is a (polymorphic) property that defines the familiar notion of an injective function:

Injective <a> <b> (f: a -> b) : Type
Injective a b f = (x: a) -> (y: a) -> (e: Equal b (f x) (f y)) -> (Equal a x y)

We can instantiate a rule of injectivity with

Nat.succ_injective : Injective ((x: Nat) => Nat.succ x)
Nat.succ_injective =
  (a: Nat) =>
  (b: Nat) =>
  (e: Equal Nat (Nat.succ a) (Nat.succ b)) =>
  Equal.apply (x => Nat.pred x) e