Dependent Types To Eliminate Runtime Checks

One of the main advantages of static type checking is to catch errors before we deploy code to production. Dependent Types allow us to eliminate some checks that are usually done at run time. Through a simple example, this article demonstrates how dependent types can be applied in everyday programming.

Give Me The Money

Let us start with an example. We will define a simple type for representing money and a function to add money.

1data Money = Money Rational

Now we can add them together as

1add :: Money -> Money -> Money
2add (Money m1) (Money m2)  = Money (m1 + m2)
3
4money1 = Money (50 % 100)
5money2 = Money (25 % 100)
6
7total = add money1 money2

Everything OK There?

We’ve overlooked a crucial detail: currency. Money is always denominated in a specific currency (e.g., US Dollar), and it’s invalid to add amounts from different currencies.

Let’s include currency information in our Money type. A simple approach is to keep a string representing the currency (“GBP”, “USD”, etc.) along with the amount.

1data Money = Money String Rational
2
3twoDollars :: Money
4twoDollars = Money "USD" 2

Houston, We’ve Got a Problem

The constraint that only Money values with same currency can be added makes our add function partial.

1add:: Money -> Money -> Money
2add   (Money c1 m1) (Money c2 m2) =
3      case c1 == c2 of
4          True  ->  Money c1 (m2 + m2)
5      --  False ->  ??  -- the function is not defined for this value 

Partial functions are bad. They pass type check and fail at runtime. The application crashes when inputs for which the function is not defined are passed. Our add function above fails if it is ever called with two Money values with different currency.

1λ> :t add fiftyPence twoDollars
2add fiftyPence twoDollars :: Money
3
4λ> add fiftyPence twoDollars
5*** Exception: /Users/vj/workspace/Haskell/Money.hs:(23,7)-(24,37): Non-exhaustive patterns in case

Improvise, Adapt, Overcome

A common approach to resolve this is to extend the function, making it return a specific value (an error value) for inputs where it’s not well-defined.

Wrapping the return type with Maybe or Either e are common approaches to extending the function. A special value of Nothing::Maybe Money (or Left "Incompatible Currency"::Either String Money) can be returned for all the inputs where add is originally not defined.

If we use Maybe Money or Either Error Money as the return type, the calling function must handle these potential error values (perhaps by propagating the error to its own caller).

1add :: Money -> Money -> Maybe Money
2add   (Money c1 m1) (Money c2 m2) = 
3      case c1 == c2 of
4          True  -> Just (Money c1 (m1 + m2))
5          False -> Nothing

Independence? Freedom? What?

Using dependent types we can avoid the runtime check by making it possible for the compiler to do that check for us. Since the compiler prohibits calling our add function with incompatible money values, we are not only freed from runtime check, we also don’t have to worry about error handling.

This is in contrast to extending the function. Here we restrict the domain of the function to contain only those values for which the function is defined.

 1{-# LANGUAGE KindSignatures, DataKinds #-}
 2
 3import GHC.TypeLits (Symbol)
 4import Data.Ratio ((%))
 5
 6data Money (currency :: Symbol) = Money Rational
 7
 8fiftyPence :: Money "GBP"
 9fiftyPence = Money (50 % 100)
10
11twoDollars :: Money "USD"
12twoDollars = Money 2
13
14add :: Money c -> Money c -> Money c
15add (Money m1) (Money m2) = Money (m1 + m2)

Notice how the implementation of add function is same as the one before introducing currency parameter. It has no if/case expressions and no Maybe return type. It is a compilation error to add Money values with different currency.

 1λ> :t add fiftyPence fiftyPence
 2add fiftyPence fiftyPence :: Money "GBP"
 3
 4λ> :t add fiftyPence twoDollars
 5
 6<interactive>:1:16: error:
 7    • Couldn't match type ‘"USD"’ with ‘"GBP"’
 8      Expected type: Money "GBP"
 9        Actual type: Money "USD"
10    • In the second argument of ‘add’, namely ‘twoDollars’
11      In the expression: add fiftyPence twoDollars

We use language extensions in GHC for using dependent types. I will try to explain their usage in simple terms.

Be Kind To Others

Notice the type of fiftyPence -

1fiftyPence :: Money "GBP"

Money is a type constructor, as we know, type constructors only accepts other types as parameters (Maybe Int, [Int] etc.). But, "GBP" looks like a String value! How is this possible?

Firstly, "GBP" in fiftyPence :: Money "GBP" is not a value but a type with kind Symbol. You can see that in the data definition of Money. currency type parameter is of kind Symbol.

1data Money (currency :: Symbol) = Money Rational

Symbol is a convenient Kind provided by GHC in the GHC.TypeLits module which is the kind for type-level strings. It lets us use string literals like “GBP” as a type.

Congratulations! You have Been Promoted

OK, So, KindSignatures extension lets me specify that currency has kind Symbol, but how does "GBP" and "USD" become types of of kind Symbol?

1fiftyPence :: Money "GBP"
2fiftyPence = Money (50 % 100)
3
4twoDollars :: Money "USD"
5twoDollars = Money 2

This is all thanks to another GHC extension we have used - DataKinds. When this extension is enabled, the type constructors are promoted to Kinds and value constructors are promoted to type constructors.

In our case, the kind Symbol is already provided by GHC. All we need is for GHC to promote and recognize "GBP" as type.

 1λ> :k Money "GBP"
 2
 3<interactive>:1:7: error:
 4    Illegal type: ‘"GBP"’ Perhaps you intended to use DataKinds
 5
 6λ> :set -XDataKinds
 7λ> :k Money "GBP"
 8Money "GBP" :: *
 9
10λ> :k Money Int
11
12<interactive>:1:7: error:
13    • Expected kind ‘Symbol’, but ‘Int’ has kind ‘*’
14    • In the first argument of ‘Money’, namely ‘Int’
15      In the type ‘Money Int’

The Beginning

There is much more to depended types than what we have seen here. This is to show readers that dependent types can be useful in day-to-day programming as well.