The first confusing thing is the type signatures. Concatenative languages pass everything around with a stack so here the double dash separates a top part of the stack before application from what the application of the word transforms that bit of the stack into, so:

  succ : Nat -- Nat

means that if you can prove there is a Nat, n on the top of the stack, you can do succ to replace that with a Nat, succ n. Similarly we have:

  + : Nat Nat -- Nat

Which says if you have two Nats on the top of the stack you can do + to get a single Nat.

The next weird thing is pattern matching. + is defined with two cases. The first is:

  zero + = id

Which makes some sense: to add zero to x, do nothing. Making up a variable syntax it would look like:

  <x> zero + = <x>

The pattern matching on the next line is harder:

  succ + = + succ

Which (making up syntax again) says that if your stack looks like:

  m n

And n = succ k:

  m (succ k)

And you do +, you “unapply” succ to get a “stack” that looks like:

  m k succ

With the application of + shown:

  m k succ +

And this matches the pattern above so we transform:

  m k + succ

And evaluate:

  (m+k) succ
  (m+k+1)
  (m+n)

I think this is a rough idea of how the basic types work:

  Denote a “stack” of types (e.g. Nat Nat above) as [a], and single types a.
  If e : [a] -- [b] then for any [c], e : [c] [a] -- [c] [b]
  If dashes are omitted from a type a, it is the same as the type -- a (ie [b] -- [b] a for any [b])
  If e : [a] -- [b] and f : [b] -- [c] then e f : [a] -- [c]

  To define a word w : [a] -- [b], e w = f is a valid clause if:
  1. e has type [c] -- [a]
  2. f has type [c] -- [b]
  3. e is a valid pattern (ie made out of constructors (?))

I guess the rest of the typing rules are more complicated.

The syntax is a bit peculiar, but they defined the union type Nat, defined the function + which takes two Nats and returns a Nat (which they defined in a thoroughly confusing point-free way because the language is concatenative), and demonstrated the associativity of +.

If you read any introduction to dependent types, they will do this.

Ok, now I get it... I was just lost in the syntax.