Kind is a dependently typed programming language made by uwu-tech that I recently discovered through GitHub. Unlike Agda, Coq and co., Kind doesn't rely on a ML-esque syntax, but rather in one that resembles Typescript or Rust, which is interesting. It also has a small core and two main implementations; runs under Javascript or with Scheme (but that requires compiling the toolkit on macOS). So, in this blog post we'll be playing around a little bit with Kind.

Hello world!

My favorite kind of "hello world" on languages is not printing that to stdout, I think that there is something more beautiful when encoding Peano's natural numbers definition as an "hello world". For now, let's remember that a natural number \( \mathbb{N} \) is given by following inductive definition:

$$\begin{align*} zero &: \mathbb{N} \\ succ &: \mathbb{N} \to \mathbb{N} \end{align*}$$

which should be implemented like this:

type Nat {
	zero
	succ(ccus: Nat)
}

Running the type checker will give us the following (assuming the code is correct):

[email protected] Folder % kind-scm file.kind 
Nat: Type
Nat.s: Nat
Nat.succ: (ccus:Nat) -> Nat
Nat.zero: Nat

All terms check.

That's great. Now we are going to do something more complex. (Didn't happen)

Standar Library

Kind includes an useful standard library that will be using. But you need to have the type checker inside that folder in order to use it. This is one of the things that I don't like about this language. As far as I know, there is not proper way of importing external files (there was, but it's not the case anymore, it seems).

Discussion

It's an interesting project, but I don't think that it's in a state in which I consider it actually useful. There is a lot of great things that are actually implemented in Kind, but it's lack of documentation (and a few other things) make it difficult to use.

I have been the last two days trying to do something a little more complex, but it didn't work out. Or maybe it's just me who can't do it.

I'll try again in the future. But right now, I feel comfortable enough with Agda and Lean.

Binaries

For OS X: https://old.ivmoreau.com/static/kind-scm (I had to compile it myself)

For Linux: https://github.com/uwu-tech/Kind/releases

Enjoy!!