Exactly a year ago, in one of my previous posts, we proved Monoid laws with Idris. We’ll do the same with Groups.
Category: Mathematics
Tuply singleton v3 (with proof)
In my previous post, I had a different approach to Tuply singleton.
This is the third and last post in the Tuply singleton series. We will provide mathematical proof for correctness, and also show a generalized formula.
Tuply singleton v2
In my previous post I showed how we can encode a pair into a single number.
I found out that encoding is wrong for some numbers. For example, consider the pairs 
In this post, we will change our strategy and slightly adjust our formula.
Tuply singleton
I noticed this while at a company team meetup. Whenever we were discussing which place we should eat food at, most of my coworkers were paying attention to two numbers: rating and number of votes.
For example, Restaurant #1 can have a 5.0-star rating with 1 vote, and Restaurant #2 can have a 3.9-star rating with 17 votes.
This metric makes a tuple, where the first element is the rating and the second element is the vote count. It is represented by, e.g. (3.9, 17) in Haskell (and is of type (Double, Int)), or [3.9, 17] (or { fst: 3.9, snd: 17 }) in JavaScript.
So we need two elements (or numbers) to capture this metric. What is a good way to combine them in a single element, such that both can be extracted at any time?
One plus one equals two
Suppose one of your programmer friends comes to you and says: “Hey, convince me that 1 + 1 = 2!”.
What a request. You start by “Okay, I have one apple in my hand. I grab another one. Now I have two apples”.
Your friend proceeds: “I am still not convinced”. Now you turn to formalities.
