The first thing to know about Haskell and set theory is, yes, we can do real set theory with Haskell’s Data.Set package. But as beginners learning the ropes we will start with a simpler representation of sets through Haskell’s basic list data structure. Realize, however, that a list is not a set; they are two different beasts, and we’ll have to account for that. For one, a set may have duplicates, whereas a list holds a definite sequence of things, i.e., every element of the list is unique, even if some elements are repeated So it’s not really a “grocery list,” it’s a “grocery set” since \(\{eggs,sugar,coffee,eggs\}\;\;\;\) is invariably interpreted as just \(\{eggs,sugar,coffee\}\;\;\), right? Or would you go ahead and get eggs twice? . So the set \(\{1,2,1\}\;\) is the same as \(\{1,2\}\;\) is the same as \(\{2,1,1\}\;\) because sets don’t mind duplicates, nor do they worry about order Why is this? There is a LE to the definition of a set union, namely, \(A \cup B = \{x \;\;|\;\; x \in A \;\;\;or\;\;\; x \in B \}\quad\). Consider the sets \(A = \{1,2,3\}\;\), \(B = \{2,3,4\}\;\), and \(C = \{3,4,5\}\;\). If you draw out Their union \(A \cup B \cup C = \{x \;|\; x \in A \;\;\text{or}\;\;x \in B\;\; \text{or}\;\;x \in C \}\quad\;\;\) as a Venn diagram, you’ll see how duplicates get left out. . But the lists [1,2,1], [1,2], and [2,1,1] are in fact all different lists. Initially, we’ll practice set theory with lists and build alternate set theory code based on lists. Then when we understand “squirrel math” a little more, i.e., how to work with the data structures known as trees, we’ll do proper set theory with Haskell’s set theory module, Data.Set Take a look at this Hackage page. It has a nice little intro to Haskell’s sets. Get in the habit of perusing Hackage whenever you’re using a Haskell function or data type you don’t quite understand. Sometimes you’ll have to just dive into the code, but sometimes there are excellent intro docs like this. . For the immediate future we’ll consider a list to be a beginner’s substitute for a set. And so a simple “how many” function on a list standing in for a set is length

length [1,2,3,4,5]

5

Again, more excitement to come. Watch this space.

Haskell is a typed language with a feature called type classes For a quick introduction with examples go here in LYAHFGG. . A Haskell type class encompasses traits, patterns, concepts, or what we might call a certain “-ness” that can be imparted to data types. In Haskell, for example, numbers and the characters of the alphabet can be directly compared for “equal-ness,” and when we test at the ghci REPL prompt, this seems to be built-in

((5 == 3) || ('a' == 'a')) || ('b' == 'B')

True

Mindful of LE, we see that Haskell’s Eq class housing this equal-ness must have some sort of behind-the-scenes mechanism that allows us to take two things, analyze them, then return a decision, true or false (yes they are equal, no they’re not equal), on whether two said things were equal or not — all of this just for doing some typing, e.g., 5 == 3 into the REPL.

Something else to consider is how some things don’t necessarily have the concept of equal or not equal straight out of the box. What if we created a data type for colors and we wanted to compare the individual color values for equal-ness? Intuitively, we might say red, yellow, and blue are equal since they are all primary colors; likewise, orange, green, and violet are equal because they’re the secondary colors. But what if we just say each color is equal to itself and not equal to any of the others? … So how would we establish equal-ness for colors? If we want to type Green == Blue into the REPL it’s up to us to have created some sort of equal-ness and told Haskell about it.

Data types that need to establish equal-ness for themselves can apply to the Haskell Eq type class for membership. Type class membership is registered with an instance statement. To see all the data types that have an instance registered with Eq we can use :info (abbreviated :i) at the REPL Go ahead and check out the hackage.haskell.org entry for Eq here. Note the properties (==) should follow: reflexivity, symmetry, transitivity, extentionality, and negation. We’ll dive into what this all means when we look closer into the higher algebra of sets and functions. Note all the built-in, “batteries-included” Eq instances for the various types. Some are rather exotic.

:i Eq

type Eq :: * -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  {-# MINIMAL (==) | (/=) #-}
  	-- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
...
instance Eq Int -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Eq Float -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Eq Double -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Eq Char -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Eq Bool -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
...

which gives us a long list (abbreviated above) of data types that have equal-ness defined Quick LE question: Can functions be compared for equal-ness? Here’s a direct quote from a prominent combinatorics text: When two formulas enumerate the same set, then they must be equal. But not so fast in the computer world. To say f x == g x Haskell isn’t logically set up to actually prove (demonstrate) and accept that f and g always give the same results given the same x input. We would literally have to test every possible x, which is not possible. Still, we’ll examine this idea a bit closer soon. It’s a real big deal in numerical math. . Notice the two “prescribed” methods (functions) (==) and (/=). These functions are the mechanism used by Eq to establish equal-ness. They must be custom defined in each instance declaration in order for a data type to have its own established equal-ness Note {-# MINIMAL (==) | (/=) #-} which is a directive meaning we may choose to define either (==) or (note the or pipe | ) (/=), i.e., we don’t actually have to define both because by defining one, the other will be automatically generated. Neat. . And so if you create a new type, you, the programmer, must come up with your own version of these two functions, (==) and (/=) to establish the trait, the property of equal-ness for that new data type. As LYAHFGG notes, the type signature for the equal-ness function (==) is :t is short for :type.

:t (==)

(==) :: Eq a => a -> a -> Bool

which indicates (==) takes two inputs of some type a and returns a Bool type, i.e., either True or False. Good, we saw how that works with our examples above. But there’s another wrinkle to this story. So if (==) is a function that takes two objects of type a, e.g., two integers, real numbers, characters, booleans, etc., how can we use this same symbol (==) in so many different contexts? Looking above, how did Haskell know to use integer equal-ness rules (defined by instance Eq Int) when comparing integers, and then letter equal-ness rules (defined by instance Eq Char) when comparing letters? This feat is what we call ad hoc polymorphism ad hoc, from Latin to this, is something put together on the fly for one narrow, pressing, or special purpose. polymorphic, from Greek polus much, many, and morphism, having the shape, form, or structure, i.e., having many shapes. , which allows just a single function symbol, e.g., (==), to be used (overloaded) in many different contexts. And so Haskell figures out behind the scenes which instance to apply. Neat.

Let’s take a closer look at a color type by defining our own As LYAHFGG says, Read and Show are also type classes to which you may register your data type. Here we’ve used the deriving keyword to let Haskell figure it out, i.e., we’re not defining Read and Show ourselves; rather, we’re telling Haskell to auto-generate and register these instances for us. We’ll go into more detail about declaring our own data types as we progress. But for now we’ll say Color is a sum type, as opposed to a product type. Sum types are patterned after the addition principle which we’ll also go into later. Note, the pipes \(\;|\;\) between the colors can be understood as logical or—as in we must choose one or the other of the colors.

data Color = Red | Yellow | Blue | Green deriving (Show,Read)

Obviously, the colors red, yellow, blue, and green have no intrinsic numerical properties by which to compare one with the other. However, Haskell’s type class system still allows us to create some manner of equal-ness for it. And so we write this version of an instance of Eq for Color

instance Eq Color where
  Red == Red = True      -- could also be (==) Red Red = True
  Yellow == Yellow = True
  Blue == Blue = True
  Green == Green = True
  _ == _ = False         -- anything getting to this point must be false

And so we’ve hand-coded our own equal-ness for Color by spelling out how (==) works for Color. This literally tells Haskell what Color equal-ness should be by customizing how the function (==) should work. Let’s have another look at the type signature for (==)

:t (==)

(==) :: Eq a => a -> a -> Bool

As LYAHFGG notes, the Eq a part is known as a class constraint. This means whatever a might be …and this is an example of parametric polymorphism where the parameter (aka type variable) a can be any data type. In Haskell, smaller-case letters such as a, b, c, etc., are generic parameter names and can indicate any data type. In (==) :: Eq a => a -> a -> Bool we see that two inputs of the same type a are fed to (==), which produces a Bool output. Another example would be myFunc :: a -> b -> a. Here the type signature says the inputs don’t have to be of the same type (although they could be), but no matter what type the parameter b is, the output will be of type a. , it must have an equal-ness instance already registered for it — which we do — otherwise, Haskell won’t know how to compare two things of a for equal-ness For our Color we’ve created our own equal-ness, although in this example we could have let Haskell figure it out, i.e., ...| Green deriving (Eq) would have done the same thing. This was an easy one. Haskell can’t always figure out the less obvious cases. .

(Red == Red) && (Red /= Green)

True

Good, it’s working and we now can compare Color values for equal-ness, but how do we order colors? No matter how we establish one color before the other, it might seem arbitrary, but we can do it if we want. For basic order-ness Haskell has the type class Ord to which types can register

:i Ord

type Ord :: * -> Constraint
class Eq a => Ord a where
  compare :: a -> a -> Ordering
  (<) :: a -> a -> Bool
  (<=) :: a -> a -> Bool
  (>) :: a -> a -> Bool
  (>=) :: a -> a -> Bool
  max :: a -> a -> a
  min :: a -> a -> a
  {-# MINIMAL compare | (<=) #-}
  	-- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
...
instance Ord Ordering -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Int -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Float -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Double -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Char -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Bool -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Ord Integer -- Defined in ‘GHC.Num.Integer’
...

Note how the Ord declaration itself has a class constraint, i.e., Eq a =>. This means any data type a must already have its Eq instance registered. Hence, Eq is a sort of super-class, and yes, type classes can build hierarchies of themselves.

Again, we see Ord has a minimum requirement for order-ness, namely, that we define the method The habit of calling a set of functions associated with a Haskell type class methods might be a hold/spill-over from the world of object-oriented programming where an OOP class will have method functions attached to it. This is called encapsulation, i.e., a system for keeping things that belong together together. However, an OOP class and a Haskell type class are entirely different beasts. So let’s keep our head stuck in the Haskell particle accelerator for now… (function) compare … and then we get all the other order-ness methods, (<) … min for free, as in Haskell is smart enough to figure them out just based on what you gave for compare. Neat In general, anytime your programming language starts writing code for you, it’s cool… .

:t compare

compare :: Ord a => a -> a -> Ordering

The function compare is, like (==), a binary (two inputs) operation that takes inputs of the same data type a and returns something of type Ordering. So what is Ordering? Let’s ask

:i Ordering

type Ordering :: *
data Ordering = LT | EQ | GT
  	-- Defined in ‘ghc-prim-0.7.0:GHC.Types’
instance Eq Ordering -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Monoid Ordering -- Defined in ‘GHC.Base’
instance Ord Ordering -- Defined in ‘ghc-prim-0.7.0:GHC.Classes’
instance Semigroup Ordering -- Defined in ‘GHC.Base’
instance Enum Ordering -- Defined in ‘GHC.Enum’
instance Show Ordering -- Defined in ‘GHC.Show’
instance Read Ordering -- Defined in ‘GHC.Read’
instance Bounded Ordering -- Defined in ‘GHC.Enum’

There’s a lot of information here. Note the data type declaration for Ordering is

...
data Ordering = LT | EQ | GT
...

While the type Bool had two data constructors True and False, Ordering has three — LT, EQ, and GT. Now, let’s write code to register an instance of Ord for Color We make heavy use of the wildcard _ by which we mean any variable can be in the _ position. For example compare Red _ = GT means when we compare Red to anything else, Red will always be greater than it. We also leveraged the order of these declarations, i.e., by having compare Red _ = GT at the very start, Red versus anything will be sorted out first. This is a conditional situation implicitly, which we’ll use lots more.

instance Ord Color where
  compare Red Red = EQ
  compare Red _ = GT
  compare _ Red = LT
  compare Yellow Yellow = EQ
  compare Yellow _ = GT
  compare _ Yellow = LT
  compare Blue Blue = EQ
  compare Blue _ = GT
  compare _ Blue = LT
  compare Green Green = EQ

Again, the Ord type class required us to create our own compare method, which painstakingly we did. Now we can compare two values of Color for order-ness with our basic Ord comparison operators Remember, math operators in Haskell are just a sort of function. Which means (==) Red Red is identical to Red == Red. Haskell requires operators in the function (prefix) position to be in parentheses, whereas in the infix (between) position they can be naked operators. Notice min Red Yellow that min is in the prefix position. Just put back-ticks around it to use it infix: Red `min` Yellow. , >, <, and ==,

((Blue < Green) || (Red == Red)) && (Yellow >= Blue)

True

(min Red Yellow) > (max Blue Green)

True

Now, how many possible combinations of these four colors would we have to make in order to test all possible cases? This is a topic the basics of which we’ll explore later. But here’s a taste of these future endeavors. Perhaps you noticed in LYAHFGG the talk about list comprehensions. These mimic set comprehensions fairly closely

\begin{align*} & C = \{Red,Yellow,Blue,Green \} \\ & \{(x,y) \;|\; x \in C, \;y \in C \} \end{align*}

And in Haskell

cset = [Red,Yellow,Blue,Green]

[ (x,y) | x <- cset, y <- cset]

[(Red,Red),(Red,Yellow),(Red,Blue),(Red,Green),(Yellow,Red),(Yellow,Yellow),(Yellow,Blue),(Yellow,Green),(Blue,Red),(Blue,Yellow),(Blue,Blue),(Blue,Green),(Green,Red),(Green,Yellow),(Green,Blue),(Green,Green)]

Let’s define another color type and simply rely on Haskell’s deriving to create instances for Eq and Ord

data Color2 = Green2 | Blue2 | Yellow2 | Red2 deriving (Show,Read,Eq,Ord)

(Red2 == Red2 && Red2 == Green2)

False

For equal-ness deriving simply made everything equal to itself and not equal to other colors—just like we did before by hand. Then for order-ness deriving simply took the Color2 data constructors in the order they were declared and ranked them in ascending order

((Green2 < Blue2) == (Blue2 < Yellow2)) == (Yellow2 < Red2)

True

:i Color

: type Color :: *
: data Color = Red | Yellow | Blue | Green
:   	-- Defined at omni1.1.hs:29:1
: instance [safe] Eq Color -- Defined at omni1.1.hs:30:10
: instance [safe] Ord Color -- Defined at omni1.1.hs:36:10
: instance [safe] Read Color -- Defined at omni1.1.hs:29:57
: instance [safe] Show Color -- Defined at omni1.1.hs:29:52

data StreetShops a = Grant a | Lee a | Lincoln a deriving (Show,Read)

:k StreetShops

StreetShops :: * -> *

shopsOnGrant = Grant ["Tre Chic","Dollar Chasm","Gofer Burgers"]

shopsOnGrant

Grant ["Tre Chic","Dollar Chasm","Gofer Burgers"]

:t shopsOnGrant

shopsOnGrant :: StreetShops [String]

visitorsOnGrant = Grant 1294

visitorsOnGrant

Grant 1294

:t visitorsOnGrant

visitorsOnGrant :: Num a => StreetShops a

:t 1

1 :: Num p => p

:i Num

type Num :: * -> Constraint
class Num a where
  (+) :: a -> a -> a
  (-) :: a -> a -> a
  (*) :: a -> a -> a
  negate :: a -> a
  abs :: a -> a
  signum :: a -> a
  fromInteger :: Integer -> a
  {-# MINIMAL (+), (*), abs, signum, fromInteger, (negate | (-)) #-}
  	-- Defined in ‘GHC.Num’
instance Num Word -- Defined in ‘GHC.Num’
instance Num Integer -- Defined in ‘GHC.Num’
instance Num Int -- Defined in ‘GHC.Num’
instance Num Float -- Defined in ‘GHC.Float’
instance Num Double -- Defined in ‘GHC.Float’
...

Filling out or enumerating a set often rests on the concept of induction.

The most basic enumeration in Haskell is filling a range of numbers.

Later we’ll go into a more detail about what a function really is, but for now our basic understanding of functions will do. So let’s bring to the idea of one thing succeeding another a successor function \(s(n)\;\). For example, if we start at \(0\), the successor to \(0\) is \(1\;\), or \(s(0) = 1\;\). But if we’re going to be highly abstract and pure about this, we don’t want to rely on the base\(_{10}\) numbers. Instead, we’ll just keep reapplying the successor function \(S\;\) similar to nesting Russian dolls Russian or matryoshka dolls:

\begin{align*} 0 &= 0 \\ 1 &= S(0) \\ 2 &= S(S(0)) \\ 3 &= S(S(S(0))) \\ 4 &= S(S(S(S(0)))) \\ \ldots \end{align*}

Awkward? YMMV Your mileage may vary… . But we have to admit we’ve defined something akin to the natural numbers using just the constant \(0\) and a successor function applied to it. Now, let’s define addition on this system. To do this we’ll use these two identities

\begin{align} x + 0 &= x \\ x + s(y) &= s(x + y) \end{align}

This should cover all possible cases of addition. Testing, let’s add \(1\) and \(2\;\) or \(s(0) + s(s(0))\;\)

\begin{align} s(0) + s(s(0)) &= \\ s(s(0) + s(0)) &= \\ s(s(s(0)) + 0) &= s(s(s(0))) \end{align}

• We apply (2) to (3) to get (4); in effect abstracting \(1+2\;\), the left side of (2), to the successor of \(1+1\;\), the right side of (2).
• But now the inner part of (4), namely \(s(0) + s(0)\;\), resembles (2) allowing us to match the first \(s(0)\) to \(x\) and the second to \(s(y)\), which in turn allows us to rewrite it as \(s(s(0) + 0)\;\).
• But according to (1) \(s(0) + 0 = s(0)\;\;\), leaving \(s(s(0))\;\)
• Including back in the outermost \(s\) we now have \(s(s(s(0)))\;\) our answer.

What have we accomplished with this convoluted method? For one, we’ve reduced the entire idea of the natural numbers, along with adding two of these reimagined natural numbers, to just a small set of symbols, namely

• a constant symbol \(0\)
• variable symbols \(x\) and \(y\)
• and a function symbol \(s\)

And with these four symbols we create statements made of terms built from our symbols as in (1) and (2), e.g., \(x + 0\;\) is term, and \(s(x + y)\;\) is another term. This allows us to state our problem as terms, then rewrite these terms step-by-step as we did above to get to a final term rewrite that is our answer. And so we have a term rewriting system that provides addition of our natural numbers Rewriting is basically what you do when you, e.g., take steps to simplify or reduce a fraction. More on normal or canonical forms later. . As Madhavan Mukund says &mukund2009lecture

So what’s the alternative? Your modern digital computer creates a human-friendly world of numbers and addition with the help of base\(_{2}\) binary numbers, computer circuit board logic gates, and lots and lots of Assembler code to manage it all. Then come the higher languages which present math as we normally see it, e.g., \(1 + 1 = 2\;\). When seen in this light, we might begin to appreciate a very basic, fundamental fact about modern computing, namely, we can create strategies to accomplish logical calculations by manipulating (rewriting) terms built of symbols. Again, this adds a whole new dimension to our age-old math world mix of scrolls, paper, books, pencils, blackboards and chalk, and those mysterious mental representations of math inside our human brains.

Example of induction: if one domino falls, so will the next.

Simplistic as our natural number system in the previous section may seem, there’s actually quite a bit of math theory to unpack to really understand what just happened. When we build a number up from repeated or nested application of the successor function \(s\) we were using the ideas of induction and recursion You may or may not have encountered induction. Typically, a math course will introduce it as a proof strategy. .

Again, this may seem very simplistic, but the idea of induction is inherent to the natural numbers. So if \(\mathbb{N}\;\) is also referred to as the counting numbers, then we count or enumerate things with them—going up as high as we need to

Table 1: Enumeration of the first ten primes

1	2	3	4	5	6	7	8	9	10
2	3	5	7	11	13	17	19	23	29

Let’s make a quick look-up table in Haskell for Table 1

primeEnum n | (n < 11) && (n > 0) = case (n) of
                          1  -> 2
                          2  -> 3
                          3  -> 5
                          4  -> 7
                          5  -> 11
                          6  -> 13
                          7  -> 17
                          8  -> 19
                          9  -> 23
                          10 -> 29
            | otherwise = error "We only know the first ten primes."
            

primeEnum 9

23

Mathematicians abstracted “the next one” by saying for any \(n \in \mathbb{N}\;\), there will be a \(n+1 \in \mathbb{N}\;\;\) “next one after \(n\;\)”. Myriad phenomena in life and math lend themselves to this “if you’ve got this one, you can get next one” idea.

𝖟𝕭 zB: German abbreviation for zum Beispiel, or for example. : A classic proof using mathematical induction is the proposition Propositions are statements or assertions that can be proven to be either true or false. Make sure you went down this rabbit hole.

\begin{align*} P(n) = 0 + 1 + 2 + 3 + \ldots + n = \frac{n(n+1)}{2} \end{align*}

To be clear, we’re not deriving this formula The story behind this formula is interesting. See this for the backstory. Note the formula is
\begin{align*} \frac{\text{(number of pairs)} ⋅ \text{(sum of each pair)}}{2} \end{align*}
, we’re attempting to prove it. So for example if we add the first three numbers, according to the formula we should get \(6\;\)

\begin{align*} \frac{(3)(3+1)}{2} = \frac{(12)}{2} = 6 \end{align*}

An induction proof is a two-step process: a base case and an induction step

Base case: \(P(0)\)

\(P(0)\;\) is trivial. Just plug in \(0\)

\begin{align*} \frac{(0)(0+1)}{2} = \frac{(0\cdot1)}{2} = 0 \end{align*}

Inductive step: Now we have to consider \(n \gt 0\;\) cases. The whole idea is to show that for any number \(k \ge 0\;\), if \(P(k)\;\) works, so will \(P(k+1)\;\)

We start by assuming what is called the induction hypothesis, i.e., that our statement \(P\) will hold for \(P(n)\;\). Here we’re saying for the unique case when \(n = k\;\) that \(P(k)\;\) is true

\begin{align} 0 + 1 + 2 + \ldots + k = \frac{k(k+1)}{2} \end{align}

Good. Now we want to consider \(P(k+1)\;\). We’ll just add it on both sides since it is the next step after \(k\;\)

\begin{align*} (0 + 1 + 2 + \ldots + k) + (k + 1) = \frac{k(k+1)}{2} + (k+1) \end{align*}

Now, we consider just the right side of this equation and do some algebraic manipulation

\begin{align*} \frac{k(k+1)}{2} + (k+1) &= \frac{k(k+1)}{2} + \frac{2(k+1)}{2} \\ &= \frac{k(k+1)+2(k+1)}{2} &= \frac{(k+1)(k+2)}{2} &= \frac{(k+1)((k+1)+1)}{2} \end{align*}

Going back to our original left-hand side

\begin{align} (0 + 1 + 2 + \ldots + k) + (k + 1) = \frac{(k+1)((k+1)+1)}{2} \end{align}

Now, compare (6) with (7). On the left-hand side of (7) we have the next step \((k+1)\;\) and on the right-hand side of (7) we have in the numerator the “number of pairs” increased from \(k\;\) to \(k+1\;\) and the “sum of each pair” likewise increased by \(1\;\) from \(k+1\) to \(k + 1 + 1\;\). Through algebraic manipulation we have proved that “the next one” will indeed increase as we might want it to. For example, if we total the first ten numbers

\begin{align*} \text{Total sum} = \frac{10 \cdot 11}{2} \end{align*}

and totalling the next number \(11\) will just be

\begin{align*} \text{Total sum} = \frac{11 \cdot 12}{2} \end{align*}

which is covered in our proof for any \(k+1\;\).

We’ll do a Haskell example where Gauss’ summing formula will be of use.

⇲ In a sequence on natural numbers \(1 \ldots n\;\) one of the numbers \(k\;\) is missing, e.g., \(1, \ldots, k-1, k+1, \ldots, n\;\). Find which number it is.

If we have a relatively short list we can no doubt spot it, e.g., \(1,2,4,5\;\); obviously \(3\;\) is missing. But what if our sequence is thousands of numbers long. For example, with Haskell’s list completion we can create a list representing a very big sequence

[1..100]

[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100]

Still doable, but for a sequence going from \(1\) to \(1,000\) it would be hard to spot the missing number. One solution would be to recurse through the list testing each number that it was the next after the previous

:{
missingNumberGen n m | 
:}

:{
missingTest1 xs
:}

For example, what if we add up the first three consecutive odd numbers

Peano postulated axioms, givens, starting points. Using set theory methods, he attempted to

According to a modern treatment, there are five basic Peano axioms Peano actually had nine axioms; however, four of these deal with the equality of his natural numbers, which we’ll deal with later when we explore relations, a more general concept above functions. . The first axiom states

1. \(0\) is a natural number, i.e., \(0 \in \mathbb{N}\)

This is our starting point. Peano then gives four axioms to establish equality

2. For every natural number \(n\), \(S(n)\;\) is a natural number. That is, the natural numbers are closed under \(S\;\). Or \(x \in \mathbb{N} \rightarrow Sx \in \mathbb{N}\;\;\).

1. For all natural numbers x and y, if x = y, then y = x. That is, equality is symmetric.

Turning math into code means we must first decide which data structure to use. For our string of \(1\)’s we will use the Haskell list data structure. This may seem ironic to a budding mathematician who went down the set theory rabbit holes above. Yes, so much of math can be seen as set theory-based. And no, a list is not a set. And yes, Haskell has a library for sets. But as beginners we will simulate sets with lists We could also represent our \(1\)’s as a string, i.e., like text between double-quotes, but any string in Haskell is just a list of the text’s individual characters, e.g., "1111" is really just ['1','1','1','1']. . This means our set of \(1\)’s will be represented as a list with the integer \(1\) repeated as its elements, e.g., [1,1,1,1,1] is \(11111\).

First we’ll try a really primitive way to do UNS subtraction

• Put \(1\)’s into lists,
• Apply the built-in list element counter function, length, on each to count the number of \(1\)’s in each,
• Subtract one from the other.

Not very enlightening, but it works

(length [1,1,1,1]) - (length [1,1])

2

We can write our own function uns1 for this taking two values as input

uns1 list1 list2 = (length list1) - (length list2)

uns1 [1,1,1,1] [1,1]

2

Now, let’s create a better function utilizing Haskell’s type and recursion features

unsSub2 :: [a] -> [a] -> [a]
unsSub2 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsSub2 (l1:l1x) (l2:l2x) = unsSub2 l1x l2x

We’re relying on Haskell’s pattern matching and guards to accomplish loop-like behavior … a lot at once.

It seems to work when the subtrahend is smaller than the minuend

unsSub2 [1,1,1,1,1,1] [1,1,1,1,1]

[1]

unsSub2 [1,1] [1,1]

[]

But the following test exposes a problem, i.e., unsSub2 gets things backwards when the subtrahend is larger than the minuend. This is a logic error, i.e., the code evaluates and runs, but produces bad output

unsSub2 [1,1] [1,1,1,1]

[1,1]

We can correct this by changing the second line 3

1: :{
2: unsSub21 :: [a] -> [a] -> [a]
3: unsSub21 l1x l2x | null l1x = []
4:                 | null l2x = l1x
5: unsSub21 (l1:l1x) (l2:l2x) = unsSub21 l1x l2x
6: :}

Now it works

unsSub21 [1,1,1,1,1] [1,1,1,1,1,1,1]

[]

Another attempt would have us turn any extra \(1\)’s in the minuend turned into \(-1\)’s. No, it’s not exactly UNS, but we’re just practicing here. unsSub3 below should do it, but the first evaluation gives an error Eventually you’ll be a pro with Haskell error messages, but for now we’ll just have to puzzle them out. : There is something wrong with the type declaration.

unsSub3 :: [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x

No instance for (Num a) arising from a use of ‘negate’
  ...

One trick is to simply comment out your type declaration and try again

-- unsSub3 :: [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x

When we allow Haskell to infer the type, we have success.

:t unsSub3

unsSub3 :: Num a => [a] -> [a] -> [a]

Because we’re using negate our list type [a] cannot be just anything, rather, the a’s, the list elements, must be instances of the class Num. Retrying with Haskell’s type declaration

:{
unsSub3 :: Num a => [a] -> [a] -> [a]
unsSub3 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub3 (l1:l1x) (l2:l2x) = unsSub3 l1x l2x
:}

this evaluates. Now

unsSub3 [1,1] [1,1,1,1,1]

[-1,-1,-1]

One improvement would be to make sure our input lists are made up of just ones. For this we have a choice of Haskell built-ins like filter, all, map, any, and elem

list1 = [1,1,1,1]
list2 = [-1,1,1,1,1]

One version using any to test for not equal to 1

any (/=1) list2

True

Another version of testing for not equal to 1 using a (lambda) anonymous function

any (\x -> x /= 1) list2  -- checks if any in the list conform to test

True

We can test two lists by using Boolean or (||)

(any (\x -> x /= 1) list1) || (any (\x -> x /= 1) list2)

True

filter returns a list with elements conforming to the test

filter (/=1) [1,1,1,1]

[]

all checks if all elements conform to test and returns Boolean

all (==1)  [1,1,1,2]

False

map, (see Maps and filters) which we’ll use extensively, applies the test to a list and outputs a new list with the outcomes of each test on each input list element. Here the test is an anonymous function testing again for not equal to 1

map (\x -> (x > 1) || (x < 1)) [-1,1,2,3,4]

[True,False,True,True,True]

elem with type Eq a => a -> [a] -> Bool is not quite as handy since it doesn’t allow for a Boolean predicate test. So yes, we could test if 1 is an element of a list, but not if all are

elem 1 [1,1,1,1] || elem 1 [1,2,3]

True

We can “trick” elem into helping us. First, we produce a list created from map as above testing each element for 1

map (\x -> x /= 1) [1,1,-1,1]

[False,False,True,False]

Then elem will tell us if any elements were not equal to 1

elem True $ map (\x -> x /= 1) [1,1,-1,1]

True

We’ll build in a test using any, but like before, this code doesn’t evaluate properly

unsSub4 :: Num a => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x

The error once again complains of something to do with the elements a of the input arrays

Could not deduce (Eq a) arising from a use of ‘/=’
...
Possible fix:
        add (Eq a) to the context of
          the type signature for:
            unsSub4 :: forall a. Num a => [a] -> [a] -> [a]

Again, we’ll leave out a type declaration and see what Haskell thinks it is

:{
-- unsSub4 :: Num a => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x
:}

:t unsSub4

unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a]

Trying this

:{
unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsSub4 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsSub4 l1x l2x | null l1x = (map negate l2x)
                | null l2x = l1x
unsSub4 (l1:l1x) (l2:l2x) = unsSub4 l1x l2x
:}

and it evaluates. What’s happening? As before, the input element a’s type must also be an instance of the Eq class, which means there has to be a way to equate any pair of a’s

:i Eq

type Eq :: * -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  {-# MINIMAL (==) | (/=) #-}
  	-- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance (Eq a, Eq b) => Eq (Either a b)
  -- Defined in ‘Data.Either’
instance Eq a => Eq [a] -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Word -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Ordering -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
instance Eq Int -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...

What :i or :info is saying about the typeclass Eq is that in order to be an instance of it, input a must have defined what happens when two of its members are subjected to an equality tests (==) and (/=).

Now unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a] restricts a to being a value that has instances for Eq and Num registered. Why is this important? Because without specifying, anticipating the ability to perform equality (Eq) comparisons on only numerical values (Num), other non-numerical values for a might give false output. When we declare the function unsSub4’s input and output types with unsSub4 :: (Eq a, Num a) => [a] -> [a] -> [a], we are guaranteeing sane behavior.

unsSub4 [1,2] [1,1,1,1,1,1]

[]

What will happen if we use lists of strings of 1?

unsSub4 ["1","1"] ["1","1","1","1"]

<interactive>:2516:1-35: error:
    • No instance for (Num [Char]) arising from a use of ‘unsSub4’
    • In the expression: unsSub4 ["1", "1"] ["1", "1", "1", "1"]
      In an equation for ‘it’:
          it = unsSub4 ["1", "1"] ["1", "1", "1", ....]

Again, Haskell is playing it safe. We haven’t made Haskell aware of any way to handle strings as list elements. We use (/=), which will work

'1' /= '2'

True

but we haven’t accounted for negate which wants to negate an actual number. Looking into negate’s type

:t negate

negate :: Num a => a -> a

we see it cannot handle anything but numbers registered with the typeclass Num. So yes, we can use string versions of 1, but that’s because there is a registered instance for Char which defines behind the scenes how to equate numbers

:i Eq

type Eq :: * -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  {-# MINIMAL (==) | (/=) #-}
  	-- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...
instance Eq Char -- Defined in ‘ghc-prim-0.6.1:GHC.Classes’
...

As you saw in LYAHFGG, recursion is the Haskell way of looping. UNS addition, as represented by lists, will be a simple matter of combining two lists of 1’s into one total list. Borrowing from above, we can start out very simple by concatenating the lists

[1,1,1,1] ++ [1,1]

[1,1,1,1,1,1]

uns2 list1 list2 = list1 ++ list2

:{
unsAdd1 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsAdd1 l1x l2x | (any (\x -> x /= 1) l1x) || (any (\y -> y /= 1) l2x) = []
unsAdd1 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd1 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd1 l1x l2x
:}

unsAdd1 [1,1] [1]

[1,1,1]

unsAdd1 gives a nice example of recursion. But what if any of the list elements are negative 1’s? Let’s say if the lists contain -1’s we’ll take away a positive 1. One approach would be to just concatenate both lists, then go through removing positive and negative pairs

:{
unsAdd2 :: (Eq a, Num a) => [a] -> [a] -> [a]
unsAdd2 l1x l2x | ((any (/=1) l1x) && (any (/=(-1)) l1x))
                  || ((any (/=1) l2x) && (any (/=(-1)) l2x)) = []
unsAdd2 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd2 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd2 l1x l2x
:}

unsAdd2 [1,1] [-1,-1,-1]

[1,-1,1,-1,-1]

Here’s a variant where the test for 1 and -1 is somewhat shorter building on this idea

all (`elem` [1,-1]) [1,1,1,-1,1,-1,-1]

True

:{
unsAdd3 l1x l2x | not (all (`elem` [1,-1]) l1x) && not (all (`elem` [1,-1]) l2x) = []
unsAdd3 l1x l2x | null l1x = l2x
                | null l2x = l1x
unsAdd3 (l1:l1x) (l2:l2x) = l1 : l2 : unsAdd3 l1x l2x
:}

unsAdd3 [1,1] [-1,-1,-1]

[1,-1,1,-1,-1]

One simple idea would be to use a fold, e.g.

foldr (\x acc -> x + acc) 0 [1,-1,1,1,1,-1,1]

3

foldr (\x acc -> x + acc) 0 [1,-1,1,-1,-1,-1,1]

-1

:{
unsAdd4 l1x l2x = let ux = l1x ++ l2x
                  in collps ux
                     where collps = foldr (\x acc -> x + acc) 0
:}

unsAdd4 [1,1,1,-1] [1,-1]

2

:{
unsAdd5 ux = let pux = filter (==1) ux
                 mux = filter (==(-1)) ux
             in pux ++ mux
:}

unsAdd5 [1,-1,1,1,-1,-1,1,-1,1,1,1,1]

[1,1,1,1,1,1,1,1,-1,-1,-1,-1]

The UNS is considered a bijective base-1 numeral system. How is bijective meant here? The answer is to imagine the set of all whole numerals \(1,2,\ldots,\infin\;\), and then the set of all UNS 1-strings, e.g., 1, 11, 111. These two sets are mapped bijectively, as with bijective functions. The term unary can be interpreted mainly as a number system having only one digit. However, when we explore Peano numbers, we will revisit the idea of unary functions and unary operators.

The built-in Haskell gcd was used to reduce the rational number, e.g., fraction, to its lowest terms.

𝖟𝕭. Find the lowest terms of \(42/56\)

gcd 42 56

14

i.e., \(14\) is the greatest common divisor of both \(42\) and \(56\)

\[ \frac{42}{56} \]

Euclid’s algorithm, is an efficient method for computing the greatest common divisor (GCD) of two integers (numbers), the largest number that divides them both without a remainder.

:{
eGCD :: Integral i => i -> i -> i
eGCD 0 b = b
eGCD a b = eGCD (b `mod` a) a
:}

eGCD 60 25

5

This code give the first four perfect numbers In number theory, a perfect number is a positive integer that is equal to the sum of its positive divisors, excluding the number itself. For instance, \(6\) has divisors \(1\), \(2\) and \(3\) (excluding itself), and \(1 + 2 + 3 = 6\;\), so \(6\) is a perfect number.

:{
main = do
  let n = 4
  mapM_ print $
    take n [candidate | candidate <- [2 .. 2 ^ 19], getSum candidate == 1 ]
    where
      getSum candidate =
        1 % candidate + sum [1 % factor + 1 % (candidate `div` factor)
                            | factor <- [2 .. floor (sqrt (fromIntegral candidate))]
                            , candidate `mod` factor == 0 ]
:}

main

6
28
496
8128