Skip to content

Instantly share code, notes, and snippets.

@rampion

rampion/LetsGetDangerous.md

Last active January 20, 2020 05:02
Show Gist options
  • Save rampion/c14d1bc3639b4f00ed8d33d948d01080 to your computer and use it in GitHub Desktop.
Save rampion/c14d1bc3639b4f00ed8d33d948d01080 to your computer and use it in GitHub Desktop.
Download ZIP
Let's Get Dangerous
Raw
LetsGetDangerous.md

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:

@noaheasterly, January 15, 2020:

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
  }

@noaheasterly, January 15, 2020:

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
    }

sumNotionals :: [Trade] -> PMoney

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

@alexnixon_uk, January 15, 2020:

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
  add (Inj si (Trade quantity (Money price) _)) = 
    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)
  ]

Literate Haskell

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"
nnoremap <Leader> :make<CR>
nnoremap <Leader>p :!pandoc --from gfm --standalone > %:r.html % --metadata title="Let's Get Dangerous"<CR>
nnoremap <Leader>t :!doctest -pgmL bin/markdown-unlit %:r.lhs<CR>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment