Upgrade to Pro — share decks privately, control downloads, hide ads and more …

What About the Natural Numbers by José Manuel C...

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?"

Papers_We_Love

September 12, 2019
Tweet

More Decks by Papers_We_Love

Other Decks in Programming

Transcript

  1. N

  2. N?

  3. “Some thirty years into the history of machine-independent programming language

    design, the treatment of numbers is still problematic.” — Colin Runciman, 1989
  4. “Some sixty years into the history of machine-independent programming language

    design, the treatment of numbers is still problematic.” — Me, just now
  5. Main takeaway The number system we use should relate to

    the structures of the problem we’re solving.
  6. Main takeaway For some domains, the use of Reals1 may

    be appropriate: 1or their approximation via Floats
  7. 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
  8. 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.
  9. 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.
  10. #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
  11. #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.
  12. Shape of things to come 1. Overview of the Ns

    themselves 2. Programming with Nat
  13. Shape of things to come 1. Overview of the Ns

    themselves 2. Programming with Nat 3. Arithmetic with Nat and properties we care about
  14. 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?
  15. 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
  16. 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
  17. 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
  18. 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
  19. Setting Yourself Up For Success Several possible Set-theoretic definitions, von

    Neumann proposed the following: 0 = {} 1 = 0 ∪ {0}
  20. Setting Yourself Up For Success Several possible Set-theoretic definitions, von

    Neumann proposed the following: 0 = {} 1 = 0 ∪ {0} 2 = 1 ∪ {1}
  21. 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} = {{}, {{}}}
  22. Setting Yourself Up For Success In 1889 Giuseppe Peano published

    “The principles of arithmetic presented by a new method”
  23. Setting Yourself Up For Success The two axioms we care

    about most (right now) are simple enough:
  24. Setting Yourself Up For Success The two axioms we care

    about most (right now) are simple enough: 0 ∈ N
  25. Setting Yourself Up For Success The two axioms we care

    about most (right now) are simple enough: 0 ∈ N ∀n ∈ N. S(n) ∈ N
  26. 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
  27. 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
  28. Spoonful of sugar type List elem where [] : List

    elem (::) : elem -> List elem -> List elem
  29. Spoonful of sugar Lists are flexible and easy to reason

    about, but they have the same problem!
  30. Spoonful of sugar Lists are flexible and easy to reason

    about, but they have the same problem! type String = List Char
  31. 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’ :: []))
  32. Spoonful of sugar Because of this ubiquity of lists, compiler

    writers quickly came up with syntactic sugar for them:
  33. Spoonful of sugar Because of this ubiquity of lists, compiler

    writers quickly came up with syntactic sugar for them: "PWL" ⇒ ’P’ :: (’W’ :: (’L’ :: []))
  34. 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 :: []))
  35. Spoonful of sugar Similarly, we can implement syntactic sugar for

    the natural numbers: 3 ⇒ Succ (Succ (Succ Z))
  36. Spoonful of sugar We lose nothing with the syntactic sugar,

    we can still pattern match on naturals and retain all of our inductive reasoning.
  37. Pattern Matching still available... (<=) : Nat -> Nat ->

    Bool Z _ = True (Succ _) Z = False (Succ x) (Succ y) = x <= y
  38. 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
  39. Reading, Writing and ... 1. Programmers expect some arithmetic ‘out

    of the box’ when dealing with numbers. 2. At the very least they expect +, −, ×, ÷
  40. 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.
  41. 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’
  42. 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?
  43. Exceptional negatives Think of how many APIs return an “Int”.

    1. How many of these APIs only use the negative numbers to signal errors?
  44. What do we want? If we think a bit about

    arithmetic we may conclude the following:
  45. What do we want? If we think a bit about

    arithmetic we may conclude the following: 1. Ideally, our operators would be total
  46. 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
  47. Why? These properties, when combined, allow us to be confident

    that when we operate on two Nats, we get another Nat.
  48. 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!)
  49. 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!
  50. Closure Our functions being closed means that the result values

    lie within the same number system as their arguments.
  51. 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
  52. Don’t wait, saturate (.-.) : Nat -> Nat -> Nat

    n .-. Z = n Z .-. _ = Z (Succ n) .-. (Succ m) = n .-. m
  53. Relate back to data structures drop : Nat -> List

    a -> List a drop Z xs = xs drop _ [] = [] drop (Succ n) (x::xs) = drop n xs
  54. Relate back to data structures We want a correspondence between

    operations on data structures and on numbers: length (drop n xs) === length xs .-. n
  55. Relate back to data structures These sorts of correspondences are

    what we use (often in our head) when programming or refactoring.
  56. A divisive issue Unlike Subtraction, division is already closed over

    Natural Numbers (for the cases for which it is defined!)
  57. Back to square zero Some mathematicians define the Natural Numbers

    as starting from One! Would that save us from this issue?
  58. Back to square zero Maybe, but then we’d lose the

    important correspondence with real data structures.
  59. Two solutions Runciman proposes two solutions to the ‘division by

    zero’ problem: 1. based on viewing division on Ns as ‘slicing’
  60. 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
  61. Division as slicing We can write a total division, //,

    in terms of a partial (fails when dividing by zero) division, /:
  62. 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)
  63. Let’s fix it We get back correctness by subtracting 1

    from the divisor before passing it // x ./. y = x // (y .-. 1)
  64. You coward! In a sense we’ve only side-stepped the problem!

    If you think this is the lazy solution...
  65. Go infinity... If we’re in a lazy language we can

    have infinite structures! infinity = Succ infinity
  66. No cheating x ./. y = if x < y

    then 0 else Succ ((x .-. y) ./. y)
  67. More power to you Exponentiation is not closed over the

    Integers, but over Naturals it is!
  68. 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
  69. Save yourself some computation Are there more than 10 people

    in your company? ... expensive > 10 ...
  70. Laziness, revisited Lazy numbers let us compare the sizes of

    things without necessarily fully computing the size!
  71. 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
  72. 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
  73. Size size : List elem -> Nat size [] =

    Z size (x::xs) = Succ (size xs)
  74. Position/Index: Mark 1 position : elem -> List elem ->

    ?????????? position a xs = pos xs 0 where pos (x::xs) n =
  75. 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)
  76. 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 = ????
  77. 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
  78. 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 = []
  79. sublist The sublist function has invariants that the user has

    to keep in mind sublist m n = take (n - m+1) . drop m
  80. 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)?
  81. 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!
  82. 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)
  83. 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
  84. Issues Why don’t we see Nats everywhere? Language designers don’t

    include them in the stdlibs Concerns about performance
  85. Interesting observation Even languages that try to have some sort

    of non-negative number end up tripping over themselves!
  86. 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
  87. Reality check This person is not wrong! understanding the behavior

    of casts (especially implicit ones) is hard!
  88. Is all hope lost? The issue is twofold: Unsigned values

    can be coerced away Programmers aren’t forced to recon with 0!
  89. All hope is not lost Some languages do it right!

    Idris and Agda compile Peano Nats to machine words
  90. 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
  91. What about the lazy Nats? What are the alternatives? 1.

    a machine number 2. an unevaluated computation (i.e. a thunk)
  92. 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
  93. Perfect pair? This leaves some combination of machine number and

    thunk 1. Static analyses can help make it more efficient
  94. 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
  95. 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
  96. Consider the following: 1. A function from an API you’re

    using returns a List 2. Does order matter?
  97. 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?
  98. Mind the gap! 1. What if the same function returned

    a Set? 2. No order in the representation
  99. Mind the gap! 1. What if the same function returned

    a Set? 2. No order in the representation 3. No duplicate elements
  100. 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
  101. 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
  102. 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
  103. 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
  104. Smash that subscribe button Thanks for your time! You can

    read more of my rants @josecalderon
  105. N!