A Kind Welcome

To an efficient, minimal, and practical language, that aims to rethink functional programming from the scratch, with a modern and consistent design.

The goal of this documentation is to be as simple as it is to learn Kind. Therefore, we decided to adopt a minimalist and simple design, so you can promptly find what you need.

Fast navigation index

About Kind

Kind aims to be more practical and conventional-like as a language. It is statically typed, and its types are so powerful that you can even prove mathematical theorems with them.

A possible description for Kind is to imagine it as the Universe when you try to capture an image of it from the outside. When you create a new file in Kind, it's like the whole Universe is there except the piece you're looking for is not specified.

Ok, it is weird to think about the universe from the outside, it can get a bit confusing, so let's use a little story to better understand it:

We are Astronauts, Kind Astronauts. One day, in this fruitful little exploration, our spaceship comes across a planet that already has a name: "Boolean Logics". In this planet, we discover the functions "AND", "NOT" and "OR", and then decide to formally prove those beings. With all proved and documented, we have a hard time finding another Boolean logic function. Therefore, by thinking "our job is done", we jump back into the Kind Spaceship to look for new planets to explore.

Nonetheless, a few days later there are news all over the universe, people are talking about other new types of functions discovered in planet Boolean Logics: "XOR", "NAND" and "XNOR". Just before our departure from the planet, another Kind astronaut arrived there and encountered those new functions.

Even with all the work, we couldn't find those functions the other astronaut did. But they were there. So, just because a function has not been discovered yet, it doesn't mean that it didn't exist before.

Above, the Boolean Type is used to better elucidate our example. It is like a planet in our Universe, and its Definitions and Functions are the Biome and Ecosystem from the planet.

This Kind Universe is as big as your imagination, in fact, it is probably bigger than that. There are endless planets, ecosystems and biomes to explore. With that in mind, would you like to become a Kind Astronaut and embark in this fun (and not that perilous) adventure with many other astronauts?

If you don't like the idea of exploring the Universe, it's okay, we could use another analogy, a shorter and easy one. Just imagine Kind Lang as a Book Recipe, an empty one, with an endless amount of ingredients, and as long as you can find recipes you can write in the recipe book for other people to use.

Learning Kind Basics

A quick guide for new recruits.

If this is your first time studying Kind, it may take some time to get used with its syntax and other details. So, before exploring this vast Universe, take a look in these eight topics:

They are necessary to better understand deeper contexts as we proceed towards our goal. After some preparation to start the journey, you'll have a first contact with the basic about Functions and how to build some of them, Boolean Logics, working with Bool types and constructors.

This learning method was tested before with many other Kind Astronaut Recruits, generating data about the best outcome and learning curve. Hoping that you feel comfortable with this approach, welcome to Kind Basics!

Terminal

The exploration is not terminating, we are just getting started.

If you already know how to work with terminals, skip to the Installation step.

What is a Terminal

A terminal can be described as an interface for users to communicate with the computer.

They are our command-line interface, a place where we type commands and the computer process it.

Let's open our terminal:

Opening the terminal on Linux

TODO

Opening the terminal on Windows (WSL2)

TODO

Opening the terminal on MacOS

TODO

Opening the terminal on Windows

TODO

if you are using Linux or Windows your terminal would probably look like this:

If you are using MacOS your terminal would probably like this:

You can customize your terminal the way you want and feel most comfortable with.

Command-lines in a terminal follow a "left to right" hierarchy, the left side always come first and the computer interprets them in this order.

Before explaining terminal commands to you, there is a very important command that you need to understand, the sudo command. sudo is the abbreviation of "super user do" that, when used, allows a user to get privileges of another user (usually the super user) to securely perform specific tasks within the system in a administrator controllable manner. You will need to use the sudo command in a lot of cases.

Terminal Commands

When double clicking a folder in order to open it, your computer basically understand and does the cd folder command; the same happens when renaming a file, the computer will understand it as using the command mv oldfilename.kind2 newfilename.kind2.

The terminal is simply a command line where you type those commands directly to your computer. As this is extensively used in this guide book, it is recommended that you get familiar with this by playing with the commands below (just be careful with some of them, like rm).

For now, let's take a look at a few of the most used terminal commands. Even though everything that is used in this guide will be explained, if you want to dive deeper into terminal commands, look up to this this link.

List of Commands

cd
ls
mkdir
rm
mv
touch
clear
  • The command cd stands for "Change Directory", and it navigates through them.
Command                Description
cdHome: Goes back to your base folder (main folder).
cd ..Back: Moves to the previous folder.
cd 'folderName'Through Files: Will take you to that folder specified.
  • The command ls stands for "List Files", and lists the content of the current folder.
Command                Description
lsListing: Will show you a list of the files and folders
in the current folder that you are in.
ls -laDeeper Listing: Will show a more detailed version of
the ls command, with it's hidden files or folders.
  • The command mkdir , that stands for "Make Directory", creates a new folder.
Command              Description
mkdir folderNameCreating: Works by creating a folder with the specified
name. For example:
mkdir exampleFolder creates it with the name
"exampleFolder"
  • The command rm stands for "Remove", and removes the specified file or folder.
Command                Description
rm fileNameRemoving Files: Removes the file specified in it.
rm -r folderNameRemoving Folders: Removes a folder in the same way
as mkdir creates it, you need to specify which
folder you want to remove.
    • This command is VERY DANGEROUS! If possible, DO NOT USE IT, there are a lot of memes on the internet from people using rm to delete important folders. Avoid everything that has the rm command on internet, otherwise, use it by your own discretion and responsibility!

  • The command mvstands for "Move", and has two functionalities, to move and rename files or folders.

CommandDescription
mv fileName /folderNameMoving things: Using command moves the fileName
file to the folderName folder. In order for this command
to work, it is needed to write the file name
followed by the name of the directory that you want to
send the file to. For example:
mv kindFile.kind2 /newDirectory to move a file to a
folder inside the current folder.
mv kindFile.kind2 ../folderName to take a file to a
folder in a previous folder by using "../" before the name
of the folder.
mv oldFileName newFileNameRenaming things: The command changes the name of a
file or folder to the name specified in the second
parameter. For example:
mv oldName.kind2 newName.kind2 to rename a file from
"oldName.kind2" to "newName.kind2".
mv oldKindFolder newKindFolder to rename a folder
from "oldKindFolder" to "newKindFolder".
  • The command touch can do a couple of complicated things, such as update file access and it's modification time. But, right now we are only gonna use it to create new files.
Command                Description
touchCreating Flies: The command creates (if this file do
not exists yet) a new file. For example:
touch newfile.kind2 will create a .kind2 file with the
specified name.
  • The command clear will clear your command line.
Command                Description
clearCleaning up the mess: The command will clear the
command line window. Use it when your terminal is
just a giant text wall and you will have a fresh new
terminal. It's very refreshing,
trust me!.

The command will clear the command line window. Use it when your terminal is just a giant text wall and you will have a fresh new terminal. It's very refreshing, trust me!

With this basic commands, proceed to the Kind Installation, as we are using the terminal to do so. If you already have Kind installed in your computer, proceed to the section Text Editors.

Installation

Prepare your spaceship carefully.

This guide teaches how to download and install Kind through Rust, using Cargo, a tool used for managing packages. It may be necessary to have an internet connection to proceed with this guide.

First, install Rust using this link.

  • Currently, Cargo is the only way to install Kind.
  • This guide was written when Kind was in the beta version, so it is necessary to install the nightly channel version.

Linux or MacOS

Use your package manager (Cargo) to install Kind. To do so, open the terminal and type the following code:

cargo +nightly install kind2

Windows

For Windows users, it is possible to use Kind through CMD or WSL2. If you choose WSL, the installation method is in this link.

Use your package manager (Cargo) to install Kind. To do so, open Bash (WSL2) or Terminal (CMD) and type the following command:

cargo +nightly install kind2

Cloning the Kind Repository - Method 1

Clone the Kind repository using the "git clone" command, as follows:

git clone https://github.com/HigherOrderCO/Kind

After the cloning step, use the following command for installation:

cargo +nightly install --path crates/kind-cli --force

Cloning the Kind Repository - Method 2

Cargo allows you to install using git, without the need to clone any repository, as follows:

cargo +nightly install --git https://github.com/HigherOrderCO/Kind.git

By following the above steps, we can start using Kind.

Now, let's proceed to Text Editors and finish preparing our spaceship for exploration.

Text Editors

For the VVim!

  • If you already know what a Text Editor is, and already has your own favorite, proceed to the Hello Kind! section. Otherwise, this page will be very helpful.

What is a Text Editor?

It is basically a type of computer software that edits pain text.

When having the first contact with codes and program skills, skimming through different types of programming languages on the internet is very easy. But something may be missing there, so you start to ask yourself things like "How am i going to code?" and "Where am I going to write those codes?". And it probably is not clear yet. So this guide will try to help you in each and every step of this journey. Coding is meant to be fun, seriously!

First things first, before thinking about which programming language you want to learn (Probably, since you are here, that language is Kind) let's think about which Text Editor to use.

There are actually a lot of them, each one has it's own pros and cons, and probably the best way to choose is by testing them. In This blog, there are 13 different types of Text Editors to look.

But, if you don't want to spend too much time searching an "ideal Text Editor", it is strongly recommend you to start with Visual Studio Code. "VS Code" is the most popular text editor with the most integrations and syntax highlighting extensions that you can find out there. It's fairly simple to use, and there's a lot of tutorials on "how to use it better" on the internet.

Even so, this is just a recommendation, fell free to choose and use anyone of them.

Now that we have picked our text editor, let's start coding. And as usual, start by doing a Hello Kind!.

Hello Kind

This is definitely not another "Hello World!" guide. Or is it?

By this point, Kind should already be installed in your machine. If not, please go back to Installation and move along with the instructions.

You are not sure Kind is correctly installed? Try proceeding with this guide, if it doesn't work, well... it's not installed. If it worked, then you're ready to learn how to become a PRO GAMER Kind programmer!~

In this guide, command lines and text editors will be used, so make sure the terminal is open to proceed through the steps. Don't know what is a Terminal and Text Editor? So go back to Terminal guide and Text Editors.

Creating the documents

First of all, create a directory to store the Kind files. It is recommended to use a dedicated directory to keep all the exercises and examples, but feel free to do as you want.

The three commands below will create a directory called 'KindExamples' and a file called 'hello_world.kind2' inside the project directory. Use them in order:

//Making a directory
mkdir KindExamples

//Moving through directories
cd    KindExamples

//Making a file
touch hello_world.kind2  ////CMD use "copy nul hello_world.kind2 > nul"

The .kind2 extension is what makes it a Kind file. For example, a file that ends with .exe is an Executable; .js is a JavaScript file; .rs is a Rust file, etc.

If the commands were used correctly, the file hello_world.kind2 should be inside the folder KindExamples. Then it's time for fun, CODING!

Hello World

Open the hello_world.kind2 file on the Text Editors, it is going to be empty, but no worries, remember our little story in About Kind about exploring a Universe? This is just your first exploration.

  • Starting now, there are going to be some advanced concepts. But don't be scared, everything will make sense in the future, ethoses concepts that are pertinent will be explained in it's given time.
  • It is recommended that you manually type the codes, instead of copy pasting them in your file.

Let's write your first code into the hello_world.kind2 file:

//hello_world.kind2
Main {
  "Hello, Kind!"
}

And that's it! That's how a Kind "Hello World!" is written. A print function in four lines.

Type Checking

With the code ready, you should use the Type Check to see if everything is in order. The Type Checker is unknown until now in this guide, but will be explained further. Right now, simply understand it as a verifier that checks if the file is correctly typed and "typed" (haha!).

To Type Check a Kind file, just use the command Kind fileName.kind2. For the hello_world.kind2 file it would be:

//Terminal
kind2 check hello_world.kind2

The message "All terms check." means your file is ready!

//Terminal
All terms check.

The Type Check is ok? Then let's run the code.

Running the code

To Run a file in Kind, use the command kind2 run nomeDoArquivo.kind. Yes, the fileName goes without the extension in this case. It should look like this:

//Terminal
kind2 run hello_world.kind2

And voila! your terminal should print Hello, Kind! back to you.

Just remember every steps above, Type Check it then run!

//Terminal
"Hello, Kind!"

With that you've finished your first exploration and may call yourself a Kind Astronaut, congratulations! Welcome to the Kind programming world!

In this first mission you explored your first ecosystem, discovered.

You just explored your first ecosystem and discovered your first function. The next section will go deeper into the Kind Basics.

Kind Basics

Types, Functions and Theorems are the fundamentals of Kind.

The basics of Kind language are:

  • Types
  • Functions
  • Theorems

But first, let's take a look and get comfortable with the first two. Theorems is a more complicated subject and will be explained later in this book.

By working with basic functions and types in this segment, you'll know and have a better understating of the Kind syntax and how it works.

Comments

Throughout this book, you will notice that sometimes there is a "double slash" // followed by a code or a text. This double slash is used to tell the compiler that EVERYTHING that comes after it, in that specific line, will be seen as a comment. So the compiler does not read those comments.

Comments are generally used to describe the functionality of a function, but you can use it to write whatever you want in how many lines you desire as long as you remember to use "//" in each line.

For example:

//comments.kind2

This is not a comment.

//This is a comment.
 
This code works. // Anything after the double slash, doesn't work anymore.

//This code doesn't work // Neither does this one

This code works. // This code doesn't // Neither does this // Or this

This works too //

So, when you see a // just know that it is a commented code, and everything to the right of the it will not be interpreted by the compiler.

Now that you, fellow Kind Astronaut, know went through all this preparation, our journey has everything to begin!

Let's start by learning what are these so called "Types".

"Types of what?! Fruits?" - Recruit nº42.

Basic Types

What you need to know about Types in Kind.

Types, which is short for "Data Types", have an important role in Kind's environment. They provide Kind the information about which type of data it's going to work with. That's why the word "Type" appears a lot throughout this guide.

So, it is extremely important that you get as comfortable as possible using it. Please, read this guide as many times as necessary to fell like an expert in this subject.

What are Types?

A Type is how a group of values is seted. Every value within that group is in the same category. Bellow, types system will be represented as boxes in a visual example that makes it more understandable

---Img---

The easiest way to think about Types is to see them as a group that defines other things. Or, in a way that Astronauts can understand, they are like planets in this Kind Universe.

---Img---

This is how it looks when you define a type in Kind using Bool as an example:

//Bool.kind2

type Bool {  
  true
  false
}

There are basically two things that forms a Type, a name and its Constructors. Let's understand better this syntax:

---Img---

In the first line write type to say it is defining a type, followed by the name of the type. The first letter of this name is always in upper case, unlike type, which is always written in lower case.

---Img---

The curly brackets determines where type definition starts and ends. Everything inside the curly brackets are the constructors of that type, and constructor names must be in lower case as well.

---Img---

It is important to notice that constructos do not have a value unless they are in a function. In other words, inside the Type definition, they don't have it. For example, constructors like "true" and "false", that are from the Bool type, do not hold any meaning by themselves, they are just a name. Only when inside functions it is assigned values to them that defines what is true and what is false.

Note that a Type can hod an uncountable number of constructors:

//example.kind2

type Typename { 
  constructor1
  constructor2
  constructor3
  constructor4
  constr...
}
// "..." meaning continuation

It is very important to name constructors based on what value they will have inside the functions, it improves the readability of the code.

Now that you know Types a little bit better, it's time to dig deeper into what constitutes a type. Let's proceed to Constructors.

- Basic Constructors

What are they building?

Constructor is a short name for "data constructor". Every one of them belongs to a Type and stores a value. It can be used to store values together, but can also store none. In that last case it is called a Nullary Constructor, meaning that they are constants.

Here is an example of Constructors from the Bool Type:

 //Bool.kind2

type Bool { // type's declaration + type name
  true      // first  constructor, named true
  false     // second constructor, named false
}           // end of declaration

In the Boolean type we have two Nullary constructors, true and false, for the sake of simplicity, all constructors examples in the Kind Basics section are going to be Nullary, further along, examples of other types of constructors will be shown.

Boxes for constructors

A Type is basically a box to keep the Constructors. The Bool Type, for example, is a box that stores the true and false constructors. But remember, when inside that box, they don't have any value, just a name, in order to have values, they need to be inside functions.

  • Reminder: The box is just a container, and so, it is used as an example. A type could be represented by anything with the capability to store things.

Constructors represents the concrete values stored by a Type, and are called by using it's type name + constructor name:

// Boolean type
type Bool {
    true
    false
}

// representation of the value
    Bool.true
    //or
    Bool.false

The Bool.true and Bool.false are the correct way to call those constructors outside their Type. In this case, the Bool Type.

Basic Functions

The life inside Kind Universe.

What are Functions

Functions gives types and constructors a meaning. Types, by themselves, are simply a categorization of constructors, but, when applied to functions, that's when the "magic" happens!

Just like the Astronaut from About Kind story, let's explore the Boolean planet to "discover" and document the functions "AND", "NOT" and "OR" (Don't it just look like some sort of time travel? Are you the Astronaut from the story?).

The Bool still has no concrete use, since it still has no function. True and false is just names for the constructors, but even so, they got to have some logic behind them. Let's start with Not Function, the Boolean Negation.

Defining a Function

Functions in Kind are like mathematical functions, you tell them how to work, give them something to work with and it will return an answer. Let's see how it works in the example bellow:

// selfReturningFunction.kind2

Identity (b: Bool) : Bool
Identity Bool.true = Bool.true
Identity Bool.false = Bool.false

This is a function that returns the input itself, it is called Identity function. And it is a simple example of the functions' syntax in Kind. In the first line there are a lot of information about the function for us and the machine to interpret it. And so here is a "translation" of this first line:

  • "Hmrm clears throat identity is a function that receives a variable named b , which is of the type Bool, and the function returns something of the type Bool."

Function Anatomy

--Img--

[Yes, all of that is written up there, functions in Kind always start with their name, the name not necessarily needs to start with a lower case letter, but its my personal preference, you could name it ItSelf or Itself.After you name the function we open brackets and we write the arguments followed to the type of that function (b: Bool) (c: Bool) (d: Bool) and then we close brackets. Once we are done listing all the arguments our function has we add a cólon : to tell Kind we have named our function and listing the arguments and we proceed to the return, after the Cólon it means that our function is going to give us a result of something of that type, in our example we decided to use Bool as the type of return, but it could be any existing type in Kind, even a type you create yourself. [It is kind erroneous calling it a variable since they are immutable, they are values of that type, but we call them variable]]

Return

Lets use our box again, when we pattern matched our variable and we got either true or false, now we must specify what to return for those cases, on our example we returned Bool.true when true and Bool.false for false, that means we covered every possibility in the type Bool and we gave a Bool return to the function, which is what it expected.

for the box, it would look like this:

--Img--

You always gotta fill the answer with something of the type you specified in first place, it won't work if you return something of a different type from what you specified, this would be an example;

Wrong (a: Bool) : Bool
Wrong Bool.true = Bool.true
Wrong Bool.false = Nat.zero

Nat.zero is something of the type Nat, but we specified the return as a Bool, therefore the type checker would return an error of type in this situation.

// Type mismatch in the function named wrong.

-   ERROR  Type mismatch

  • Got      : Nat 
  • Expected : Bool 

  Wrong Bool.true = Bool.true
  Wrong Bool.false = Nat.zero
                     ┬───────
                     └Here!

As we have seen in Type Checker, this is how a code would return with the wrong type

Pattern Matching - match

All a data constructor does is holding values together. When we want to use them we need to deconstruct in order to specify what to do based on which constructor is being used. This is done with pattern matching. Type is the creator, holder, container, match is the deconstructed, analyzer, bond breaker.

Pattern matching is the act of verify possible matches of a given value, this is done sequentially.

On our functions in Kind we call it case and we give the value our variable, like in the second line of our example, we verify within b the possible matches, in that case it can only be true or false, since the Bool type has only two possible matches.

Let's go back to our boxes, here is the boolean box:

--Img--

~~These are the two possible cases of a value of the type Bool, it's either true or false, because its how we defined in our type Bool , so when we open a match of something from the type Bool, its like if we were opening the box, looking at every possibility and giving them an answer to what to do when the pattern matches for every of the single cases. ~~

To visualize the options we can use branches to see clearer the possible paths.

  match variable
   /       \ 
 true      false
  |          |     
  ?a         ?b

  • ?a is the return for the function MATCH the variable we input is true.

  • ?b is the return for the function MATCH the variable we input is false.

in our example itself we returned True case b is true and False case b is false.

    match b
   /      \ 
 true     false
  |         |     
 true     false

The returns are the tips of the branches.

Basic Function Example

First things first, create a new file namedNegation.kind2.

In our Negation.kind2 file we start with the first line (You can try doing it by yourself, click here for the answer)

Negation.function (b: Bool) : Bool 
Negation.function b = ?help

Kind Goals

A goal can be written as ? followed by a name. For example, ?help is a goal named help. Goals are extremely useful when developing algorithms and proofs, as they allow you to keep a part of your program incomplete while you work on the rest. They also allow you to inspect the context and expected type on that part. For example, our help goal in negation will display:

+  INFO  Inspection.

    • Expected: Bool 

    • Context: 
    •   b : Bool 

    Negation.function (b: Bool) : Bool 
    Negation.function b = ?help
                          ┬────
                          └Here!

Notice how it shows the type it expects on each hole, as well as the context available there.

Our function named functionhas only one variable for us to work with, now if we had more variables and needed to look even further in our branches of possibilities, we could open a case inside a case (pattern match a value inside another branch). We are going to look further in the following examples.

Intermediate Function Example

After we defined the "NOT" function, we still have the "AND" and "OR" functions, but those functions have two variables as arguments, and we need to verify deeper down inside each case, lets investigate together.

Now that we are done with the Negation.kind2 file, we can save it and open a new one named Logics.kind2

The logical AND operator returns true if both operands are true and returns false otherwise, and the result is of type Bool. This is how the function header would look like:

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and a b = ?ab

If you want, you can proceed by yourself. After this line, it is the solution and explanation.

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and Bool.true b = ?a
Logics.and Bool.false b = ?b

We are pattern matching our variable b , in the first branch, we are working with the possibility of b being true, in that case we must analyze a because the answer depends on that, since its only true if both of our values are true.

      case b
     /       \ 
-> true      false
    |          |     
   ?a         ?b

We can open a case in the variable a when we are analyzing the case of b being true. It would look like that

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and Bool.true  Bool.true = ?a
Logics.and Bool.false Bool.true = ?b
Logics.and a          Bool.false = ?c

Now we are working with both cases:

  • Case b is true and case a is true = Goal a (?a)
  • Case b is true and case a is false = Goal b (?b)
       case b
      /      \ 
    true     false
     |         |     
-> case a      ?c
   /    \
 ?a      ?b

Following our logic, when A and B are true, the answer is true, therefore the goal a (?a) is Bool.true, and when B is true but A is false, we have Bool.false as answer:

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and Bool.true  Bool.true = Bool.true
Logics.and Bool.false Bool.true = Bool.false
Logics.and a          Bool.false = ?c
       case b
      /      \ 
    true     false
     |         |     
-> case a      ?c
   /    \
true    false
 |        |
true     false

We have now finished our left branch, or, the branch with value true. Time for us to go to the false branch.

We do the same as we did before, but we know both values MUST be true in order for the function to return true, therefore if b is already false, it is impossible for it to return true, we would get the function looking like that:

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and Bool.true  Bool.true = Bool.true
Logics.and Bool.false Bool.true = Bool.false
Logics.and a          Bool.false = Bool.false
       case b
      /      \ 
    true     false
     |         |     
   case a    false  <-
   /    \
true    false
 |        |
true     false

And this is how the And function would look like in Kind . . . BUT! you can improve it even further, i wont give you the answer here, but you are more than welcome to do it yourself, don't worry if you cant find the answer now, you can come back later and redo it with way more knowledge! ahh!! the smarter version is in Functions if you want to look for it.

Running a Function

Now that we have learned all about how to build a function, it is time for us to test our logics and if the function is working as intended, if we wrote everything right and all type checked, it means all types and syntaxes are right, and in here, we are going to learn how to run a function.

First we are going to add the name of the file as a function in the code, without arguments just the name and a return, since our file is named Logics.kind2we are going to add it to the bottom of the file, with the return of the function we are going to try out. We are testing the Logics.and function, therefore the return is of the Bool type, we would add a line with the following code:

Main : Bool {
  ...
}

Main: type of Return

Bellow that line we call our function to run, our Logics.and function receives two booleans as argument of the variables a and b , so we are going to test it with two booleans:

Logics.and (a: Bool) (b: Bool) : Bool
Logics.and Bool.true  Bool.true = Bool.true
Logics.and Bool.false Bool.true = Bool.false
Logics.and a          Bool.false = Bool.false

Main : Bool {
  Logics.and Bool.true Bool.false 
}

If you want to try other options, you can change the two arguments as the following examples:

//Examples of function call:
// Logics.and (Bool.true)  (Bool.true)
// Logics.and (Bool.false) (Bool.true)
// Logics.and (Bool.false) (Bool.false)

Note: Kind can only run one function at time, you can have as many functions in a file as you want, but you can only run one at a time.

With all this knowledge, you can do the "OR" logics, and you can also find more basic Bool exercises in our github. The "OR" logic answer can be found here.

Before proceeding to learn about functions, and how to use constructors inside them, it is important to understand about an important tool in Kind's environment, the Type Checker!

Type Checker

Expected description, found joke.

The Type Checker is one of Kind's strongest features, and throughout this book it will be used very often. Remember back in Hello Kind! where we "type checked" a file? Now is the time to understand what really happened there.

What is a Type Checker

A type exists with its rules, and those rules place limits on its constructors. The Type Checker is an algorithm that inspect if the limits of a type are being respected. The action of verifying types is called type checking.

The Type checker is a very important tool, because the bigger a code is, the harder it will be to make changes, even small ones, and not compromise something along the way. It guides us in where it is needed to make changes. This, by itself, drastically reduces the chances of bugs in our programs while also helping to keep our codes more concise and readable.

As big as a code can be, the Type Checker will be your best friend when working with it. The bigger the code, the more rewarding it feels to use it.

Type Checkers can be separated in two categories:

  • Static Type Checker
  • Dynamic Type Checker

And this guide addresses the one that Kind uses, the Static Type Checker.

What it does

The Type Checker does two sorts of verifications:

  • Syntax Verification
  • Types Verification

In the first step, the Type Checker checks the syntax of the code. Syntax is the language used in Kind, just like all the other languages in the word. Portuguese, deutsch, english and so on, every one of these has its own rules and methods, and it's used to communicate. Kind syntax works in the same way, and the Type Checker will verify if there it is no mistakes in your writing. If it finds any mistake, Kind's Type Checker will point to you where and what it is.

- ERROR  Unexpected token 'true'.

type Bool  
 true
 ┬───
 └Here!
 false
}

Above, the Type Checker found an error in the code. See how it says how it was expected a curly bracket, and instead found the letter "true". That's why this code is missing a "{" to open the constructors' box. If no syntax error is found in the code, the Type Checker will proceed to its next function, to verify if the Types are correct. Kind is strongly Typed, therefore it's always necessary to explicit the types that are in the code.

Imagine you are reading a code that uses the Bool Type, and in some point you verify that a function returns a Nat type (the type of the natural numbers). The Type Checker mission is to find and point this mismatch. That way, this code can be corrected and will be more safe, reliable and clearer. The Type Checker is like your best friend when writing.

It is called Static Type Checker because it checks everything before running the program. iIf both syntax and type are ok, the console will show the message: All terms check. This means that the file Syntax and Types are right and ready to run!

//Terminal
All terms check.

It is strongly recommended to Type Check a file every time before running it, to avoid potential time waste. Because, if the types are wrong, there will be a compilation error message, and it will be necessary to type check it all over again, and that's double of your time wasted! To type check a file, simply use this command:

//Terminal
kind2 check hello_world.kind2

You must replace the fileName for the name of the file you're using, and don't forget the extension .kind! Knowing how to use this powerful tool, let's learn more about what gives life to Kind, the functions.

Thats all of the Kind Basics! if have come all this way congrats! now you can write basic functions in Kind, now, we can proceed to Kind Intermediate! Let's go Rookie, time for us go to a Voyage!

Examples

After learning about Constructors, Types and Functions, you may use this section to see and study some examples from each of them. Simply use the index navigation below:

  1. Basic Types Examples
  2. Basic Constructor Examples
  3. Basic Function Examples

Basic Type Examples

Then, in this section you may find Basic type examples with only Nullary Constructors.

Type Single

// A type with only one constructor that doesn't have a stored value.
type Single { 
  lonely       // :(
}

// Single concrete values: 
  // Single.lonely

Type Bool

// A type with two constructors where both doesn't have a stored value.

type Bool { 
  true
  false
}

// Bool concrete values:
  // Bool.true
  // Bool.false

Type Cardinal

Type Cardinal
// A type with four constructors and neither of them have a stored value.

type Cardinal { 
  north
  south
  west
  east
}

// Cardinal concrete values: 
  // Cardinal.north
  // Cardinal.south
  // Cardinal.west
  // Cardinal.east

Basic Constructors Examples

Here are examples of nullary constructors using different Types.

Single Constructors

// A type with only one constructor without a stored value.

type Single {
  lonely       // :(
}

// Single constructor: 
  // lonely

Bool Constructors

// A type with two constructors where both do not have a stored value.

type Bool { 
  true
  false 
}

// Bool constructors:
  // true
  // false

Cardinal Constructors

// A type with four constructors and neither of them have a stored value.

type Cardinal { 
  north  
  south  
  west   
  east     
}

// Cardinal constructors: 
  // north
  // south
  // west
  // east

Basic Function Examples

And finally, some Basic Function Examples using the Boolean Type.

Function Identity

Identity (b: Bool): Bool 
Identity b = b

The Identity function always returns the input value itself. Therefore, if "b" value is "True" then the output is also "True". The same would happen if the value of "b" is "False".

Function Negation

Negation (a: Bool) : Bool 
Negation Bool.true = Bool.false
Negation Bool.false = Bool.true

The function negation always returns the opposite of the user input. If the input is the Boolean "True", it returns "False". The contrary is also correct.

Function And

And (a: Bool) (b: Bool) : Bool
And Bool.true Bool.true = Bool.true
And Bool.true Bool.false = Bool.false
And Bool.false Bool.true = Bool.false
And Bool.false Bool.false = Bool.false

This function basically returns True if both inputs are "True". Taking close attention to the "True" branch inside "case b", you may realize it does the same as function identity, returns the value of the input itself. Also, you don't really need to examine the "False" branch, because every other input will return False. So, let's take a look on how to better write this function.

Function And with Pattern Matching

And (a: Bool) (b: Bool) : Bool {
  match Bool a {
    true => b
    false => Bool.false
  }
}

One possible way to write the function is opening the "case a b", in other worlds, opening both cases at the same time. But, in this situation, there are a lot of Bool.false outcomes. To avoid this repetition you can set a default answer and make the cases that matches this to be implicit. Just like below:

And (a: Bool) (b: Bool) : Bool
And Bool.true  b = b
And Bool.false b = Bool.false

Function Or

Or (a: Bool) (b: Bool) : Bool
Or Bool.true Bool.true = Bool.true
Or Bool.true Bool.false = Bool.true
Or Bool.false Bool.true = Bool.true
Or Bool.false Bool.false = Bool.false

According to the Or logics, if any input to this function is "True", then the outcome will also be "True". That's why the "True" branch on "case a" does not depend on the "b" value. On the other hand, for the "False" branch inside the same case, the outcome depends purely on the "b" value. If it is "True" the function returns "True", and if it is "False" the return will also be "False".

Let's see how it is possible to would work using Pattern Matching.

Function Or with Pattern Matching

Or (a: Bool) (b: Bool) : Bool {
 match Bool a {
    true => Bool.true
    false => b
  }
}

It basically happens the same as the function AND example, there is a repetition of the same outcome, in this case the "Bool.true". So it is possible to do the sabe as we did before, set it as the default answer and implicit some of the pattern match cases. It would look like this:

Or (a: Bool) (b: Bool) : Bool
Or Bool.true  b = Bool.true
Or Bool.false b = b

Function Equal with composition

Eql (a: Bool) (b: Bool) : Bool
Eql Bool.true   Bool.true  = Bool.true
Eql Bool.false  Bool.false = Bool.true
Eql a           b          = Bool.false

You can use functions inside functions as well, that is, hacking the game! We are going to learn about it later, but as you are already here, know that you can compose functions.

A Kind Voyage!

We are here again Kind astronaut, for a new voyage, in this Journey we are going to explore things beyond only syntax in Kind, we are going to see different types, constructors and concepts, everything is listed in the topics bellow:

  1. Constructors with Value - Constructors Part 2
  2. Polymorphic Types - Types Part 2
  3. Accessing Constructors Values
  4. More about Functions - Functions Part 2

In our previous exploration we went a little bit deep into the Boolean planet, now we are going to explore some complex Life Forms, the Maybe and Pair Planet.

In our voyage we are going to have a very similar approach that we had in Kind Basics, but instead we are in a Intermediate level, the learning curve here is a little bit higher but nothing impossible, i am sure that together we can understand and work with these types, so, let's go buddy, time for us to learn more things about Constructors.

Constructors with Value

Constructors Part 2

Atmospheric Entry

In this Voyage we are going to take larger steps, a lot of abstract concepts are going to be seen here, but we are going to start with a simpler approach and as we proceed, we are going to go deeper on everything we learn in here. Before we leave on our next trip towards the Pair and Maybe planets, i want to show you some simpler concepts before we fully see their potential, then lets proceed.

Beyond Nullary Constructors

Constructors are made to hold values together, we just learned about the Nullary constructors, or constants, and here we are going to learn about constructors with values. if it sound confusing don't worry, we are going to explore this concept in order for us to understand all about it, first we proceed with a variation of the type Maybe, then we go for the Pairs.

Maybe variation and Constructors with Values

The type Maybe in kind is very powerful, but in here we are going to use a variation of that type to explain the concept of constructors with value. Constructors are functions, Nullary constructors has no arguments, therefore they return nothing but their own value, but constructors with arguments their value can vary, and this is how the constructor with arguments would look:

type MaybeBool {
  none
  some (value: Bool)
}

As you can see, the some constructor is a function that has an argument value of the type Bool.

If we think of the type Bool it is a type with two possible values True or False, in this Maybe version it is very similar, but instead, it has a function that stores a value of the type Bool. Therefore, we can notice that this MaybeBool is basically the same as the Boolean type, but instead of only giving us two options, it also stores a value of that type. In the case of our constructor to be none, it has no value, but if it is some, it has something stored inside the constructor. Using a bag as example, either you have No bag (none) or a bag with something inside (some).

Building a Maybe Variation Concrete value using Constructors with arguments

To build concrete values we are going to do the same as we learned in Basic Types, we write typename.constructor:

MaybeBool.none // Right
MaybeBool.some // Wrong

But that wouldn't work, since MaybeBool is a function, we need to give him something of the type Bool, since the variable value is of the type Bool

MaybeBool.some (Bool.true)  // Right
MaybeBool.some (Bool.false) // Right

Either of the options works, since we fulfilled with what Kind asked us, if it doesn't seem very organic to you, we are going to revise this concept multiple time throughout the book. Then all you gotta do is, typename.constructor(arguments of that type) and you build a concrete value of that type, let us see another example, now with Pairs.

Pair variation and Constructors with Values

Same as the Maybe type, the pair also has a constructor with value, but as the name suggest it has TWO values, and instead of being either One or Another, it is always BOTH, can you figure out how? If not thats ok, lets write a variation of the Pair type, a Pair of Bool.

type PairBool {
  new (fst: Bool) (snd: Bool)
}

This is how a pair of bool would look like, you have only one constructor because it is ALWAYS that one, you cannot have an either option here! i choose the name new for the constructor. fst and snd for the arguments just to make it clearer, you could choose any name you want! Let us build now concrete pair values using the Bool type.

Building a Pair Variation Concrete value using Constructors with arguments

Pair.new // Wrong

The new constructor receives two values as arguments, the fst and snd, both being of the type Bool, therefore

Pair.new Bool.true Bool.true
Pair.new Bool.true Bool.false

There are two other possibilities for this pair, if you want to try to build yourself using the Bool.false, you are more than welcome to, for practice purposes.

Pair is a good type to store two things together, imagine you want to have a name linked to a number? Like:

1 - Anna
2 - Bruce
3 - Jeorge
4 - Myrna
...

Or maybe you want to link other two things together, like a list to a boolean.

 []      - Bool.true
 [1]     - Bool.false
 [1,2]   - Bool.true
 [1,2,3] - Bool.false
 . . .

That is a lot of different types, we've seen Numbers, Text, List, Booleans (Nat, String, List, Bool) only in this example, there are infinite types out there, imagine creating a Pair type for each and every of the possibilities, or making a Maybe Type for each of the possible types, that would take forever right? Yes, it would take forever, BUT types are very smart and they asked themselves, what if we become a VARIABLE?

Yes, types can be variables, in Polymorphic Types we are going to learn how to use this powerful Tool to include every possible type.

Let's go partner, it is time for me to take you to the real Pair and Maybe planets, off we go to the Polymorphic Types planets, FIRST ONE, Pairs!!!!

Polymorphic Types

Types Part 2

First Encounter

Welcome to this new planet, the Pair planet, in here we are going to learn about a new sort of Type.

In the Pair Planet, every single life form is tied to another, two things walking hands held to each other, we can also notice, all life forms in the Bool Planet they have no specific shape, their shape is NOT YET DEFINED, but let me show you a thing, the portal shaper.

Whenever the pairs pass through the portal shaper, they actually get their shape defined, and once its defined they can't go back, therefore, before the portal shaper they have no defined shape, after they pass through they get their shape defined.

The Pair shape, each one get an individual shape, they can be the same, they can be different, no matter, they can be anything, as long as they pass through the Shaper, this sort of life form is known as Polymorphic.

Polymorphism

Whenever i ask you to think of a Pair, i am pretty sure your brain will think of a Pair of somethings am i right? even if you think of a pair of "nothings", this nothing is a something, on Kind it is the same. Something is abstract and can be anything, this something can be Fruits, can be Cars, can be Number, can be anything of a group, and groups are Types.

The portal shaper is the return of the function, and before the pairs pass through they are variables, and once they pass, the variable becomes a specific Type.

In Kind we name these as Polymorphic Types, they are variables that can assume any type, some types needs these variables in order to encompass multiple things, same for Lists, whenever you think of a list, you think of a list of something, imagine having to define types for every single thing in existence? The way we do it, is having a variable that we can assign it to some specific type we want.

Pairs

As we have seen in Constructors with Value, the Pair is a type with a single constructor that has two arguments to it, the First (fst) value of the pair and the Second (snd) value of that pair, but now we are going to modify a thing, our Pair was a Pair of Booleans, now we are going to make the type Pair that includes all types in kind using Variables as Polymorphic Types, in this case it would look like this:

type Pair (a: Type) (b: Type) { 
  new (fst: a) (snd: b)
}

Well, let us read that right now:

Hmrm clears throat the type Pair is a type that has TWO POLYMORPHIC TYPES A and B, it has one constructor named new, and this constructor has two (arguments, values, variables. Either of these options work) values, fst is of type A and snd is of the type B.

This would be the anatomy of this type.

--Img--

A and B are type variables, we call these variables Polymorphic Types, to differ them of value variables, to make the code more readable, most of the Type variables are written in Upper case Letter, as the constructor variables usually start in lower case, to make it clearer to the reader.

The Pair type has two variables because you can have a Pair of two distinct things, like we saw earlier, but A and B can be of the same type, that is not a problem, as long as their values belong to the Types you input, Pairs accept them all, even other pairs (Let this part for later! Too deep down!!!).

That changes mainly the way we build our concrete values with Polymorphic Types, as we specify what is the type of each of the values inside the constructor before we fill them, here are some examples of Pairs:

// Pair of Bools 
Pair.new Bool Bool Bool.true  Bool.true 
Pair.new Bool Bool Bool.false Bool.false

//Pair of Number and Text 
Pair.new Nat String 1n "Anna"
Pair.new Nat String 2n "Bruce"

//Pair of a Numeric List and a Boolean
Pair.new (List Nat) Bool [] Bool.true
Pair.new (List Nat) Bool [1n] Bool.false

As said above, you gotta be very precise with specifying a type, if you invert A with B you would get errors.

// Here we said the First type is a Number and we wrote a String (Text)
// We also said the Second type is a String and we wrote a Nat (Number)

Pair.new Nat String "Anna" 1n 
Pair.new Nat String "Bruce" 2n

Next, let's look for the other type we learned earlier the Maybe type, but now, lets make it work with all Types, having a Polymorphic Type variable.

Maybe

We are going to use Maybe a lot, imagine we need to write a function that get the first element of a list, if this list is empty, what would we return? the number 0? a text saying "nothing"? we have the Maybe.none for that, and if that list has something, we take the first element and save him inside our bag, the Maybe.some. Bless the Maybe!!

Like the Pair and many other types are going to work in the future, the Maybe type has a Polymorphic Type variable attached to it, since we can save everything on it, isn't it lovely?(Is it clear my favoritism to the type maybe? no? i gotta make it clear here!) This is how it should look:

type Maybe (a: Type) {
  none 
  some (value: a)
}

Well, let us read that:

Hmrm clears throat the type Maybe is a type that has ONE POLYMORPHIC TYPE A, it has two constructors, none and some, and the some constructor has one (argument, value, variable. Either of these options work) variable, named value that is something of the type A.

In this case we only need one Polymorphic Type variable, since it only stores one value of a single Type Lets build some concrete value on the Maybe type:

//None examples
Maybe.none Bool
Maybe.none Nat
Maybe.none String
Maybe.none (List Nat)

//Some examples
Maybe.some Bool Bool.true
Maybe.some Bool Bool.false
Maybe.some String "Maria"
Maybe.some String "Anna"

I like to say that the some constructor "hugs" the value and takes care of him, the Maybe is very lovely with their values!

Since the type Pair stores two values and the type Maybe stores one value, if we need to access them somehow in a function, we are going to do within cases as well, pretty much everything in kind is done with case, let us learn how to in the next section, Accessing Constructor Values.

Accessing Constructor Values

In case you need to access, case.

A New Discovery

In the Basic Function section we learned that Case is the desconstrutor, analyzer, bond breaker, and now we are going to understand why it is the desconstrutor. Constructors they Hold the value, and the case gives us access to that value, when we are pattern matching a variable of a type with a constructor that is storing some information.

I am going to write a wrapper function for the Boolean true, that function is going to store the concrete value of Bool.false in a maybe type. Let's make a file named WeLoveMaybe.... ah, okay, we can make a Maybes.kind to test our functions.

Accessing Values in Constructors using Maybe as example

Maybe.wrapper (b: Bool) : Maybe Bool
Maybe.wrapper Bool.true = Maybe.some Bool.true
Maybe.wrapper Bool.false = Maybe.none Bool

This function isn't very useful, but it works as an example, lets run it and see the results for each input, Bool.true and Bool.false

--Img--

The Maybe.some saves anything we want to, in this case we decided to save a concrete value of Bool.false, and if we input a Bool.false value, it returns none, we are going to have better usage for the Maybe type in the future. Now let us do the opposite, an unwrapper, a function that receives a Maybe and returns to us a Bool

Maybe.unwrapper (b: (Maybe Bool)) : Bool
Maybe.unwrapper Maybe.none = ?a
Maybe.unwrapper (Maybe.some value) = ?b

This is a very important part that we want you to pay attention, i am going to explain how data saved by constructors can be used, using branches to make it visible and clearer, also within the goals and cases for more visualization, lets proceed.

If we type check this code, Kind is going to give us two paths for us to follow, the none and some, the type checker would look somewhat like that:

+   INFO  Inspection.

  • Expected: Bool 

  Maybe.unwrapper Maybe.none = ?a
                               ┬─
                               └Here!

+ INFO  Inspection.

  • Expected: Bool 

  • Context: 
    •   b.value : Type 
    •   b.value = Bool 
    •   v       : b.value 

  Maybe.unwrapper (Maybe.some v) = ?b
                                   ┬─
                                   └Here!

This is how it would look like with the branches

    case b
    /   \
 none   some (value)
  |      |
  ?a     ?b

The some Constructor carries the saved value with him, and the way it is represented in kind is constructor.data,

but this value is ONLY ACCESSIBLE BY THAT BRANCH, the none has NO access to concrete value, remember the bag example? the none branch means YOU HAVE NO BAG, but the some means YOU HAVE A BAG and the value is inside that bag.

As you can see, our b.value is something of the type Bool, which is our concrete value, the thing inside the bag, whatever the bag is holding, any value in the Maybe.some constructor is our thing.value whenever we access that variable.

But, what do we return when it is none? well, this is why the type Maybe exists, so our "unwrapper" function isn't very useful, other than to show us how this type works, but don't worry, at the end of this explanation there are going to be some real examples and usage for the type Maybe, lets proceed with the example thou. Our unwrapper version should return to us false if there it is nothing and if there it is something, it should return the value of that boolean saved. In the wrapper we saved False if the boolean given is true.

Maybes.unwrapper (b: Maybe<Bool>): Bool
  case b {
    none: Bool.false
    some: b.value
  }
     case b
    /       \
  none     some (b.value)
   |           |
Bool.false   b.value

For the Maybe type, this is how we get access to the value stored by it, if you want to see real functions uses, go here for examples or here to practice with the type Maybe. These examples were only to show you how to use the type Maybe and how to access a value stored by it, but this is how every type that has a constructor with arguments works, these are the first steps we take towards some very complex matter. Time for the Pair

Accessing values in constructors using Pairs.

Pairs are incredible and yet a very simple Type, they can see intimidating because it has two Polymorphic Types but they are indeed very simple.

Since Pairs has only one constructor, it branch always carries their values with them, we saw how a branch carries value for the Maybe type in the Maybe.some branch, lets write two functions, one that gets the First element of a pair and one that gets the Second element of a Pair.

Lets write both functions in a file named Pairs.kind, and name the functions first and second, both of the functions won't be Polymorphic at first, but then we write them to be Polymorphic, just for the simplicity of the example. The functions are going to have as argument a variable named pair of the type Pair Bool Bool and the return is just a Bool.

//this function returns the first value of the pair
Pairs.first (pair: (Pair Bool Bool)) : Bool {
  ?a
}

//this function returns the second value of the pair
Pairs.second (pair: (Pair Bool Bool)) : Bool {
  ?b
  }

If you want you can try to write the answer by yourself, below this line there will be the answer. Okay, first things first (hehe) as everything in case, we open a Kind! i mean, we open a Case like we always gonna do in functions.

Pairs.first (pair: (Pair Bool Bool)) : Bool {
  match Pair pair {
    new => ?a
  }
}

The Pair has only one constructor named new, then it is the only thing inside our case, looks cute doesn't it?

+ INFO  Inspection.

  • Expected: Bool 

  • Context:
    •   pair     : (Pair Bool Bool) 
    •   pair.fst : Bool 
    •   pair.snd : Bool 

  match Pair pair {
    new => ?
           ┬
           └Here!
  }

When we opened the case, we gained access to both values, fst and snd, this is how it would look like in the branch.

  match pair
         |
        new pair.fst pair.snd
         |
         ?a

A very simple branch, as said above, pairs are very simple, since we want the first value of that pair, all we need to do is return the pair.fst value.

Pairs.first (pair: (Pair Bool Bool)) : Bool {
  match Pair pair {
    new => pair.fst
  }
}

The second you can try to do by yourself, the answer is in the Function Examples you can find later on, i strongly recommend you to try to do them by yourself.

Well, this function only works for Booleans, imagine if we had to do one for each type in Kind, lucky for us we know Polymorphic Types, we can use them to make functions that accepts every sort of type, and we call that Abstraction, when you can abstract your function to work for every single type in Kind. Some functions won't really work, but a lot of them will, and if you can think how to Abstract them, that is very good, abstraction is one of the keys to be a good Kind Developer, YET it is a very hard concept and thing to get used to, give yourself some time, it is okay.

If you want to practice some pair functions can be found here, and the answers here.

Okay Buddy, now that we have met the Polymorphic Types and Constructor that saves data and how to access that data, lets learn how to work with that information with, learn more about pattern match is going to be very useful for us, let's see More about Functions.

More about Functions

Functions Part 2

Another Research

Whenever we talk about Pattern Matching, a lot of doubt can occur, in here i plan to get rid of most of this doubt about Polymorphic Type functions, so we can proceed to the next section of this Book, lets work in some Case usage, examples and exercises.

Case and Values

As said in Basic Functions, "Pattern matching is the act of verify possible matches of a given value, this is done sequentially." and in here i want to focus in values, now that we know how to access values held by constructors.

We are going to build some functions that work particularly in situations where we need to analyze values, since we know the types Bool, Maybe and Pair, we are going to mostly use them to practice. Here are some examples of functions using values that we access from the type Maybe.

Maybe First Example

This first function example can be seen as a function to verify if something you saved is the same as you input, we are going to use this function in a future example with different parameters.

is_equal (input: Bool) (saved: (Maybe Bool)) : Bool {
	match Maybe saved {
    none => Bool.false
    some => ?b
  }
}

If we Type Check that function we get the following result:

+ INFO  Inspection.

  • Expected: Bool 

  • Context: 
    •   input       : Bool 
    •   saved       : (Maybe Bool) 
    •   saved.value : Bool 

  none => Bool.false
  some => ?b
          ┬─
          └Here!

We have an user input that is a Bool and the saved.value that is also a Bool, now it is time for us to open a case for the saved.value, it is a value of the type Bool, then you have either true or false.

is_equal (input: Bool) (saved: (Maybe Bool)) : Bool {
  match Maybe saved {
    none => Bool.false
    some => match Bool saved.value {
      true => ?a
      false => ?b
    }
  }
}

Now we just need to verify each branch, this function idea is to show you that we can open a case in everything that is a concrete value, since saved.value is a concrete value of the type Bool, we can pattern match it.

The answer of this function can be found here, and let's proceed to the next function, in here we are going to build a value inside a function and pattern match it.

Maybe Second Example

This one is purely meant to show you that we can build values inside function and pattern match it, i am going to write here the same function we just did but version 2.

Is_equal_2 (input: Bool) (saved: (Maybe Bool)) : Bool {
  match Maybe saved {
    none => Bool.false
    some => (
      let eql = Bool.equal Bool.true saved.value
      ?a
    )
  }
}

Now, to the type check:

+ INFO  Inspection.

  • Expected: Bool 

  • Context: 
    •   input       : Bool 
    •   saved       : (Maybe Bool) 
    •   saved.value : Bool 
    •   eql         : Bool 
    •   eql         = (Bool.equal Bool.true saved.value)

  let eql = Bool.equal Bool.true saved.value
  ?a
  ┬─
  └Here!

First i need to explain you the let . We use let to build some value inside a function and assign it to a name, that sometimes makes the code clearer and have better readability, but we are going to go without it, it is just for showing purposes. In this case we built something of the type Bool using the function Bool.eql, the result is either true or false, then it is a value of the type Bool Lets move the Bool.eql out of the let and just pattern match it.

Is_equal_2(input: Bool) (saved: (Maybe Bool)) : Bool {
  match Maybe saved {
    none => Bool.false
    some => match Bool (Bool.eql Bool.true saved.value) {
      true => ?a
      false => ?b
    }
  }
}

//If you wanted to use case on a value declared on the let you could
Is_equal_2 (input: Bool) (saved: (Maybe Bool)) : Bool {
  match Maybe saved {
    none => Bool.false
    some => (
      let eql = Bool.equal Bool.true saved.value
      match Bool eql {
        true => ?a
        false => ?b
      }
    )
  }
}
  
  //They're the same

That is completely legal and works, you are saying the following: "If the saved value is true then ?a . else ?b " and ah, that is literally the known if else on Kind.

Pair First Example

We are going to dive a little bit here, for us to practice Polymorphic Types, first a function that verifies if any of values of the pair are true.

//If we open the pair first
Snd(pair: (Pair Bool Bool)) : Bool {
  match Pair pair {
    new fst snd => snd
  }
}

//If we open the pair afterwards
Snd(pair: (Pair Bool Bool)) : Bool {
  match Pair pair {
    new => pair.snd
  }
}

This function gets the second value of the Pair, that in this case is a Bool, but what if we wanted other Types? not only Bool?

//If we open the pair first
Snd <a> (pair: (Pair a a)) : a {
  match Pair pair {
    new fst snd => snd
  }
}

//If we open the pair afterwards
Snd <a> (pair: (Pair a a)) : a {
  match Pair pair {
    new => pair.snd
  }
}

But the problem is, we limited the Types, the pairs can only have the same Type in this case, what if we wanted a Pair of two different values?

Pair Second Example

//If we open the pair first
Snd <a> <b> (pair: (Pair a b)) : b {
  match Pair pair {
    new fst snd => snd
  }
}

//If we open the pair afterwards
Snd <a> <b> (pair: (Pair a b)) : b {
  match Pair pair {
    new => pair.snd
  }
}

ps: A and B can be of the same Type, they are just variables.

We literally just changed the header of the function, everything else stays the same. This is a complicated step to take, but don't worry, only with practice and time this will clarify in your mind, i wanted to show you Abstraction for you to know that it is possible and have it growing on your mind, you are going to learn with time, don't worry!

You can look for more practicing exercises here, or look for Variation Examples or the official Pair/Maybe example. This is the end of our Voyage and the start of our Discovery!

Examples

After learning about Voyage, you may use this section to see and study some examples from each of them. Simply use the index navigation below:

  1. Maybe and Pair Basics
  2. Maybe and Pair
  3. Intermediate Types
  4. Intermediate Functions

Maybe and Pair Basics

MaybeBool type and PairBool type

Types

MaybeBool

type MaybeBool { 
  none 
  some (value: Bool)
 }
  
// MaybeBool concrete values:
  // MaybeBool.none
  // MaybeBool.some Bool.true 
  // MaybeBool.some Bool.false

PairBool

type PairBool {
  new (fst: Bool) (snd: Bool)
}

// PairBool concrete values:
  // PairBool.new Bool.true  Bool.true 
  // PairBool.new Bool.true  Bool.false
  // PairBool.new Bool.false Bool.true 
  // PairBool.new Bool.false Bool.false

Maybe and Pair

Maybe type and Pair type

Types

Maybe

type Maybe (a: Type) { 
  none 
  some (value: Bool)
 }
  
// Maybe concrete values:
  // Maybe.none
  // Maybe.some a value // value can be anything of the type a

//Examples:
  // Maybe.some Bool.true
  // Maybe.some (Pair.new Bool.true Bool.true)

Pair

type Pair (a: Type) (b: Type) {
  new (fst: a) (snd: b)
}

// Pair concrete values:
  // Pair.new a b fst snd // fst and snd can be anything of the type a and a
  
//Examples:
  // Pair.new Bool.true Bool.false
  // Pair.new (Maybe.none Bool) Bool.true

Intermediate Types

Types

type Relationship

//a type with three constructors, where two of them has no value stored to it, but
//the constructor other has a value named single of the type Single

type Relationship {
  couple
  marriage
  other (single: Single)
}

// Relationship concrete values:
	// Relationship.couple
	// Relationship.marriage
	// Relationship.other (Single.lonely)

type Multiple

//a type with two Polymorphic Types named a and b and four constructors,
//
//threethings has 
//          x is a value of the type a
//          y is a value of the type b
//          z is a value of the type Multiple with two Polymorphic types a and b
//
//onething has
//          x is a value of the type b
//
//twothings has
//          x is a value of the type a
//          y is a value of the type b
//
//emtpy has no value store to it 

type Multiple (a: Type) (b: Type) {
  threethings (x: a) (y: b) (z: Multiple a b)
  onething (x: b)
  twothings (x: a) (y: b)
  empty
}

//Since a and b are variables, some of the possibilites as example:
// a = Duo            | b = Duo
// a = Multiple a b   | b = Bool
// a = Bool           | b = Nat
//They can be of any Type, a and b can have the same Type as well.

// Multiple Concrete values:
	// Multiple.threethings Bool.true Bool.false (Multiple.empty)
	// Multiple.onething Bool.false
	// Multiple.twothings Bool.true Bool.false
	// Multiple.empty

Intermediate Functions

MaybeBool Examples

Function Create

Create (a:Bool) : MaybeBool{
 MaybeBool.some a
}

The create function gets the input "a" of the Type Bool and creates a Type MaybeBool where its value is "a". Therefore, if "a" is Bool.true, the result will be MaybeBool.some Bool.true, note that the value of "a" is now stored inside the constructor "some" of the MaybeBool type.

Function Or

Or (a: MaybeBool) (b: MaybeBool) : MaybeBool {
  match MaybeBool a {
    none => b
    some value => MaybeBool.some value
  }
}

The function "or" returns the first input that is a Maybe.some

PairBool Examples

Function neg

Neg (riap: PairBool) : PairBool {
  match PairBool riap {
    new fst snd => 
      match Bool fst {
        true => 
          match Bool snd {
            true => PairBool.new Bool.false Bool.false
            false => PairBool.new Bool.false Bool.true
          }
        false => 
          match Bool snd {
            true => PairBool.new Bool.true Bool.false
            false => PairBool.new Bool.true Bool.true
          }
      }
  }
}

This function receives a PairBool and returns a new PairBool with the negation of its elements. If you look closely, there is a smarter way to do this function.

Function swap

swap (a: PairBool) : PairBool {
   match PairBool a {
    new: PairBool.new a.snd a.fst
  }
}

The swap functions simply swaps the first with the second element of the pair. Basically it creates a new pair where the second element is the first and vice versa.

A Kind Discovery!

Black holes and Revelations

Kind's universe is unlimited, there it is countless planets and also countless life forms ,but in here we are going to explore some abstractions, and the most important for this part, recursion and some ways to work with them:

  1. Currying
  2. Nat and List Types
  3. Recursive Algorithms

The Natural Number Planet and the Pair Planet.

In our voyage we are going to have a very similar approach that we had in Kind Basics, but instead we are in a Intermediate level, the learning curve here is a little bit higher but nothing impossible, i am sure that together we can understand and work with these types, so, let's go buddy, time for us to learn more things about Constructors.

Currying

Spicing things up

A Different method to represent a function

We learned in Basic Functions the standard method to build a function but here things are about to get spicy.

Currying

Currying is the transformation of a function with multiple arguments into a sequence of single-argument functions. That means converting a function like this f(a) (b) (c). The variables, a, b and c must have a type in Kind, lets name them a,b and c Polymorphic Types, since they can be of any type, and represent them using an Arrow:

f: a -> b -> c

In this example the function f has an argument of the type a, then one of the type b and return something of the type c, remember, a, b and c are only names for the Polymorphic Types, they can have the same type:

f (a: Bool) (b:Bool) : Bool         // Bool.eql, Bool.or, Bool.and, ...
/////////////////////////
f:    Bool ->  Bool -> Bool        // Bool.eql, Bool.or, Bool.and, ...
/////////////////////////
f:    Bool ->  Bool -> Bool
|      |        |       |
v      v        v       v
f (a: Bool) (b:Bool) : Bool

This method works for representing Generic Functions, since our function f can be any Bool function that receives two arguments, we don't clearly know which function we are referring to, that means we abstracted the specific function to a generic one. We are going to use this syntax in some functions and to understand better the type Nat.

Natural Numbers

A New Voyage

Welcome to the new planet, i hope you aren't dizzy from the travel! Let's go partner, I have many things I want to show you, and ah, welcome to the Natural Number Planet. Then let me ask you, when i said Natural Numbers, and thinking of types, can you imagine us doing an infinite type, since the natural numbers can go from zero to positive infinite? Well, you could go with:

type Nat { 
  zero
  one
  two
  three
  ....
}

And that would take ages (forever i would say), that's what the natural numbers thought as well, then they had to figure out how to have all numbers in a much smaller structure, it had to fit in a Planet. After years, the Nat (We are going to affectionately call them Nat, the type Nat) found out how:

type Nat {
  zero
  succ (pred: Nat)
}

Within these 2 constructors, the type Nat managed to approach all positive infinite numbers starting with zero, if you can't see how yet, by the end of this page, we are going to be able to! Also, just to make it clear, succ is a short name for Successor and pred is for Predecessor.

type Nat {
  zero                // Nullary constructor
  succ (pred: Nat)    // constructor with value
}

As we can see, zero is a constant, a Nullary constructor (which is true), now succ has a variable named pred of the type Nat.

Constructors with value

Lets remember two things here:

  • To declare concrete values, we write typename.constructor, using Bool as example we would have either Bool.true or Bool.false as valid concrete data to Bool type.
  • Functions have a name, followed to its arguments, the type, then the return. Now that we know the Nat type, if we were to declare its concrete values we would have:
Nat.zero
Nat.succ

Lets make a new file, named Numbers.kind and type check both of values, remembering, we can only do it one by one in Kind.

We add a line with Numbers: Nat to our file and lets test first the Nat.zero:

Numbers: Nat

All terms check.

Time for us to do the same with the Nat.succ:

Type mismatch.
- Expected: Nat
- Detected: (pred:Nat) -> Nat

The type checker acuses a Type mismatch, since it expected something of the type Nat, and found a function that has an argument of the type Nat, and then this function is something of the type Nat.

  • In kind we write a function the way we learned in Basic Functions, but we can represent it with arrows -> as explained in Currying, you can find more examples about it here.

Succs and Preds

TODO

Recursive Algorithms

TODO b

Syntax Sugar

Sugar

Contribuidores