{{ message }}

Instantly share code, notes, and snippets.

# rampion/LetsGetDangerous.md

Last active Jan 20, 2020
Let's Get Dangerous

Alex Nixon's recent "Static Types Are Dangerous(ly interesting)" does a great job of showing how, even with the power of static types, it's far from obvious to how best use them, and how to best balance convenience with safety.

The example problem presented in the article discussed how to sum the notional value of a set of "trades" where individual trades may use different currencies.

One of the approaches Alex presented used Data Kinds to statically assure that different types of currency didn't mixed up, but ran into trouble when creating a list of trades of different currencies.

My proposed solution to that particular problem was to use sum and product types over currencies:

I’d probably take the approach of creating two types:

```data SMoney
= Pounds (Money GBP)
| Dollars (Money USD)
| Yen (Money JPY)

data PMoney = PMoney
{ pounds :: Money GBP
, dollars :: Money USD
, yen :: Money JPY
}```

PMoney is isomorphic to Map Currency Rational, so feel free to substitute that. PMoney can have a Num instance.

Then use

```data Trade = Trade
{ tQty    :: Rational
, tPrice  :: SMoney
, tTicker :: Ticker
}

Alex had a legit concern, which that it doesn't seem to generalize:

Yeah that's really nice! The downside I think is that it doesn't generalise.

For example, say you want to represent a well-typed map where the keys are a "Trade" and the values "Money", and the currency is statically proven to be the same.

So here, I'd like to rise to the challenge and show one way of generalizing my original solution.

### Dependent types

The primary tool I'm going to use is that of dependent types.

If you've done much haskell, you're probably familiar with the concept of algebraic types. `(a, b)` is called a product type because the number of values of type `(a, b)` is equal to the number of values of type `a` times the number of values of type `b`. `Either a b` is a called a coproduct or sum type because the number of values of type `Either a b` is equal to the number of values of type `a` plus the number of values of type `b`.

``````|(a,b)|      = |a| * |b|
|Either a b| = |a| + |b|
``````

Haskell lets us create sums and products of arbitrary numbers of types:

```{-# LANGUAGE DataKinds, GADTs, DataKinds, PolyKinds, TypeOperators #-}
-- …
data SumOf (as :: [*]) where
Here  :: a -> SumOf (a ': as)
There :: SumOf as -> SumOf (a ': as)

data ProductOf (as :: [*]) where
Unit :: ProductOf '[]
(:*) :: a -> ProductOf as -> ProductOf (a ': ts)```

And we can calculate their cardinality fairly directly:

``````|SumOf [a₀, a₁, ... aₙ]|     = |a₀| + |a₁| + … + |aₙ| = sum(|aᵢ| for i in [0..n])
|ProductOf [a₀, a₁, ... aₙ]| = |a₀| * |a₁| * … * |aₙ| = product(|aᵢ| for i in [0..n])
``````

Dependent sum types and dependent product types work similarly, except they let us create sums and products of types that are parameterized by some other type.

``````|Σ k a| = |a i₀| + |a i₁| + … + |a iₙ| = sum(|a i| for i ∈ k)
|Π k a| = |a i₀| * |a i₁| * … * |a iₙ| = product(|a i| for i ∈ k)
``````

In languages like Agda, we can write dependent types directly:

```data Σ (K : Set) (A : K → Set) : Set where
Σ_intro : ∀ (i : K) → A i → Σ K P

data Π (K : Set) (A : K → Set) : Set where
Π_intro : (∀ (i : K) → A i) → Π K P```

In haskell, we can implement `Σ` and `Π`¹ using singleton types to lift values of type `k` into types of kind `k` and some helper functions to manipulate the dependent sums and products.

```{-# LANGUAGE Rank2Types, TypeFamilies #-}
-- import Data.Functor.Identity (Identity(..))
-- …
data Σ k a where
Inj :: Sing k i -> a i -> Σ k a

one :: Functor f => (forall i. Sing k i -> a i -> f (b i)) -> Σ k a -> f (Σ k b)
one f (Inj si ai) = Inj si <\$> f si ai

newtype Π k (a :: k -> *) = Exp { runExp :: forall (i :: k). Sing k i -> a i }

proj :: Sing k i -> Π k a -> a i
proj = flip runExp

class Algebraic k where
data Sing k :: k -> *
every :: Applicative f => (forall i. Sing k i -> a i -> f (b i)) -> Π k a -> f (Π k b)
lensFor :: Functor f => Sing k i -> (a i -> f (a i)) -> Π k a -> f (Π k a)

update :: Algebraic k => Sing k i -> (a i -> a i) -> Π k a -> Π k a
update si f = runIdentity . (lensFor si \$ Identity . f)```

### Handling currency

In order to use this machinery, we need to define a singleton type for our `Currency` type:

```-- import Data.Functor ((<&>))
-- import Control.Applicative (liftA3)
-- …
data Currency = USD | GBP | JPY

instance Algebraic Currency where
data Sing Currency i where
SUSD :: Sing Currency 'USD
SGBP :: Sing Currency 'GBP
SJPY :: Sing Currency 'JPY

every f (Exp g) = liftA3 ΠCurrency
(f SUSD \$ g SUSD)
(f SGBP \$ g SGBP)
(f SJPY \$ g SJPY)

lensFor SUSD f (Exp g) = f (g SUSD) <&> \dollars -> ΠCurrency dollars (g SGBP) (g SJPY)
lensFor SGBP f (Exp g) = f (g SGBP) <&> \pounds  -> ΠCurrency (g SUSD) pounds (g SJPY)
lensFor SJPY f (Exp g) = f (g SJPY) <&> \yen     -> ΠCurrency (g SUSD) (g SGBP) yen```

If we wanted to, we could define pattern synonyms (pseudo-constructors) for creating/matching `Σ Currency a` and `Π Currency a` values:

```{-# LANGUAGE LambdaCase, PatternSynonyms, ViewPatterns #-}
-- import Control.Arrow ((&&&))
-- …
pattern Dollars :: a 'USD -> Σ Currency a
pattern Dollars m = Inj SUSD m

pattern Pounds :: a 'GBP -> Σ Currency a
pattern Pounds m = Inj SGBP m

pattern Yen :: a 'JPY -> Σ Currency a
pattern Yen m = Inj SJPY m

{-# COMPLETE Dollars, Pounds, Yen #-}

pattern ΠCurrency :: a 'USD -> a 'GBP -> a 'JPY -> Π Currency a
pattern ΠCurrency { dollars, pounds, yen } <- (proj SUSD &&& proj SGBP &&& proj SJPY -> (dollars, (pounds, yen)))
where ΠCurrency dollars pounds yen = Exp \$ \case
SUSD -> dollars
SGBP -> pounds
SJPY -> yen

{-# COMPLETE ΠCurrency #-}```

### Notional sum

Now if we have our parametrized `Money` type:

`newtype Money (c :: Currency) = Money { unMoney :: Rational }`

The `SMoney` and `PMoney` types from my original solution are isomorphic to `Σ Currency Money` and `Π Currency Money` respectively.

```data SMoney
= Dollars (Money USD)
| Pounds (Money GBP)
| Yen (Money JPY)

data PMoney = PMoney
{ pounds :: Money GBP
, dollars :: Money USD
, yen :: Money JPY
}```

So we can use the same approach to compute a notional sum of our trades:

```data Trade c = Trade
{ quantity    :: Rational
, price       :: Money c
, uuid        :: String
}

sumNotionals :: [Σ Currency Trade] -> Π Currency Money
sumNotionals = foldr add zero where

zero :: Π Currency Money
zero = ΠCurrency (Money 0) (Money 0) (Money 0)

add :: Σ Currency Trade -> Π Currency Money -> Π Currency Money
update si \$ \(Money total) -> Money \$ total + quantity * price```

As an example of use:

```>>> :{
sumNotionals
[ Inj SUSD \$ Trade 3 (Money 1.25) "coke"
, Inj SGBP \$ Trade 1 (Money 2.0) "tea"
, Inj SUSD \$ Trade 4 (Money 11.5) "bagels"
, Inj SGBP \$ Trade 9 (Money 12.0) "crumpets"
, Inj SJPY \$ Trade 2 (Money 7.30) "nori"
]
:}
49.75USD 110.00GBP 14.60JPY
```

### A Well-typed map

But what about the other problem?

For example, say you want to represent a well-typed map where the keys are a "Trade" and the values "Money", and the currency is statically proven to be the same.

All we need is a parameterized map type:

```{-# LANGUAGE QuantifiedConstraints #-}
-- import           Data.Functor.Compose (Compose(..))
-- import           Data.Functor.Product (Product(..))
-- import           Data.Map (Map)
-- import qualified Data.Map as Map
-- …
newtype Map1 key val i = Map1 { getMap1 :: Map (key i) (val i) }

type PMap (key :: k -> *) (val :: k -> *) = Π k (Map1 key val)

empty :: PMap key val
empty = Exp \$ \_ -> Map1 Map.empty

lookup :: Ord (key i) => Sing k i -> key i -> PMap key val -> Maybe (val i)
lookup si ki = Map.lookup ki . getMap1 . proj si

insert :: Algebraic k => Ord (key i) => Sing k i -> key i -> val i -> PMap key val -> PMap key val
insert si ki vi = update si (Map1 . Map.insert ki vi . getMap1)

fromList :: (Algebraic k, forall i. Ord (key i)) => [Σ k (Product key val)] -> PMap key val
fromList = foldr (\(Inj si (Pair ki vi)) -> insert si ki vi) empty

type PList (a :: k -> *) = Π k (Compose [] a)

fromList' :: (Algebraic k, forall (i :: k). Ord (key i)) => PList (Product key val) -> PMap key val
fromList' = runIdentity . every (\_ -> Identity . Map1 . Map.fromList . fmap (\(Pair ki vi) -> (ki,vi)) . getCompose)```

Now creating a well typed trade map is easy:

```example :: PMap Trade Money -- ~ Π Currency (Map1 Trade Money)
example = fromList
[ Inj SUSD (Trade 3 (Money 1.25) "coke" `Pair` Money 43000)
, Inj SGBP (Trade 1 (Money 2.0) "tea" `Pair` Money 1588)
, Inj SUSD (Trade 4 (Money 11.5) "bagels" `Pair` Money 11.99)
, Inj SGBP (Trade 9 (Money 12.0) "crumpets" `Pair` Money 1e34)
, Inj SJPY (Trade 2 (Money 7.30) "nori" `Pair` Money 0)
]```

This markdown file is literate haskell, and can be compiled using `markdown-unlit`:

``````\$ ln -s LetsGetDangerous.md LetsGetDangerous.lhs
\$ cabal install markdown-unlit
\$ ghc --make -pgmL bin/markdown-unlit LetsGetDangerous.lhs
``````

: ignoring bottom, which I will continue to do through the article.

¹: `Σ` is pronounced "Sigma" and `Π` is pronounced "Pi". The notation is borrowed from mathematics, and is whole lot easier to use in vimٰ² once you learn about the `<C-K>S*` and `<C-K>P*` digraphs.

²: Here's my vim tooling, if you're interested:

```let &makeprg="ghc --make -pgmL bin/markdown-unlit %:r.lhs"