How does the `Word` type work in Kind Lang?

Question

The Word type (in kind lang) looks like this:

type Word ~ (size: Nat) {
  e                              ~ (size = Nat.zero),
  o<size: Nat>(pred: Word(size)) ~ (size = Nat.succ(size)),
  i<size: Nat>(pred: Word(size)) ~ (size = Nat.succ(size)),
}

The syntax is defined here.

All it says is:

type Name (A: Par0, B: Par1 ...) ~ (i: Idx0, j: Idx1 ...) {
  ctor0(field0: Fld0, field1: Fld1 ...) ~ (i = id0, j = idx1 ...)
  ctor1(field0: Fld0, field1: Fld1 ...) ~ (i = id0, j = idx1 ...)
  ...
}

Declares an inductive algebraic datatype. A simple datatype starts with the type keyword, followed by its name, followed by any number of parameters ("static polymorphic types"). Inside {} follows any number of constructors, each one is followed by its fields.

As an example, the following type, in Haskell:

data List a = Nil | Cons a (List a)

Can be written in Kind as:

type List (A: Type) {
  nil
  cons(head: A, tail: List(A))
}

... Where ~ (it's optional) stands for any number of indices ("dynamic polymorphic types"). In the constructor, its fields are also optionally followed by ~ and its concrete indices.

The Word type is used all over, mainly like this:

type U8 {
  new(value: Word(8))
}

That makes sense to me, we have a type record with a value field which is type Word(8). But how does the Word type itself work? I don't follow. Take one constructor line, like this:

o<size: Nat>(pred: Word(size)) ~ (size = Nat.succ(size))

What does that mean? Passing the pred: Word(size) seems like an infinite loop.

Another type with similar definition is Bits:

type Bits {
  e,
  o(pred: Bits),
  i(pred: Bits),
}

Maybe it has to do with self types?

Answer 1

I remembered this question seeing you issues in the Kind repo. The best way to understand the Word type is to understand the problem it solves. In our case we had the problem of defining a type for bytes, 32-bit integers, 64-bit integers etc. The first idea is to define it like this

type Byte {
  new(
    b0: Bool, b1: Bool, b2: Bool, b3: Bool, b4: Bool, b5: Bool, b6: Bool, b7: Bool
  )
}

this is correct, but writing algorithms using this type would be a pain. If we tried this with 32-bit integers it would cease to be a pain and become completely impractical. It's tempting to use

type Bits {
  e
  i(pred: Bits)
  o(pred: Bits)
}

because the algorithms would be much shorter. But this isn't correct since this type includes bit sequences of any length. However you could do something like this

type Bits0 {
  e
}
type Bits1 {
  i(pred: Bits0)
  o(pred: Bits0)
}
type Bits2 {
  i(pred: Bits1)
  o(pred: Bits1)
}

and so on. Of course this would make the algorithms terrible again, but what if instead of writing all these types we could write a function Word :: (n: Nat) -> Type that would serve that purpose? With Kind you can do that! And in two different ways. The simplest, easiest to understand and in hindsight what we should've done looks like this

type WordTip {
  e
}

type WordBit (n: Nat) {
  i(pred: Word(n))
  o(pred: Word(n))
}

Word(n: Nat): Type
  case n {
    zero:
      WordTip
    succ:
      WordBit(n.pred)
  }

The actual Word definition uses indexes to build the type as Labbekak explained. The difference between the two approaches is that our function uses the length to determine the constructors of the type. Indexed types go the other way around and use the constructors and parameters to determine the index of the constructed value. Indexes are more flexible. Functions that return types are generally easier to use. To give an example of what kinds of information we can keep track of using indexes. Consider this type

type NatList ~ (odds: Nat) {
  nil ~ (odds = 0)
  cons(tail_odds: Nat, head: Nat, tail: NatList(tail_odds)) ~ (odds = Nat.add(Nat.mod(head, 2), tail_odds))
}

It keeps track of the amount of odd numbers in a list of natural numbers. The (odds = Nat.add(Nat.mod(head, 2), tail_odds)) tells us what the index of the resulting will be after we call the constructor. So

NatList.cons(0, 5, NatList.nil)
  :: NatList(Nat.add(Nat.mod(5, 2), 0))
NatList.cons(0, 5, NatList.nil)
  :: NatList(1)

and

NatList.cons(0, 4, NatList.nil)
  :: NatList(Nat.add(Nat.mod(4, 2), 0))
NatList.cons(0, 4, NatList.nil)
  :: NatList(0)

Also note that we could use the same name for a parameter of the constructor and for the index. Like this

type NatList ~ (odds: Nat) {
  nil ~ (odds = 0)
  cons(odds: Nat, head: Nat, tail: NatList(odds)) ~ (odds = Nat.add(Nat.mod(head, 2), odds))
}

but that's confusing.

Answer 2

Giving the datatype in Agda-style syntax:

data Word : Nat -> Set where
  e : Word zero
  o : {size : Nat} -> Word size -> Word (suc size)
  i : {size : Nat} -> Word size -> Word (suc size)

So e is an empty bitstring (word), it contains zero bits! o adds a 0 to the bitstring and i adds a 1 to the bitstring. Both of these constructors add 1 bit to the bitstring so the "size" increases with 1 (using the suc constructor of Nat).

This is an indexed datatype (also known as an inductive family or a Generalized Algebraic Datatype). In this case the datatype is indexed by a Nat. You can see that each constructor may give a different value for the Nat. This allows you to gain knowledge about the instance of the datatype by looking at the index (or by pattern matching). For example you know that a w : Word zero must be an e, because none of the other constructors allow a zero for the index!