4 ms·

Some examples here: https://twitter.com/afsofia_/status/1105913438650486784 https://twitter.com/afsofia_/status/1105913438650486784

nudpiedo 7y ago
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?
- Smaug123 7y ago
  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.
  - nudpiedo 7y ago
    Ok, now I get it... I was just lost in the syntax.
- dan-robertson 7y ago
  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.

nudpiedo 7y ago

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?

Smaug123 7y ago
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.
- nudpiedo 7y ago
  Ok, now I get it... I was just lost in the syntax.
dan-robertson 7y ago
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.