This is a comment that I would like to share about your blog post titled Keep your types small...
Expanding the domain seems silly to do – we accept more possible values than we know what to do with. This is clearly not going to make it easier or simpler to implement our programs.
I agree that expanding the domain seems silly at first. However, you are making an assumption when you say "we accept more possible values than we know what to do with", and in contrast to your last statement, it can definitely be both easier and simpler to implement a function with a larger domain.
In mathematics, there is a proof technique related to induction that I remember by the phrase
it can be easier to prove a stronger result.
Udi Manber has a pedagogical paper called USING INDUCTION TO DESIGN ALGORITHMS that very clearly explains this idea using two examples. See the section on page 8 titled "STRENGTHENING THE INDUCTION HYPOTHESIS".
Here is how I like to explain the intuition for why it can be easier to prove a stronger result by induction. The base case of the inductive proof is designed to be trivial, so there is no difficulty here. In the inductive step of the inductive proof, we need to deduce a certain claim using a slightly weaker version of the same claim (formally called the inductive hypothesis). Now consider a trying to prove by induction a slightly stronger result. Again, the base case is designed to be trivial, but the inductive step is more interesting. Compared to the inductive step in the previous inductive proof, both the claim to be deduced and the inductive hypothesis are stronger. Said another way, we are trying to prove more but we are given more to start with. Most of the time, this will make the proof harder, but sometimes things get easier.
The concept in programming that corresponds to proof by induction is a recursive function. When you enlarge the domain of a recursive function, you have certainly made your job harder in the sense that you are making a larger promise to your callers. On the other hand, you have also made your job simpler because you are now able to make use of this larger promise yourself when implementing your function.
The two examples in Udi's paper (as the paper's title suggests) are algorithmic, so you can look there to see how he expands the domain in order to implement the functions. I think a simpler example is possible though if one isn't also concerned with proofs by induction like he is.
As a toy example, consider the function f(n) defined recursively as n * f(-n+1) for |n| > 0 and f(0) = 1. Now suppose that for some application, you will only ever call this function with non-negative integer inputs. An implementation for that particular domain would not be the most obvious one given this definition. Instead, it would be easier to expand the domain to all integers. Then the implementation can exactly mirror this definition. (I hope this toy example helps even though, for non-negative integers, it is the case that f(n) = (-1)^floor(n/2) * n!).
This is a comment that I would like to share about your blog post titled Keep your types small...
I agree that expanding the domain seems silly at first. However, you are making an assumption when you say "we accept more possible values than we know what to do with", and in contrast to your last statement, it can definitely be both easier and simpler to implement a function with a larger domain.
In mathematics, there is a proof technique related to induction that I remember by the phrase
Udi Manber has a pedagogical paper called USING INDUCTION TO DESIGN ALGORITHMS that very clearly explains this idea using two examples. See the section on page 8 titled "STRENGTHENING THE INDUCTION HYPOTHESIS".
Here is how I like to explain the intuition for why it can be easier to prove a stronger result by induction. The base case of the inductive proof is designed to be trivial, so there is no difficulty here. In the inductive step of the inductive proof, we need to deduce a certain claim using a slightly weaker version of the same claim (formally called the inductive hypothesis). Now consider a trying to prove by induction a slightly stronger result. Again, the base case is designed to be trivial, but the inductive step is more interesting. Compared to the inductive step in the previous inductive proof, both the claim to be deduced and the inductive hypothesis are stronger. Said another way, we are trying to prove more but we are given more to start with. Most of the time, this will make the proof harder, but sometimes things get easier.
The concept in programming that corresponds to proof by induction is a recursive function. When you enlarge the domain of a recursive function, you have certainly made your job harder in the sense that you are making a larger promise to your callers. On the other hand, you have also made your job simpler because you are now able to make use of this larger promise yourself when implementing your function.
The two examples in Udi's paper (as the paper's title suggests) are algorithmic, so you can look there to see how he expands the domain in order to implement the functions. I think a simpler example is possible though if one isn't also concerned with proofs by induction like he is.
As a toy example, consider the function
f(n)defined recursively asn * f(-n+1)for|n| > 0andf(0) = 1. Now suppose that for some application, you will only ever call this function with non-negative integer inputs. An implementation for that particular domain would not be the most obvious one given this definition. Instead, it would be easier to expand the domain to all integers. Then the implementation can exactly mirror this definition. (I hope this toy example helps even though, for non-negative integers, it is the case thatf(n) = (-1)^floor(n/2) * n!).As a final thought, Udi later expanded that paper into a book called Introduction to Algorithms: A Creative Approach, so it definitely contains some good stuff.
Oh, and I just found your blog a few days ago and really enjoy all the posts that I have read. Keep up the good work! :)