Modules

We don't have a module system yet :pensive:. To use functions from other files, you need to create a file within the same directory (e.g., the root folder of Kindex.

Use

The use statement is a useful feature in the Kind language that allows you to create aliases for functions or data types. It simplifies the usage of specific functions or types in your code. Let's explore its usage with practical examples.

Step 1: Importing Functions with use

The first use of use is to import functions. Suppose you are working with the Data.Nat.succ function and want to import it with a shorter alias, such as Succ, for easier usage in your code. Here's an example:

#![allow(unused)]
fn main() {
use Data.Nat as Succ
}

With this statement, you import the Data.Nat.succ function and associate it with the Succ alias. You can now use Succ instead of Data.Nat.succ to refer to that function.

Step 2: Using Aliases for Data Types

In addition to importing functions, use can also create aliases for specific data types. Suppose you want to create an alias for the Data.Nat type called Nat. Here's an example:

#![allow(unused)]
fn main() {
use Data.Nat as Nat
}

With this statement, you import the Data.Nat type and associate it with the Nat/ alias. You can now use Nat/ to refer to the Nat data type.

Now, let's use the Nat/ alias in a function called Succ:

#![allow(unused)]
fn main() {
Succ (n: Nat/) : Nat/
Succ n = Nat/succ n
}

The Succ function takes a parameter n of type Nat/ and returns a value of the same type . Within the function body, we use the Nat/ alias to invoke the succ function associated with the Nat.

Step 3: Using Aliases in Other Functions

Next, let's explore how aliases can be used in other functions. Consider the Is_equal function, which compares two Bool/ values and returns a Bool/ result:

#![allow(unused)]
fn main() {
Is_equal (b1: Bool/) (b2: Bool/) : Bool/
Is_equal b1 b2 = 
  match Bool/ b1 {
    true  => b2
    false => match b2 {
      true  => Bool/false
      false => Bool/true
    }
  }

}

In this example, we use the Bool/ alias to refer to the Data.Bool type within the match pattern. This makes the code more readable and avoids unnecessary repetition of the full module name.

Step 4: Explaining Aliases with an Additional Example

To further illustrate the use of aliases, let's consider the Add_zero function, which proves that adding zero to a number n results in n using the Equal for propositional equality:

#![allow(unused)]
fn main() {
Add_zero (n: Nat/) : Equal/ (Nat/add 0n n) n
Add_zero n = Equal/refl
}

In this function, we use the Equal/ alias to refer to the Prop.Equal type, which handles propositional equality. With the alias, we declare that the return type of the function is a proof of equality between the expression (Nat/add 0n n) and n. We also use the Equal/refl alias to create a reflexive proof of equality.

Conclusion

The use statement is a powerful tool in the Kind language that allows you to create aliases for functions or data types. It simplifies the usage of functions and types, making the code more readable and concise. With use, you can import functions with shorter aliases and create aliases for specific data types. I hope this tutorial has helped you understand the usage of use in Kind.