Money in the type system where it belongs
Money is a measurable abstraction over wealth. Like the number 7, money has little to no intrinsic value. It is civilization who agrees on a currency's utility and on whether the wealth conveyed by 7 units of a particular monetary currency are enough or not. That is, the value of money is extrinsic. Interestingly, the value of most currencies is measured in terms of the value of other currencies, most of which have no value other than the trust recursively vested in them by civilization. Money, in other words, mostly measures trust. This is less obvious for precious metals or cryptocurrencies because they have an intrinsic value of their own as well, whether civilization embraces them as currency or not. But still, that alone is not enough, civilization will drive their value up or down depending on how much they trust them.
Notwithstanding the value civilization gives to a particular currency, the amount of said currency one owns can't spontaneously increase nor decrease in number. As programmers, we do play a crucial role in ensuring amounts of currency are never made up nor lost. In this article we will explore how we can leverage types, functional programming, and in particular the safe-money Haskell library to ensure that our software deals with monetary values and world currencies as carefully as civilization requires. Mostly, we will be exploring the type system and learning how to reason through types.
Representing exact monetary values in computers is a subtle matter, and even more so is operating with them. Let's investigate some of the alternatives.
Most world currencies allow using fractional numbers to represent some amount of a currency unit. For example, 32.15 USD or 3.64 EUR are valid amounts. In programming languages, the tool we have most readily available for representing fractional numbers are floating point numbers. Unfortunately, they are the wrong tool. Consider the following example where we try to add 0.10 USD and 0.60 USD together. Naturally, we expect 0.70 USD as a result, but instead we get something else:
> 0.10 + 0.60 :: Float
0.70000005There are some problems with this result. It is not exact, sure, but more importantly: We are making up money! We can't do that. Where are those extra 0.00000005 coming from? Floating points are intended to be an approximation of numeric values belonging to an infinite set in a finite and predictable amount of computer memory. But, of course, not every numeric value in such infinite set will be exactly representable within the same finite amount of memory, so some sacrifices will be necessary at times, and rounding errors will happen. Our ideal 0.7 was one such sacrifice, a value not exactly representable as a floating point number. We got an approximation instead.
Floating point numbers are acceptable for many applications, but not for money. Otherwise, who pays for these rounding errors? Remember, money can't be made up, money can't vanish. A better representation for money is integer numbers. For example, instead of talking about 0.60 units of USD, we could talk about 60 units of “a hundredth of an USD”. That is, we would talk about whole amounts of USD cents instead of fractional amounts of USD dollars. We simply change our unit to be smaller than the dollar. Computers are excellent at working with integer numbers, so, in our previous example 10 plus 60 would have been precisely 70. And indeed, integers are a good representation for monetary values for fiat and crypto currencies to a good extent.
However, integers are still not enough for all our needs. We can identify at least two problems with this approach. The first problem is representing currencies that don't have a “canonical smallest unit” like USD had in the cent. Think of precious metals, for example. What is the smallest unit of gold? Is it a kilo? Is it a gram? Is it a tenth of a gram? Is it a troy ounce? There's no correct answer. For all practical intents and purposes, you can repeatedly split your gold into smaller pieces and still call each of the smaller pieces “gold”. So, since we can't find a canonical smallest unit for this currency, we can't count our gold as a whole amount of them. Otherwise, we'd be unable to count pieces smaller than any arbitrarily chosen smallest unit. And yes, presumably we could treat the atomic mass of the gold atom as our smallest unit, but that would be rather small and unpractical.
A more subtle problem with integer numbers is representing intermediate values. Say, what is the half of 5 USD cents? It is 2.5 cents, but of course can't be represented as a whole amount of cents. An “alternative” result, 2, is an approximation in which we lose 1 cent. 3 is another approximation in which we make up 1 cent. But we already know that losing or making up money is not acceptable. Yet, values such as “half 5 cents” are important even though it's impossible to represent them using coins or other tangible currency support. In particular, these values are very important when they are the intermediate results of some calculation. Suppose you want to write a function that calculates “ten times half of its input”. That is, f x = 10 * (x / 2). If our input is 5 cents, ideally, we would get 25 cents as a result, which is a perfectly representable whole amount of cents. However, if the intermediate result for x / 2 would have been rounded down or up, we would have gotten either 20 or 30 cents as result, respectively. Generally, this is unacceptable when dealing with money, so integer numbers are not sufficient representation for monetary values for manipulation purposes. What is the answer then?
The correct way of representing monetary values for manipulation is as rational numbers. Rational numbers always give precise results, they don't introduce rounding errors and they don't require us to acknowledge a “smallest representable unit”. For example, going back to our original example: Adding 0.10 USD cents plus 0.60 USD cents is, conceptually, the same as adding one tenth of a dollar plus six tenths of it:
> (1 % 10) + (6 % 10) :: Rational
7 % 10Note: In Haskell, we use the syntax numerator % denominator to construct a rational number.
As expected, we got a precise value. Moreover, since these are just rational numbers, if we wanted to represent 0.60 cents as the equivalent three fifths of a dollar, that would have been acceptable as well.
> (1 % 10) + (3 % 5) :: Rational
7 % 10This gives us a lot of flexibility when working with those intermediate values mentioned before. In particular, we can use values such as 25 % 1000, 1 % 40 or (1 % 2) * (5 % 100) to represent our idea of “the half of 5 cents”.
Eventually, when performing a real-world transaction for this rational amount, we will of course need to somehow approximate it to a whole number that is actually representable in our smallest currency unit of choice. This is fine, however, because by then we have already performed all the calculations we needed in a lossless manner, so our approximation will be as close to the ideal value as possible, and at that point we can make a concious decision of whether to round up or down our value if necessary. Additionally, we will see later how we can improve this by requiring that any remainder which doesn't fit in the approximated value be acknowledged. That way, money is never lost.
Something to also keep in mind is that rational numbers are not free. In principle, they could potentially occupy large amounts of memory because internally they are represented as two unbounded integer values. In practice, those integers will usually be small enough that from a memory usage point of view the difference won't be that significant. Performance will likely be worse than when working with floating point numbers or bounded integers. You'll have to benchmark and decide for yourself whether that's more important than precision.
To sum up, we now know what the correct representations for monetary values are. Integer numbers indicating an amount of some chosen “smallest currency unit” suffice when we want to represent amounts that can be evenly divided by said currency unit. On the other hand, if we perform any arithmetic operations on this amount, then rational numbers are a better representation because they will prevent any loss of money in case one of these operations results in an amount not evenly divisible by said smallest currency unit. You might recognize these two representations by other names: The integer representation gives us a discrete view of monetary values in a particular currency unit, whereas the rational representation gives us a dense view of currency amounts, whatever our smallest unit of choice may be. In safe-money, we have two datatypes for representing monetary values, they are called Discrete and Dense.
Let's look at the Dense type first:
newtype Dense (currency :: Symbol)Even if we don't know what Symbol is, we should still be able to grasp the idea that a Dense monetary value is somehow related to a particular currency, because the word currency shows up as a type parameter. If you haven't seen Symbol in Haskell before, don't worry too much about it: Symbol is like String, but it exists at the type level and not at the term level. For us, this currency type parameter will be things such as "USD", "BTC" or "XAU", and the reason why conveying the name of the currency as a type parameter is so important is because it prevents us from accidentally mixing amounts of different currencies. Later on we will learn more about the Symbols that can be used here.
Let's try and represent 2 USD, for example. Following the recommendation from the safe-money Haddock documentation, we see that fromInteger should do the trick. However, notice that we explicitly need to specify the "USD" type, as otherwise the compiler can't infer it because fromInteger can be used to create Dense values for any currency, not just USD.
> fromInteger 2 :: Dense "USD"
Dense USD 2%1 -- USD 2.00Notice that in Haskell you don't have to say fromInteger explicitly when you use a literal number. That is, saying 2 is the same as saying fromInteger 2. So, the previous example could have been written as follows.
> 2 :: Dense "USD"
Dense "USD" 2%1 -- USD 2.00If we want to represent an amount not evenly divisible by the main USD unit (the dollar) such as 3.41 dollars, then fromInteger is not enough. We need to use the fromRational smart constructor instead, as recommended by the Haddock documentation.
> 'fromRational' (341 % 100) :: Dense "USD"
Dense "USD" 341%100 -- USD 3.41Note: In some cases, when trying to build a Dense value out of a Rational number obtained from untrusted sources, dense would be a better alternative than fromRational. Refer to the Haddocks to understand why, but not now.
And as promised, we can safely operate with Dense monetary values without any loss of precision, even when working with values not evenly divisible by the currency's smallest unit. Dense supports the usual plethora of numeric-like typeclasses: Eq, Ord, Num, Fractional, Real.
> let x = 4 :: Dense "USD" -- USD 4.00
> x + 60
Dense "USD" 64%1 -- USD 64.00
> x / 3
Dense "USD" 4%3 -- USD 1.3333333...
> (x / 3) * 3 == x
True -- No loss of intermediate amounts!That's it, really. There's not much more to Dense values in terms of operating with them. You can do anything you can do with a Rational number.
Let's go back to currencies for a bit. Here is an example of using the currency type parameter to Dense in order to prevent accidentally mixing different currencies:
> (1 :: Dense "BTC") + (2 :: Dense "JPY")
<interactive>:6:35: error:
• Couldn't match type ‘"JPY"’ with ‘"BTC"’
Expected type: Dense "BTC"
Actual type: Dense "JPY"
...Great, that is exactly what we wanted. However, sometimes, instead of triggering a compiler error, we may want to exchange these different Dense values into a common currency so that they can be used together. For this, we have the aptly named exchange function.
exchange :: ExchangeRate src dst -> Dense src -> Dense dstTo seasoned Haskell developers, the behaviour of this function will be obvious from its type and the names given to the type parameters. This function is an excellent example of why Haskell, and type systems in general, are such powerful tools, so let's explore it a bit. Let's start with the asumption that we want to convert "JPY" into "BTC". Here's a transcript of what might be thought process of a seasoned Haskell developer:
The function is called exchange, and seeing how this safe-money library is about money, then quite likely “exchange” here means “exchange one currency for another”. I might be wrong, but sounds like a safe bet.
Yes! This must be the correct function, because I see something called ExchangeRate in the type signature, and I know exchange rates convey the idea of how much one currency is worth in another currency, something quite likely necessary when exchanging one currency into another.
Ah, it also takes a Dense monetary value as argument, given another Dense as result. But... these Dense values are indexed by different src and dst currencies, so clearly a monetary value in currency src is being converted to another monetary value in currency dst.
It looks like src is probably a short for “source” and dst is probably a short for “destination”. So, we convert from some source currency to some destination currency. In our case, src shall be "JPY" and dst will be "BTC".
Hmm... The ExchangeRate parameter is also indexed by both src and dst, which presumably means that the exchange rate only works for a particular combination of currencies. It makes sense. I wouldn't want to use the exchange rate for a different currency with my monetary amount.
What is a ExchangeRate anyway? Well, the function is pure, so it's certainly not the current market value or something like that. I'm glad this function is pure, by the way, it means I should be able to do something like x + exchange foo y and it will work just fine. This will be easy!
Now... how do I build an ExchangeRate "USD" "JPY"? ...
Luckily, this Haskell programmer knew a thing or two about currencies, so there was some prior knowledge about the problem domain that influenced the reasoning progress. However, what if we didn't have that advantage? What if we are trying to solve a problem in a domain we know nothing about? Let's explore this approach a bit as well, because this is a place where Haskell truly shines.
If we recall, we were trying to add two Dense values together. However, these Dense values were indexed by different type parameters, which prevented the addition from compiling. That's the problem we ultimately need to solve, and this is how another seasoned Haskell programmer that knows nothing about currencies might approach it:
I have a Dense "JPY" but I need a Dense "BTC". Is there any function Dense a -> Dense b or similar exported by safe-money?
It seems the only function that has a similar type is exchange :: ExchangeRate src dst -> Dense src -> Dense dst, so this function looks like a good candidate.
I have src ~ "JPY" and dst ~ "BTC", so, how do I obtain an ExchangeRate "JPY" "BTC", whatever that might be?
The subtle difference between this approach and the one above is that here we just don't care about domain specific concepts such as currencies or exchange rates, yet we are able to successfully make effective use of them because they have been encoded in the type system. In fact, let's take this reasoning approach one step further by repeating the steps above obfuscating the names of the things we are dealing with:
I have a Foo a but I need a Foo b. Is there any function Foo a -> Foo b or similar exported by this library?
It seems the only function that has a similar type is qux :: Bar a b -> Foo a -> Foo b, so this function looks like a good candidate.
How do I obtain an Bar a b, whatever that might be?
There's so much being said in just a type. Everything in the type of exchange is of essence. Everything is safe and clear. Programming is suddenly not about reading documentation anymore, nor about navigating executable code, but about learning how to quickly recognize the shapes of the pieces of a puzzle, knowing that as long as two pieces fit together, it will be alright. Haskell is beautiful, it makes programming fun.
We took a small detour, but hopefully we learned or were reminded of a nice thing or two about Haskell. Now it's time to go back to our safe-money library. In particular, as witnessed by our thought transcripts before, we need to learn about ExchangeRate. Luckily, however, there's not much to learn about it. An ExchangeRate src dst, as explained by its documentation, is just a rational number by which we multiply monetary values in a currency src in order to obtain an equivalent monetary value in a different currency src. We construct an ExchangeRate using exchangeRate, which takes the mentioned rational number as an argument.
> let Just jpybtc = exchangeRate (3 % 1000000) :: Maybe (ExchangeRate "JPY" "BTC")
> (1 :: Dense "BTC") + exchange jpybtc (2 :: Dense "JPY")
Dense "BTC" 500003%500000Finally, as expected, if we wanted to use this exchange rate for currencies other than JPY and BTC, the type checker would complain.
> (1 :: Dense "BTC") + exchange jpybtc (2 :: Dense "EUR")
<interactive>:17:39: error:
• Couldn't match type ‘"EUR"’ with ‘"JPY"’
Expected type: Dense "JPY"
Actual type: Dense "EUR"
...We now know how to operate with different currencies in safe-money.
Interestingly, and just as a side note, ExchangeRates can be composed as well. What does this mean? Picture yourself in Japan with gold in your pockets, a plane ticket to Spain, and nobody willing to trade your gold directly for the Euros you'll need in Spain. Do you cancel your trip? No, you sell your gold for Japanese Yen to the local goldsmith, and then exchange those Yen for Euros at one of the fiat currency exchange shops at the airport. Sure, you'll likely lose some money in the process due to the many hoops and the terrible exchange rates, but you will finally get those much needed Euros to buy some tapas and vinos in Spain. What you did in Japan was composing the exchange rate from gold to Yen, with the exchange rate from Yen to Euro. And as ugly as the rate you got might have been, what you did was beautiful. In safe-money, ExchangeRate forms a category where composition using (.) allows you to convert from one currency to another by means of some intermediate currency. In our case, we went from gold (XAU) to Euros (EUR) by means of Japanese Yen (JPY).
> :t goldsmith
goldsmith :: ExchangeRate "XAU" "JPY"
> :t fiatshop
fiatshop :: ExchangeRate "JPY" "EUR"
> let you = fiatshop . goldsmith
> :t you
you :: ExchangeRate "XAU" "EUR"As mentioned before, we can observe monetary values either through an idealized representation as a members of a dense set, or through a more realistic representation as multiples of some small unit agreed to be aceptable by the parties involved in the monetary transaction.
Let's take the Euro (EUR), for example. This currency has a widely accepted small unit called the Cent, where 100 Cents equal one Euro. So, if we were to represent amounts of this currency intended to be acceptable for transactions, we could represent them as values in a discrete set of multiples of one Cent. That is, we would convey the idea of “6 Euros” using the representation “600 Cents”. In practice, finding ths “small unit” can be tricky. For example, in The Netherlands, even though coins for 1 and 2 Cents are valid and accepted, they are not minted anymore, so for most cash transactions the amount is rounded up or down to the nearest 5 cents multiple, effectively excluding amounts that are not evenly divisible by 5 cents from the discrete set. Let's keep it simple today though. Let's asume 1 cent is an acceptable small unit for EUR.
As we saw before, we use Dense currency to represent monetary amounts of a given currency as rational numbers belonging to a dense set. Perhaps unsurprisingly, we use Discrete currency unit to represent amounts of a given currency in the discrete set of multiples of a chosen “smallest unit”. That is, Discrete is just an integer number. The unit parameter conveys our idea of a “smallest unit”, and like currency, it is also a Symbol. So, for example, if we want our discrete set to be a representation of monetary values that are multiples of one EUR Cent (that is, a discrete set of monetary amounts that can be effectively rendered as some combination of EUR bank notes and coins), then Discrete "EUR" "cent" would be our type. This type is an instance of Num, so we can rely on Haskell's polymorphic literal integers to construct them, and also perform some arithmetic operations on them.
> 1 :: Discrete "EUR" "cent"
Discrete "EUR" 100%1 1 -- 0.01 EUR
> 200 :: Discrete "EUR" "cent"
Discrete "EUR" 100%1 200 -- 2.00 EUR
> 5394 :: Discrete "EUR" "cent"
Discrete "EUR" 100%1 5394 -- 53.94 EUR
> 100 + 70 :: Discrete "EUR" "cent"
Discrete "EUR" 100%1 170 -- 1.70 EURIf we wanted to use a different “small unit”, we could. For example, you can disregard Cents altogether, and instead make the Euro itself the smallest representable unit.
> 2 :: Discrete "EUR" "euro"
Discrete "EUR" 1%1 2 -- 2.00 EURThis time, however, with Discrete "EUR" "euro" we can't represen't values such as 2.74 EUR, because insofar as this discrete representation is concerned, there are no values between 2.00 EUR and 3.00 EUR, as witnessed by succ from the Enum class, which gives us the successive value to 2.00 EUR.
> succ (2 :: Discrete "EUR" "euro")
Discrete "EUR" 1%1 3 -- 3.00 EURAnd, of course, we can't accidentally mix Euros and Cents:
> (2 :: Discrete "EUR" "euro") + (5 :: Discrete "EUR" "cent")
<interactive>:32:34: error:
• Couldn't match type ‘100’ with ‘1’
Expected type: Discrete "EUR" "euro"
Actual type: Discrete "EUR" "cent"
...In order to add Euros and Cents together, much like we did for exchange rates, we need to convert one or both of these values to a common “small unit” that can represent them. In our case it is easy, because we know that we can represent 2 Euros as 200 cents, and we already have Cents as the second operand's small unit, so we just need to find a function to make that conversion.
eurosToCents :: Discrete "EUR" "euro" -> Discrete "EUR" "cent"Perhaps surprisingly, a quick glance at the safe-money documentation doesn't mention a function resembling this reasonable lossless function. The reason for this becomes more apparent if you reverse the arrow.
centsToEuros :: Discrete "EUR" "cent" -> Discrete "EUR" "euro"You see, centsToEuros is a lossy function. That is, if you were to convert an integer number of cents to an integer number of euros, you would inevitably lose some precision because 0.72 EUR can't be represented as a whole number of Euros. This is the kind bug that a good type-system, like Haskell's, can outright eradicate.
While it is possible to whitelist source and target “small unit” pairs that are can be converted in a lossless manner, for example by checking for common factors, safe-money prefers to take a general approach that works fine whatever small units you might be dealing with.
It's time to grow up and learn the truth. So far we've been talking about “small units” when referring to things like the Euro or the Cent. However, as the attentive reader might have figured out by now, safe-money doesn't really care about names like Euro or Cent, all it cares about is the ratio between this “small unit” and the value of the currency unit. In safe-money we call this ratio “scale”, and it is simply a number that tells the number of “small units” necessary to add up exactly to the currency's main unit. For example, the Cent has a scale of 100 in the EUR currency, because 100 Cents add up to one EUR. The Euro, on the other hand, has a scale of 1, because the Euro itself is EUR's main currency already.
It is not always this straightforward, though. Something interesting about Discrete is its support for currencies where the number of “small units” in the larger unit is not a multiple of 10. For example, consider a precious metal such as gold. According to the ISO-4217 standard for currency codes that we have been following, the currency symbol for gold is XAU, and one unit of XAU amounts to one troy-ounce of gold.
> 1 :: Discrete "XAU" "troy-ounce"
Discrete "XAU" 1%1 1But what if we want to represent a smaller amount as a Discrete value? We need to find a smaller “small unit”. The troy-ounce, as most non-metric units of measurement, is terribly confusing and doesn't use a base-10 system for establishing relationships between bigger or smaller related units of mass. It's common to see gold measured in other units such as the gram. However, the relationship between the gram and the troy ounce is not a pretty number: There are 31.103477 grams in a troy-ounce. This means that a Discrete "XAU" "gram" value would be conveying an integer number that, when divided by 31.103477, will amount to a possibly fractional number of troy ounces of gold.
We have learned, however, that representing non-integer numbers involved in monetary amounts is tricky, and that we need to rely on rational numbers instead of floating point approximations. For this reason, scales in safe-money are rational numbers as well. So when we said before that the scale of Cents in EUR is 100, we actually meant 100 % 1, and when we say now 31.103477, we actually mean 31103477 % 1000000. If you have been paying attention to the REPL output in our examples, you probably noticed this fraction showing up everywhere.
> 2 :: Discrete "EUR" "euro"
Discrete "EUR" 1%1 2 -- The scale is: 1 % 1
> 130 :: Discrete "EUR" "cent"
Discrete "EUR" 100%1 130 -- The scale is: 100 % 1
> 4 :: Discrete "XAU" "gram"
Discrete "XAU" 31103477%1000000 4 -- The scale is: 31103477 % 1000000Where does the scale come from, though? If you look closer at Discrete, you'll see that it is actually a type synonym for another type called Discrete'.
data Discrete' (currency :: Symbol) (scale :: (Nat, Nat))The currency type parameter is exactly the same as in Discrete, it allows us to tell currencies apart from each other. And the scale type parameter is, of course, the scale, which as we just mentioned is a rational number which we choose to represent at the type level as a tuple consisting of its numerator and its denominator. Nat, in case you are not familiar with it, is to Natural what Symbol is to String. That is, Nat is a type-level representation of natural numbers. Having the scale at the type level prevents monetary values with different scales to be accidentally used together, as we have seen before.
The Discrete type synonym is defined as follows:
type Discrete (currency :: Symbol) (unit :: Symbol)
= Discrete' currency (Scale currency unit)Most of the times we use Discrete instead of Discrete' because it's easier and less error-prone to remember words like “cent” or “gram” than dealing with rational numbers explicitly. But at the end of the day, these two approaches are fully interchangeable, and it's up to the user of safe-money to decide what approach works best for them. Discrete relies on a helper type family called Scale to convert these memorable names to rational numbers.
A type family is basically a function. However, instead of taking terms as arguments and returning terms as a results, it takes types as arguments and returns types as results. The Scale type family works pretty much like this term-level function:
f1 :: String -> String -> Rational
f1 "EUR" "euro" = 1 % 1
f1 "EUR" "cent" = 100 % 1
f1 "XAU" "troy-ounce" = 1 % 1
f1 "XAU" "gram" = 31103477 % 1000000
f1 ...However, not quite. The problem with f1 above is that the scales for all currencies and units must be defined in the same function, and that's not something we want, since it would mean that the only supported currencies and units are the ones explicitly handled by safe-money in this function. Instead, we want to allow users of this library to add their own currencies and units. We achieve that by making Scale an open type family, meaning we are not forced to make a closed-world assumption of the currencies and units we'll be able to handle. Instead, users will be able to add more as needed, possibly across different modules and packages. In this sense, open type families are more closely related to type-class methods than to normal functions. Scale is defined like this:
type family Scale (currency :: Symbol) (unit :: Symbol) :: (Nat, Nat)That is, Scale is a type-level function that takes a currency identifier as first argument and a unit identifier as second argument, and returns the unit's scale for that currency as a rational number which we've chosen to represent as a tuple of nominator and denominator. Instances of this type family, akin to methods in instances of a type-class, are defined like so:
type instance Scale "EUR" "euro" = '(1, 1)
type instance Scale "EUR" "cent" = '(100, 1)
type instance Scale "XAU" "troy-ounce" = '(1, 1)
type instance Scale "XAU" "gram" = '(31103477, 1000000)
...The ' preceding the tuple is there to convince GHC that the kind of this tuple is (Nat, Nat). Otherwise, things like (100, 1) look just like a two element tuple of kind *. But... don't pay much attention to this tick. If you ever get it wrong the compiler will let you know.
So, with this new knowledge, we can easily see that something like Discrete "EUR" "cent" reduces to Discrete "EUR" '(100, 1). The unit name is not important when typechecking a Discrete value, only its scale is. Again, unit is there only as a convenience, since something like “gram” is easier to remember, recognize and get right than (31103477, 1000000). The choice of word “gram” is an arbitrary convention. We could have used “g” or “Gram” or “whatever” instead.
Once we understand scales, understanding how the conversion from a Discrete value to a Dense value happens should be easy. The discrete amount is simply divided by the discrete scale. In safe-money, there is a function for making this conversion readily available:
fromDiscrete :: GoodScale scale => Discrete' currency scale -> Dense currencyLet's try it in the REPL:
> fromDiscrete (1 :: Discrete "EUR" "cent")
Dense "EUR" 1%100
> fromDiscrete (1 :: Discrete "EUR" "euro")
Dense "EUR" 1%1
> fromDiscrete (1 :: Discrete "XAU" "gram")
Dense "XAU" 1000000%31103477
> fromDiscrete (34 :: Discrete "XAU" "gram")
Dense "XAU" 34000000%31103477The GoodScale constraint in fromDiscrete is there to ensure that we don't accidentally use a non-positive number as either the numerator or numerator of our scale. This is very interesting. We are using the type system again to prevent a negative scale and a denominator value of 0. A negative scale could replace losses with gains and vice-versa, and a denominator value of 0 would result in a runtime error. Here, we are prevent both situations from ever occurring, at compile time.
type GoodScale (scale :: (Nat, Nat))
= ( CmpNat 0 (Fst scale) ~ 'LT
, CmpNat 0 (Snd scale) ~ 'LT,
, KnownNat (Fst scale)
, KnownNat (Snd scale)
) :: ConstraintIn our case, GoodScale is implemented as a type family resulting in a Constraint that simply checks whether the number 0 is smaller than first (Fst) and second (Snd) elements of the given tuple. To accomplish this, it checks whether the result of comparing 0 to each element is 'LT. CmpNat, whose kind is Nat -> Nat -> Ordering, is basically the type-level version of compare :: Integer -> Integer -> Ordering. That is, CmpNat x y ~ 'LT is the type level version of compare x y == LT.
We also have KnownNat constraints in GoodScale. These witness that there exists a term-level representation as Integer of the elements in the tuple. This witness will be required when converting our type-level representation of rational numbers to a term-level Rational. And indeed, if we look inside the implementation of fromDiscrete, we will see that it calls a helper function called scale which uses KnownNat to build said Rational number.
scale :: GoodScale scale => proxy scale -> RationalThe proxy there can be anything of kind (Nat, Nat) -> Type, such as Proxy from Data.Proxy, or Discrete currency, as in the implementation of fromDiscrete. Let's try in the REPL.
> scale (Proxy :: Proxy (Scale "EUR" "cent"))
100 % 1
> scale (Proxy :: Proxy (Scale "XAU" "gram"))
31103477 % 1000000
> scale (1 :: Discrete "XAU" "gram")
31103477 % 1000000
> scale (999 :: Discrete "XAU" "gram")
31103477 % 1000000
> scale (999 :: Discrete' "XAU" '(31103477, 1000000))
31103477 % 1000000
> scale (Proxy :: Proxy '(31103477, 1000000))
31103477 % 1000000We now know how to convert a Discrete monetary value to a Dense one. Going in the other direction, however, is a bit more complicated. Imagine a situation where we want to convert 4.54 EUR to a whole number of Euro units. We can't readily do so because there would be a reminder of 0.54 EUR that we would never be able to represent as a whole number of Euro units. Simply rounding up or down the amount of round up or down is unacceptable, because we would be either losing or making up money, and that's something we just can't do. What we need to do instead is to let the users decide how they would like to approximate the value to the closest unit multiple as a Discrete value, and force them to acknowledge the existence of a reminder as a Dense value. safe-money exports the four usual rounding functions round, floor, ceiling and truncate, and they all share this behaviour.
round, floor, ceiling, truncate
:: GoodScale scale
=> Dense currency
-> (Discrete' currency scale, Dense currency)Given a Dense monetary value, these functions return a tuple where the first value is the largest possible approximation of said value to a Discrete amount in a the requested scale, rounded up or down depending on the choice of round, floor, ceiling and truncate. The second element in the returned tuple is the difference between the Discrete value and the original Dense value. That is, this value is the exact remainder of the approximation, which may of course be zero in case there's no reminder, or a negative number in case the Discrete value was rounded up.
> -- Sample dense value: EUR -1.24
> let x = fromRational (-124 % 100) :: Dense "EUR"
> -- Approximating (floor) to cent: EUR -1.24, no reminder
> Money.floor x :: (Discrete "EUR" "cent", Dense "EUR")
(Discrete "EUR" (100 % 1) -124,Dense "EUR" 0%1)
> -- Approximating (floor) to euro: EUR -2.00, reminder EUR 0.76
> Money.floor x :: (Discrete "EUR" "euro", Dense "EUR")
(Discrete "EUR" (1 % 1) -2,Dense "EUR" (19 % 25))As a quick reminder: floor rounds down, ceiling rounds up, round rounds to the nearest integer, and truncate rounds towards 0 (that is, truncate behaves like floor for positive numbers and like ceiling for negative numbers).
The lesson here is that by always returning the reminder of the approximation, we prevent any accidental monetary losses or gains. It's up to the caller of these rounding functions to decide how to deal with the reminder. For example, the caller could choose to save the remainder until a later time when it can be combined with other reminders, potentially adding up to a multiple of our Discrete scale. Of course, the caller can also chose to simply ignore the remainder, in which case the operation would be lossy. However, if that happens, we can still rest at ease knowing that any losses are due to a concious choice made by the caller, and not due to a faulty design in our library.
The safe-money library provides, optionally, serialization support for its datatypes using the aeson, binary, cereal, store, serialise and xmlbf libraries. Serializing indexed types such as Dense and Discrete is very straightforward. Let's try serializing as JSON using the aeson library, for example.
> Aeson.encode (32 :: Dense "EUR")
"[\"EUR\",32,1]"
> Aeson.encode (4 :: Discrete "XAU" "gram")
"[\"XAU\",31103477,1000000,4]"Dense values are serialized as a 3-element tuple containing the essentials: The currency name, the amount numerator, and the amount denominator. Discrete values are serialized as a 4-element tuple containing the currency name, the scale numerator, the scale denominator, and the integer amount. Deserializing to the same type works as expected.
> Aeson.decode (Aeson.encode (32 :: Dense "EUR")) :: Maybe (Dense "EUR")
Just (Dense "EUR" (32 % 1))
> Aeson.decode (Aeson.encode (4 :: Discrete "XAU" "gram")) :: Maybe (Discrete "XAU" "gram")
Just (Discrete "XAU" (31103477 % 1000000) 4)And trying to deserialize to the wrong currency or unit, of course, fails.
> Aeson.decode (Aeson.encode (32 :: Dense "EUR")) :: Maybe (Dense "JPY")
Nothing
> Aeson.decode (Aeson.encode (4 :: Discrete "XAU" "gram")) :: Maybe (Discrete "XAU" "kilogram")
NothingSo far, everything seems quite straightforward. To serialize or encode is always easy: We start with a value with lot of type information and end up with a value where all or most of that type information is gone. It's easy to see this if we look closer at type of the Aeson.encode function specialized to Discrete'.
discreteToJson :: Discrete' currency scale -> ByteStringNotice that discreteFromJson doesn't exist in safe-copy. It is simply Data.Aeson.decode with a different name.
This function takes a value with a lot of type information, presumably makes use of it internally, and then discards it. Discarding things is easy. However, what if we need to go in the other direction? That is, what if we need to deserialize or decode a value that carries no type information into some type-indexed value? Let's try to imagine what such decoding function could look like.
discreteFromJson :: ByteString -> Maybe (Discrete' currency scale)
discreteFromJson = \bs ->
-- 1. Check that `bs` is a serialization of a 4-element tuple mentioned above.
-- 2. Check that the currency encoded in `bs` is the same as `currency`.
-- 3. Check that the scale encocded in `bs` is the same as `scale`.
-- 4. Return a `Discrete'` value using the integer amount encoded in `bs`.That is, the implementation of this function relies on knowning the specific types of currency and scale even before attempting to construct a Discrete' value indexed by them. This function can't work “for all currencys and scales”, because even if it manages to find the string "USD" or "EUR" in bs, there's no way it can put that string, which was obtained during runtime as a term-level value, back in the type-level as an index to Discrete'. And the same is of course true for scale. Essentially, currency and scale are also inputs to this function. Funnily enough, they show up to the right of the last -> in this function signature, which can be a bit confusing at first. Maybe seeing this type written in a different style can help.
discreteFromJson
:: Proxy currency
-> Proxy scale
-> ByteString
-> Maybe (Discrete' currency scale)This new type signature is essentially the same as the previous one. Those two new Proxy arguments are redundant, but perhaps they help us appreciate how currency and scale are essentially types provided as inputs to this function.
So, what do we do if get a ByteString supposedly representing some Discrete' value, yet we are not sure in what currency and scale that might be? If our set of acceptable currencies and scales is small enough, we can simply use the Alternative support in Maybe in order to try decoding as different types in order. Sometimes, however, we may actually want to be able to deal with any Discrete' monetary value that comes our way without explicitly observing the related currency or scale. Perhaps all we want to do is show the Discrete' value, and for that we don't really need to known what the currency and scale type indexes are, all we need to know is that there is a Show instance for them. However, as things currently stand, in order to deserialize into a Discrete, we are always forced to choose the currency and scale indexes anyway. Have we reached an impasse? Well, not exactly.
In Haskell, it's the caller who must pick the types when there's some polymorphic type involved in a call. For example, consider the type of the dense function, used to construct a Dense value.
dense :: Rational -> Maybe (Dense currency)In dense, currency is a polymorphic type that must be chosen by the caller. See what happens in the REPL if we try to use dense without specifying the currency type.
> dense (4 % 7)
<interactive>:16:1: error:
• No instance for (GHC.TypeLits.KnownSymbol currency0)
arising from a use of ‘print’
• In a stmt of an interactive GHCi command: print itThe error is saying that since currency is not known, the KnownSymbol instance necessary to render this Dense value using print could not be found for it, which is a convoluted way of saying that currency must be specified. A similar kind of error would happen if we tried to, say, deserialize some raw JSON string without specifying the target type. If we ask for a specific currency, then everything works.
> dense (4 % 7) :: Maybe (Dense "EUR")
Just (Dense "EUR" (4 % 7))In Haskell there is a way to “workaround” this behavior so that it is not the caller, but the callee, who can chose the currency, and we can embrace this in order to allow Dense values for any currency to be deserialized from a raw JSON input, without having to enumerate the possible currencies anywhere in the type system. The solution is RankNTypes, and it requires a different arrangement of our deserializing function. So, instead of having a function denseFromJson :: ByteString -> Maybe (Dense currency), we would have something like this, which is only possible when the RankNTypes extension is enabled.
withDenseJSON
:: ByteString -- ^ Raw JSON
-> (forall currency. Dense currency -> r)
-> Maybe rLet's carefuly try and understand what withDenseJSON means. This function returns a Maybe because it's possible that parsing doesn't succeed, and Maybe is a cheap way for us to communicate that. Leaving this small detail out of the way, let's proceed to taking a serious look at the second argument to this function.
Unfortunately, the forall keyword is used for many different purposes in Haskell, so at times its meaning can be confusing. This forall here is quantifying currency so that it exists only within this limitted scope delimited by the surrounding parentheses. This means that if we were to refer to currency outside these parentheses, it would be a different type. We can see an extreme example of this:
f :: a -> (forall a. a -> b) -> (a, b)
f oa g = (oa, g False)This function takes an a, some function for obtaining a b, and returns that same a along with a b. This “outer a”, however, is different from the a inside the parentheses. We can see a proof of that if we partially apply f in a way that would force the outer a to be fixed to a concrete type.
> :t f ()
f () :: (forall a. a -> b) -> ((), b)The outer a is now gone, it has been replaced with a specific type (). The inner a remains, however, since was is different from the outer a. What is happening is that the scopes over which these two as are quantified are different. Or, more precisely, the outer a is available within the scope of the second argument to f, but not the other way around. That is, the inner a can't share the same scope as the outer a. Or in more precise terms, the inner a has a higher rank than the outer a, thus the extension name RankNTypes. In our definition of f we deliberately used the same name a for two different type variables. While this works, much like term-level variable name shadowing, it can be confusing, and GHC will warn us about it. We deliberately chose to use name shadowing to make a point, but in practice you should probably use different variable names for the sake of your users.
<interactive>:89:31: warning: [-Wname-shadowing]
This binding for ‘a’ shadows the existing binding
bound at <interactive>:89:13We used False, of type Bool, somewhere in our definition of f. However, nowhere in f's type we can see Bool. What is happening? Well, this is the crux of RankNTypes. Do you remember how we said earlier that when faced with a polymorphic type, the outermost caller that first encounters that polymorphism is the one who must chose what the concrete type should be? Well, this is exactly what is happening here. The important detail, however, is that our higher-ranked a is first introduced within the implementation of the callee, so our callee becomes the caller that needs to choose a concrete type for a. And, perhaps surprisingly, it can chose any type it wants. Here we chose Bool because one of its constructors was readily available, but we could have used any other type.
With this new understanding, let's go back to withDenseJSON and assume that we have some JSON blob that represents the idea of some Dense monetary value.
> withDenseJSON myJsonBlob toRational
Just (3 % 1)Great! We could convert the Dense value to a Rational even though we don't know what currency is inside myJsonBlob. But... seeing that the second argument to withDenseJSON is just a forall currency. Dense currency -> r, and that the whole withDenseJSON expression is expected to return that r, we can just pass id so that the whole expression returns said Dense currency, right? No, we can't.
> withDenseJSON myJsonBlob id
<interactive>:1:21: error:
• Couldn't match type ‘r’ with ‘Dense currency’
because type variable ‘currency’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
Dense currency -> r
at <interactive>:1:1-22
Expected type: Dense currency -> r
Actual type: r -> r
• In the second argument of ‘withDenseJSON’, namely ‘id’
In the expression: withDenseJSON "foo" idThe type-checker quite clearly tells us that r can't be Dense currency because currency would escape its scope. And we should have been expecting this. As we discussed before, the purpose of functions using higher-rank types is to be able to introduce new types in an inner scope, smaller than the scope of the function's caller. That is, currency is not defined in the outer scope where r exists. This shouldn't be surprising, since it is the same as how lexical scoping rules work for term-level values.
Note: Techically, there is a way for currency to escape this inner scope, but it requires knowing beforehand which currency you are expecting, as well as runtime type-checking, which will ofcourse fail if we don't get the currency we are expecting. We won't be exploring this.
Let's try something else. Let's try using show on our deserialized Dense value, whatever its currency might be.
> :t withDenseJSON myJsonBlob show
<interactive>:1:21: error:
• No instance for (KnownSymbol currency)
arising from a use of ‘show’
Possible fix:
add (KnownSymbol currency) to the context of
a type expected by the context:
Dense currency -> String
• In the second argument of ‘withDenseJSON’, namely ‘show’
In the expression: withDenseJSON "foo" showThe error is actually quite clear. We are applying show in the second argument of withDenseJSON, and there is no visible KnownSymbol instance for currency there. Where is that KnownSymbol requirement coming from, though? Well, we know that we are trying to show some Dense currency value, so the type of our show function would be Dense currency -> String. However, if we go to the Haddocks and search for this Show instance, we will see that there is an additional superclass to it.
instance KnownSymbol currency => Show (Dense currency) where
...We don't really need to go to the Haddocks for this, but sometimes it is just easier. We could have learned about this superclass by explicitly typing show in the REPL:
> :t show :: Dense currency -> String
<interactive>:1:1: error:
• No instance for (KnownSymbol currency)
arising from a use of ‘show’
Possible fix:
add (KnownSymbol currency) to the context of
an expression type signature:
Dense currency -> String
• In the expression: show :: Dense currency -> StringThe error is pretty much the same one we got before, which suggests we are on the right track to solving this problem. Let's explicitly add that constraint to the type signature.
> :t show :: KnownSymbol currency => Dense currency -> String
show :: KnownSymbol currency => Dense currency -> String
:: KnownSymbol currency => Dense currency -> StringSo, the issue is that much like in our very first encounter with RankNTypes, the function we are passing as a second argument to withDenseJSON doesn't include this KnownSymbol constraint, so everything depending on it fails.
Unfortunately, when you are free to pick any type like currency in withDenseJSON, or like the higher ranked a in our previous example f, the function becomes rather useless. The problem is that the function that we pass as a second argument to f knows absolutely nothing about the higher-rank a, meaning it can't do anything with it. We want something better. In our example, we want to be able to at least show the pased in higher-rank value. That's easy enough. Mostly, we just need to add the constraint to be satisfied by a inside the parentheses that are typing the passed in function.
h :: (forall a. Show a => a -> b) -> b
h g = g False
> h show :: String
"False"
> h (length . show) :: Int
5
> h (head . show) :: Char
'F'This new h function uses RankNTypes to allow the callee to take over the usual role of the caller of picking up a. This a, contrary the higher-rank a in to our previous example f, is not just any a. Instead, it must have Show instance. Applying our g function to False works because Bool is an instance of Show. However, if we tried to apply g to something like id :: x -> x, it would fail because there is no Show instance for x -> x.
h' :: (forall a. Show a => a -> b) -> b
h' g = g id
<interactive>:14:7: error:
• No instance for (Show (x -> x)) arising from a use of ‘g’
(maybe you haven't applied a function to enough arguments?)
• In the expression: g id
In an equation for ‘h'’: h' g = g idWhat this implies is that a witness that a satisfies Show is necessary at h's definition site, not at its call site. This shift of responsibility is very powerful. Suddenly we are able to show things even if we can't produce the necessary Show witness at the call site, by relying on a higher-rank function to provide it for us. And with this new understanding, let's go back to our monetary parsing problems. We know that in order for the show function on a Dense currency to work, we need a KnownSymbol currency constraint satisfied as well. Let's change the type signature of withDenseJSON just like we did in h, so that this witness is available inside the higher rank function.
withDenseJSON
:: ByteString -- ^ Raw JSON
-> (forall currency. KnownSymbol currency => Dense currency -> r)
-> Maybe rThe KnownSymbol constraint is now satisfied, so Show should be automatically satisfied as well.
> withDenseJSON myJsonBlob show
Dense "EUR" (4 % 7)So far we've talked about JSON. But what about other serialization formats? What about parsing some XML format, or perhaps some binary format? Do we have to implement withDenseXML, withDenseBinary, etc.? Hopefully not, since not only their implementations will be quite redundant, but also we can't really leverage many of the already existing tools like FromJSON, binary's Binary, or even Read, since we are always forced to use this RankNTypes approach. So... let's try and understand a bit more what we mean when we talk about deserialization to see if we can find a common approach to all of these formats.
Supose we have these four raw representations of the value fromRational (4 % 5) :: Dense "EUR" as ByteStrings.
> s1 = "[\"EUR\",4,5]" -- ^ The JSON representation we saw before.
> s2 = "4/5 EUR" -- ^ A supposedly user-friendly representation.
> s3 = "\x03\x01EUR\x04\x05" -- ^ A binary representation.
> s4 = "EUR\xff\x04\x05" -- ^ Another binary representation.These four ByteString representations are term-level values, and in them we encode the essentials that convey the idea of fromRational (4 % 5) :: Dense "EUR". That is, they mention the name of the currency "EUR", the numerator 4 of the rational number representing the monetary amount, and its denominator 5. In other words, they are isomorphic to a (Rational, String) tuple where the first element is the monetary amount as a rational number, and the second element is the currency identifier. This is the same data conveyed by a Dense value, if we consider that its rational number representing the monetary amount at the term level is always accompanied by a currency identifier at the type level. However, therein lies our problem: The currency identifier in Dense only exists at the type level, making it impossible for us to implement a function going from that raw ByteString to some arbitrary Dense currency, as this would imply that currency is a type dependent on a some data present in said ByteString. We already encountered a similar situation in discreteFromJson and we know it doesn't work without RankNTypes. However, we are deliberately trying to avoid having a RankNTypes-based solution for each of our four ByteString representations. We need a different approach.
Let's take a step back and recall what we are trying to do: We have many possible ByteString representations for a same Dense value of an unknown currency—possibly an infinite number of them—and we want to be able to write parsers for these raw representations without having to do the RankNTypes dance every time, which we know we need to do every time we go from a “less typed” representation to a “more typed” representation. That is, every time we go from a representation where the currency identifier is not in the types, to one where it is. Can you see where this is going?
What we need to do is reduce the number of times we go from a “less typed” to a “more typed” representation to just one, so that we only need to worry about RankNTypes once. How do we accomplish this? Well, we simply acknowledge that the tuple we briefly mentioned before is a perfectly acceptable term-level representation of all the data conveyed by both the Dense datatype, and all of the raw representations we care about, and as such we can treat it as some canonical “less typed” intermediate representation between them. The idea is that all of our raw ByteString representations will be parsed into this intermediate representation, which should be very straightforward because we won't need to concern ourselves with coming up with currency information at the type level. Once we have this intermediate value, we can simply rely on a unique function to do the RankNTypes work. In safe-money, we have this intermediate type and the relevant RankNTypes function out-of-the-box. They are called SomeDense and withSomeDense. Of course, SomeDense is not just a tuple, as this makes it easier to give specific instances for it, such as FromJSON. And more generally, because is always a good idea to introduce new types for any abstraction that can be conceptually identified as unique, so that we don't accidentally mix them with different yet structurally compatible abstractions, while improving type inference and error messages at the same time.
Of course, we can only deserialize raw representations that have been correctly serialized before, so SomeDense provides instances for this such as ToJSON. Serialization, however, is different than deserialization in the sense that when we serialize we are going from a “more typed” value to a “less typed” value. Exactly the opposite than in deserialization. In our case, it means that if we were to start with a value like fromRational (4 % 5) :: Dense "EUR", then we would always have that currency identifier available at the type level as input, and there would be no reason for us to worry about things like RankNTypes. This implies that whereas it is not possible for us to provide a FromJSON instance for Dense that works for all currencies, it is perfectly possible to write a ToJSON instance that works for all of them. In turn, this suggests that our intermediate representation SomeDense is not really necessary for serialization. And indeed, it is not. However, for completeness, safe-money always provides serialization and deserialization support for both Dense and SomeDense values that are compatible among them. That is, a serialized Dense value can be correctly deserialized both as both SomeDense and Dense, although in the latter case you would need to know the currency identifier beforehand. The same is true for the serialization of SomeDense, which can also be deserialized as both SomeDense or Dense.
Similarly, much like for Dense monetary values we have SomeDense, for Discrete values we have SomeDiscrete, with the small difference that SomeDiscrete hides two type level arguments currency and scale, not just one. And we also have SomeExchangeRate which hides the two type parameters to ExchangeRate.
What is it about this currency identifier that complicates our Haskell so much? It has to do with the position where we want to use Dense in function calls, a topic often overlooked yet important in order for us to develop a stronger understanding and intuition of how things compose together. Let's take a diversion to explore this topic. Consider the following hypotetical function.
f1 :: a -> bWhat can we say about a and b without knowing the implementation of f1? Well, for one, it seems that this function can't possibly be implemented because it is simply not possible to create a b out of thin air since we don't really know what b is supposed to be, so how would we produce one? Would something change if we were to change b to be some concrete type?
f2 :: a -> IntCertainly. Now we can at least imagine f2 being implemented. Here are two possible implementations.
-- | One possible implementation
f2 :: a -> Int
f2 _ = 5-- | Another possible implementation
f2 :: a -> Int
f2 _ = 895Although perfectly valid, these are rather silly functions. What we are seeing in these functions is the position of our original b argument come into play. b is said to be a function argument in positive position, which for practical purposes is mostly a fancy way of saying that a value of type b is being produced within the function. If we are producing a value of type b, however, we as producers must now what b is in order to produce it. This is why why we end up being forced to pick some arbitrary integer number. The positive position of b, and the fact that we don't already have some value of type b at hand, force us to make a decision and pick one, which necessarily makes the type of b less polymorphic.
There are also function arguments in negative position. These are the arguments consumed by the function. That is, they are taken as input somehow. In our example, a is one such argument in negative position. We chose not to do anything with a in our example, but this is besides the point. We might as well had done something with it.
It is of course possible to have a same type ocuppy both a positive position and a negative position at the same time. The simplest example of this is the identity function, whose type a -> a says the first a is in negative position while the second a is in positive position. The fact that the way id “produces” its positive a is by just reusing the negative a that was given as input is not problematic. All that matters is that id can obtain some a to provide as output somehow, and then our positive position requirements will be satisfied.
Identifying the position of function arguments is not as straightforward as it may seem at first, however. Consider the following example.
f3 :: (a -> b) -> a -> bIn this example, we see that a is received as an input in the a -> b function, and also as the second argument to f3, which suggests that a appears in negative position twice. Also, we see that b is an output of both the a -> b function, as well as an output of the whole f3 expression, which suggests b appears in positive position twice. However, that's not entirely correct.
When we talk about argument positions in a particular function, we need to look at said function's arguments as a whole, and not individually. It's not sufficient to analyse the a -> b and a arguments individually, we must also analyse all of (a -> b) -> a -> b at the same time. From this point of view, we can see that the obvious inputs to f3 are its arguments a -> b and a. That is, these two arguments are being consumed by f3, which means these are arguments in negative position. Similarly, the obvious output of f3 is the b that shows up as its return type. This particular value of b is being produced by f3, which implies that this b is in positive position. Indeed, these are all truths. And moreover, our occurrences of a and b here as negative and positive arguments, respectively, agree with our previous assessment of the positions of a and b in a -> b individually. So, are we done? Well, no, this is not the full story. The best way to understand why is to look at the usage of a -> b in an implementation of f3—which, by the way, due to parametricity, happens to be the only possible implementation of f2.
f3 :: (a -> b) -> a -> b
f3 g x = g xIsn't it true, when looking at this code, that we are calling g within the implementation of f3? And isn't it true that in order to call a function a caller must be able to produce all of the function inputs. Yes, it is all true. So, even while it's true that when assessing a -> b individually, a is in negative position, and that when assessing the type of f3, a is in negative position. It is also true that from f3's implementation point of view, an a must somehow be produced in order to be able to call g. Hence, the a in a -> b is in positive position. This is fine, a same type can be in both positive and negative positions at the same time. Similarly, while b appears in a positive position, it also appears negative position. Why? Well, isn't it true that the implementation of f3 is able to consume the b produced by g x? Indeed. This implies that b is actually in negative position here. The fact that as soon as we obtain this b we simply reuse it as f3's final value is incidental.
Enough with the contrived abstract examples. Why do we care about all of this? Well, observe the similarities between f3 and withSomeDense.
f3 :: (a -> b) -> a -> b
withSomeDense :: (forall currency. Dense currency -> b) -> SomeDense -> bIf you keep in mind that Dense currency and SomeDense are simply two different ways if representing the same thing, then the similarities are even more obvious. The dense monetary value is our a. However, as we learned before when we introduced RankNTypes, we need to quantify the currency variable so that it exists only within the scope of the given function, and finally we can explain why in simple words: Dense currency appears in positive position, which forces the implementation of withSomeDense to provide a value of this type after having chosen a currency. However, we can't, since we won't learn about our currency until runtime when we inspect what's inside the given SomeDense. So, with RankNTypes, we can defer that decision until later while still satisfying the positive position requirements of this argument, provided there is a function able to handle any Dense currency it may be given.
And with this, we will stop our tour full of distractions. Hopefully we learned a thing or two about Haskell and using the type system as a reasoning tool. And if not, perhaps at least we grew curious about this fascinating tool that allows us to stop trusting and start proving.
Regarding safe-money, you can start using it today. It is available in Hackage and GitHub, with plenty of documentation and tests. Production ready, if you fancy that term.
By Renzo Carbonara. First published in December 2017.
Do you like this? Head to A Type of Programming for more.
This work is licensed under a Creative Commons Attribution 4.0 International License.