What About the Natural Numbers by José Manuel Calderón Trilla

30 years ago Colin Runciman asked What About the Natural Numbers? Now, in 2019, we find ourselves in need of a successor to carry Runciman's banner. Despite major advances in type systems and the growing adoption of the slogan 'make illegal states unrepresentable', we often rely on Integers in cases where negative values have no meaning. Runciman's paper reminds us of a fact that we all know: the choice in types can change the nature of an API. Integers are often the default in many systems and APIs, often for no reason beyond programmer familiarity. In this talk we will argue two main points: that for many cases Natural numbers retain all of the positive aspects of the Integers with none of the negatives, and that when designing a system or an API we should constantly be asking ourselves "What about X?"

Transcript

1. What About the Natural Numbers? JMCT
2. N
3. N?
4. “Some thirty years into the history of machine-independent programming language design, the treatment of numbers is still problematic.” — Colin Runciman, 1989
5. “Some sixty years into the history of machine-independent programming language design, the treatment of numbers is still problematic.” — Me, just now
6. Main takeaway The number system we use should relate to the structures of the problem we’re solving.
7. Main takeaway For some domains, the use of Reals1 may be appropriate: 1or their approximation via Floats
8. Main takeaway For some domains, the use of Reals1 may be appropriate: e.g. physics calculations involving volume, speed, or mass 1or their approximation via Floats
9. Main takeaway For many problems Integers are appropriate:
10. Main takeaway For many problems Integers are appropriate: Fixed-precision DSP
11. Main takeaway For many problems Integers are appropriate: Fixed-precision DSP Bank account balance :’(
12. Main takeaway Runciman’s argument: For many of the discrete structures involved in the day-to-day practice of programming, the natural numbers are the most appropriate number system.
13. How? In the process of exploring the Natural Numbers, we’ll be developing an API. As we progress we’ll see how different representations affect our API.
14. #goals
15. #goals 1. Show you that the [lazy?] Ns are Good and Proper
16. #goals 1. Show you that the [lazy?] Ns are Good and Proper 2. Demonstrate that even simple choices of types for an API have deep consequences
17. #goals 1. Show you that the [lazy?] Ns are Good and Proper 2. Demonstrate that even simple choices of types for an API have deep consequences 3. Have you asking “What about the Natural Numbers?” next time you create an API.
18. Shape of things to come
19. Shape of things to come 1. Overview of the Ns themselves
20. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat
21. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about
22. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design?
23. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns
24. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat
25. Shape of things to come 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
26. Let’s start 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
27. What are they? The Natural numbers have a few definitions:
28. What are they? The Natural numbers have a few definitions: 1. Set Theoretic
29. What are they? The Natural numbers have a few definitions: 1. Set Theoretic 2. Peano Axioms
30. Setting Yourself Up For Success
31. Setting Yourself Up For Success Several possible Set-theoretic definitions, von Neumann proposed the following:
32. Setting Yourself Up For Success Several possible Set-theoretic definitions, von Neumann proposed the following: 0 = {}
33. Setting Yourself Up For Success Several possible Set-theoretic definitions, von Neumann proposed the following: 0 = {} 1 = 0 ∪ {0}
34. Setting Yourself Up For Success Several possible Set-theoretic definitions, von Neumann proposed the following: 0 = {} 1 = 0 ∪ {0} 2 = 1 ∪ {1}
35. Setting Yourself Up For Success Several possible Set-theoretic definitions, von Neumann proposed the following: 0 = {} 1 = 0 ∪ {0} = {0} = {{}} 2 = 1 ∪ {1} = {0, 1} = {{}, {{}}}
36. Setting Yourself Up For Success oof
37. Setting Yourself Up For Success In 1889 Giuseppe Peano published “The principles of arithmetic presented by a new method”
38. Setting Yourself Up For Success The two axioms we care about most (right now) are simple enough:
39. Setting Yourself Up For Success The two axioms we care about most (right now) are simple enough: 0 ∈ N
40. Setting Yourself Up For Success The two axioms we care about most (right now) are simple enough: 0 ∈ N ∀n ∈ N. S(n) ∈ N
41. Sign post 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
42. Setting Yourself Up For Success Okay, but we’re concerned with the practice of programming . . .
43. Setting Yourself Up For Success type Nat where Z : Nat Succ : Nat -> Nat
44. Setting Yourself Up For Success Now we can easily represent any N we want!
45. Setting Yourself Up For Success Now we can easily represent any N we want! Z = 0 Succ n = 1 + n
46. Talk over?
47. Talk over? This is all very nice and elegant, but the ergonomics suck
48. RSI risk Even just typing this slide made my RSI flare up: 3 ⇒ Succ (Succ (Succ Z)) 11 ⇒ Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (S
49. Spoonful of sugar What do we do for other types?
50. Spoonful of sugar type List elem where [] : List elem (::) : elem -> List elem -> List elem
51. Spoonful of sugar Lists are flexible and easy to reason about, but they have the same problem!
52. Spoonful of sugar Lists are flexible and easy to reason about, but they have the same problem! type String = List Char
53. Spoonful of sugar Lists are flexible and easy to reason about, but they have the same problem! type String = List Char initials = ’P’ :: (’W’ :: (’L’ :: []))
54. Spoonful of sugar Because of this ubiquity of lists, compiler writers quickly came up with syntactic sugar for them:
55. Spoonful of sugar Because of this ubiquity of lists, compiler writers quickly came up with syntactic sugar for them: "PWL" ⇒ ’P’ :: (’W’ :: (’L’ :: []))
56. Spoonful of sugar Because of this ubiquity of lists, compiler writers quickly came up with syntactic sugar for them: "PWL" ⇒ ’P’ :: (’W’ :: (’L’ :: [])) [1..3] ⇒ 1 :: (2 :: (3 :: []))
57. Spoonful of sugar Similarly, we can implement syntactic sugar for the natural numbers:
58. Spoonful of sugar Similarly, we can implement syntactic sugar for the natural numbers: 3 ⇒ Succ (Succ (Succ Z))
59. Spoonful of sugar We lose nothing with the syntactic sugar, we can still pattern match on naturals and retain all of our inductive reasoning.
60. Natural usage ... if length xs <= 5 then ... else ...
61. Pattern Matching still available... (<=) : Nat -> Nat -> Bool Z _ = True (Succ _) Z = False (Succ x) (Succ y) = x <= y
62. Sign post 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
63. Reading, Writing and ...
64. Reading, Writing and ... 1. Programmers expect some arithmetic ‘out of the box’ when dealing with numbers.
65. Reading, Writing and ... 1. Programmers expect some arithmetic ‘out of the box’ when dealing with numbers. 2. At the very least they expect +, −, ×, ÷
66. Real data structures When programming with the discrete structures which are common in programming, there is a correspondence between the operations on numbers and the operations on the data structures.
67. Real data structures When programming with the discrete structures which are common in programming, there is a correspondence between the operations on numbers and the operations on the data structures. 1. Think ‘array indices’, or ‘size’
68. Real data structures When programming with the discrete structures which are common in programming, there is a correspondence between the operations on numbers and the operations on the data structures. 1. Think ‘array indices’, or ‘size’ 2. What would a negative size mean?
69. Who would even do that?
70. Who would even do that? Figure: lol
71. Exceptional negatives Think of how many APIs return an “Int”.
72. Exceptional negatives Think of how many APIs return an “Int”. 1. How many of these APIs only use the negative numbers to signal errors?
73. What do we want? If we think a bit about arithmetic we may conclude the following:
74. What do we want? If we think a bit about arithmetic we may conclude the following: 1. Ideally, our operators would be total
75. What do we want? If we think a bit about arithmetic we may conclude the following: 1. Ideally, our operators would be total 2. When possible, we want our operators to be closed
76. Why? These properties, when combined, allow us to be confident that when we operate on two Nats, we get another Nat.
77. Why? These properties, when combined, allow us to be confident that when we operate on two Nats, we get another Nat. 1. This isn’t true for arithmetic over all number systems (nor should it be!)
78. Why? These properties, when combined, allow us to be confident that when we operate on two Nats, we get another Nat. 1. This isn’t true for arithmetic over all number systems (nor should it be!) 2. Many languages fail even where it should be!
79. Totality Our functions being total gives us confidence that for any input, we get a result.
80. Closure Our functions being closed means that the result values lie within the same number system as their arguments.
81. What do we want? (part 2) “The aim is a total closed system of arithmetic with results that can be safely interpreted in the context of the discrete structures in general programming” — Colin Runciman, 1989
82. Back to arithmetic Addition and Multiplication present no difficulties.
83. Back to arithmetic What about Subtraction?
84. Don’t wait, saturate
85. Don’t wait, saturate (.-.) : Nat -> Nat -> Nat n .-. Z = n Z .-. _ = Z (Succ n) .-. (Succ m) = n .-. m
86. Relate back to data structures
87. Relate back to data structures drop : Nat -> List a -> List a drop Z xs = xs drop _ [] = [] drop (Succ n) (x::xs) = drop n xs
88. Relate back to data structures We want a correspondence between operations on data structures and on numbers: length (drop n xs) === length xs .-. n
89. Relate back to data structures These sorts of correspondences are what we use (often in our head) when programming or refactoring.
90. A divisive issue Unlike Subtraction, division is already closed over Natural Numbers
91. A divisive issue Unlike Subtraction, division is already closed over Natural Numbers (for the cases for which it is defined!)
92. Back to square zero Some mathematicians define the Natural Numbers as starting from One! Would that save us from this issue?
93. Back to square zero Maybe, but then we’d lose the important correspondence with real data structures.
94. Quick digression
95. Quick digression Zero is not nothing!
96. Two solutions Runciman proposes two solutions to the ‘division by zero’ problem:
97. Two solutions Runciman proposes two solutions to the ‘division by zero’ problem: 1. based on viewing division on Ns as ‘slicing’
98. Two solutions Runciman proposes two solutions to the ‘division by zero’ problem: 1. based on viewing division on Ns as ‘slicing’ 2. based on using lazy Nats
99. Division as slicing Think of dividing x by y as cutting x in y places.
100. Division as slicing We can write a total division, //, in terms of a partial (fails when dividing by zero) division, /:
101. Division as slicing We can write a total division, //, in terms of a partial (fails when dividing by zero) division, /: x // y = x / (Succ y)
102. Umm... We get one intuitive property
103. Umm... We get one intuitive property Slicing zero times gets you the original thing back
104. ... that’s wrong At the cost of it being incorrect at every other Nat
105. Let’s fix it We get back correctness by subtracting 1 from the divisor before passing it // x ./. y = x // (y .-. 1)
106. You coward!
107. You coward! In a sense we’ve only side-stepped the problem!
108. You coward! In a sense we’ve only side-stepped the problem! If you think this is the lazy solution...
109. Even lazier Runciman proposes another solution to this problem:
110. Even lazier Runciman proposes another solution to this problem: Lazy Natural Numbers
111. Lazy Nats If we’re in a lazy language we can have infinite structures!
112. Go infinity... If we’re in a lazy language we can have infinite structures! infinity = Succ infinity
113. Back to division x ./. 0 = infinity x ./. y = x / y
114. No cheating
115. No cheating x ./. y = if x < y then 0 else Succ ((x .-. y) ./. y)
116. More power to you Exponentiation is not closed over the Integers, but over Naturals it is!
117. More power to you Exponentiation is not closed over the Integers, but over Naturals it is! pow n 0 = 1 pow n (Succ p) = n * pow n p
118. Laziness, revisited Let’s not start a war here
119. Laziness, revisited Infinite values also allow you to avoid ‘cheating’ in some standard algorithms
120. Laziness, revisited How many times have you seen inf = 999999 in a graph algorithm?
121. Save yourself some computation Are there more than 10 people in your company?
122. Save yourself some computation Are there more than 10 people in your company? ... expensive > 10 ...
123. Laziness, revisited Lazy numbers let us compare the sizes of things without necessarily fully computing the size!
124. Sign post 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
125. APIs We’ve alredy defined an API for arithmetic, with various tradeoffs.
126. APIs We’ve alredy defined an API for arithmetic, with various tradeoffs. 1. Now let’s define some non-arithmetic functions and see how the Nats guide us
127. Size Size of structures is very straightforward
128. Size size : List elem -> Nat size [] = Z size (x::xs) = Succ (size xs)
129. Position/Index Finding the index of a thing is a little more interesting
130. Position/Index: Mark 1 position : elem -> List elem -> ??????????
131. Position/Index: Mark 1 position : elem -> List elem -> ?????????? position a xs = pos xs 0 where pos (x::xs) n =
132. Position/Index: Mark 1 position : elem -> List elem -> ?????????? position a xs = pos xs 0 where pos (x::xs) n = if a == x then n else pos xs (Succ n)
133. Position/Index: Mark 1 position : elem -> List elem -> ?????????? position a xs = pos xs 0 where pos (x::xs) n = if a == x then n else pos xs (Succ n) pos [] n = ????
134. Position/Index: Mark 1 position : elem -> List elem -> Option Nat position a xs = pos xs 0 where pos (x::xs) n = if a == x then Some n else pos xs (Succ n) pos [] n = None
135. Thoughts: Mark 1 This is satisfying because we’re explicit about the possibility of failure
136. Position/Index: Mark 2 It should really be positions!
137. Position/Index: Mark 2 It should really be positions! positions : elem -> List elem -> List Nat positions a xs = pos xs 0 where pos (x::xs) n = if a == x then n :: pos xs (Succ n) else pos xs (Succ n) pos [] n = []
138. Thoughts: Mark 2 In a lazy language positions is strictly more flexible
139. Thoughts: Mark 1 & 2 Mind the gap
140. Thoughts: Mark 1 & 2 Mind the gap There were none!
141. sublist Take the sublist of a list: sublist m n = take (n - m+1) . drop m
142. sublist The sublist function has invariants that the user has to keep in mind sublist m n = take (n - m+1) . drop m
143. sublist The sublist function has invariants that the user has to keep in mind sublist m n = take (n - m+1) . drop m What if n < (m-1)?
144. sublist The sublist function has invariants that the user has to keep in mind sublist m n = take (n - m+1) . drop m What if n < (m-1)? take would be passed a negative argument!
145. sublist Fix is straightforward sublist : Nat -> Nat -> List elem -> List elem sublist 0 n = take n sublist (Succ m) n = take (n .-. m) . drop (Succ m)
146. Sign post 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
147. Issues Why don’t we see Nats everywhere?
148. Issues Why don’t we see Nats everywhere? Language designers don’t include them in the stdlibs
149. Issues Why don’t we see Nats everywhere? Language designers don’t include them in the stdlibs Concerns about performance
150. Interesting observation Even languages that try to have some sort of non-negative number end up tripping over themselves!
151. Interesting observation Even languages that try to have some sort of non-negative number end up tripping over themselves! e.g. C with size t and ssize t
152. I’m not making this up
153. ♥
154. :’(
155. Reality check This person is not wrong!
156. Reality check This person is not wrong! understanding the behavior of casts (especially implicit ones) is hard!
157. Is all hope lost? The issue is twofold:
158. Is all hope lost? The issue is twofold: Unsigned values can be coerced away
159. Is all hope lost? The issue is twofold: Unsigned values can be coerced away Programmers aren’t forced to recon with 0!
160. All hope is not lost Some languages do it right!
161. All hope is not lost Some languages do it right! Idris and Agda compile Peano Nats to machine words
162. What about the lazy Nats? There are issues with implementing the lazy Nats
163. What about the lazy Nats? There are issues with implementing the lazy Nats Lazy languages can have poor memory usage if lazy structures are implemented naively
164. What about the lazy Nats? What are the alternatives?
165. What about the lazy Nats? What are the alternatives? 1. a machine number
166. What about the lazy Nats? What are the alternatives? 1. a machine number 2. an unevaluated computation (i.e. a thunk)
167. What about the lazy Nats? What are the alternatives? 1. a machine number 2. an unevaluated computation (i.e. a thunk) 3. a pair (m,n) of machine number and thunk
168. Why not machine?
169. Why not machine? 1. Suitable for eager languages (IMO)
170. Why not machine? 1. Suitable for eager languages (IMO) 2. We lose infinity in lazy languages
171. Why not thunks?
172. Why not thunks? 1. Uses O(n) space
173. Why not thunks? 1. Uses O(n) space 2. where n is the value of the Nat!
174. Perfect pair? This leaves some combination of machine number and thunk
175. Perfect pair? This leaves some combination of machine number and thunk 1. Static analyses can help make it more efficient
176. Perfect pair? This leaves some combination of machine number and thunk 1. Static analyses can help make it more efficient 2. ‘dirty’ implementation techniques can be hidden from the user
177. Sign post 1. Overview of the Ns themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about 4. How does Nat influence API design? 5. Implementation concerns 6. Beyond Nat 7. Conclude
178. What else
179. What else 1. Sets!
180. Consider the following:
181. Consider the following: 1. A function from an API you’re using returns a List
182. Consider the following: 1. A function from an API you’re using returns a List 2. Does order matter?
183. Consider the following: 1. A function from an API you’re using returns a List 2. Does order matter? 3. What does a duplicate element signal?
184. Mind the gap!
185. Mind the gap! 1. What if the same function returned a Set?
186. Mind the gap! 1. What if the same function returned a Set? 2. No order in the representation
187. Mind the gap! 1. What if the same function returned a Set? 2. No order in the representation 3. No duplicate elements
188. Picking up the signals
189. Picking up the signals 1. Every data structure is signaling something
190. Picking up the signals 1. Every data structure is signaling something 2. Asking the consumers of your API to ignore a signal only serves to increas the cognitive burden of your API
191. Picking up the signals 1. Every data structure is signaling something 2. Asking the consumers of your API to ignore a signal only serves to increas the cognitive burden of your API 3. Try choosing structures that are necessary and sufficient
192. Picking up the signals 1. Every data structure is signaling something 2. Asking the consumers of your API to ignore a signal only serves to increas the cognitive burden of your API 3. Try choosing structures that are necessary and sufficient 4. This way, all signals are meant to be heeded
193. Closing thoughts
194. Closing thoughts No one seems to disagree, and yet...
195. Ahead of his time
196. Ahead of his time “The benefits of lazy evaluation generally are now widely recognised (though still regarded as controversial by some)” — Colin Runciman, The year of TS’s birth
197. Smash that subscribe button Thanks for your time! You can read more of my rants @josecalderon
198. N!