I have no idea how to read or make sense of these definitions. I mean semantically and grammatically. What should I read if I want to understand those snippets and how/why they do define what an addition is?
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.
https://twitter.com/afsofia_/status/1105913438650486784