Showing how to generalize PMoney and SMoney using dependent types and singletons, follow up to https://twitter.com/alexnixon_uk/status/1217446321348661248?s=20

Money.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-} 
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Money where

import Control.Applicative (liftA3)
import Control.Arrow ((&&&))

import Data.Function (on)
import Data.Functor ((<&>))
import Data.Functor.Compose (Compose(..))
import Data.Functor.Identity (Identity(..))
import Data.Functor.Product (Product(..))

import Data.Map (Map)
import qualified Data.Map as Map

import Data.Proxy (Proxy(..))

{-
One way to generalize this is to use dependant types.

First we'll need a way to encode dependent sum
and product types in Haskell.
-}

-- dependent sum type: |Σ k a| = |a x₀| + |a x₁| + … + |a xₙ| for xₜ ∈ k
data Σ k a where
  Inj :: Sing k x -> a x -> Σ k a

one :: Functor f => (forall x. Sing k x -> a x -> f (b x)) -> Σ k a -> f (Σ k b)
one f (Inj sx ax) = Inj sx <$> f sx ax

-- dependent product type: |Π k a| = |a x₀| * |a x₁| * … * |a xₙ| for xₜ ∈ k
newtype Π k (a :: k -> *) = Exp { runExp :: forall (x :: k). Sing k x -> a x }

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

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

-- we define currency as normal
data Currency = USD | GBP | JPY

instance Algebraic Currency where
  data Sing Currency x 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) where

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

-- we can define pattern synonyms (pseudo-constructors) for creating/matching Σ Currency a values:
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 #-}

-- and a pattern synonym for creating/matching Π Currency a values
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 #-}
  
newtype Money (c :: Currency) = Money { unMoney :: Rational }
{-
Σ Currency Money is isomorphic to

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

Π Currency Money is isomorphic to

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

{-
> 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.

We'll need a well-typed map
-}
newtype Map1 key val x = Map1 { getMap1 :: Map (key x) (val x) }

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

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

lookup :: Ord (key x) => Sing k x -> key x -> PMap key val -> Maybe (val x)
lookup sx kx = Map.lookup kx . getMap1 . proj sx

insert :: Algebraic k => Ord (key x) => Sing k x -> key x -> val x -> PMap key val -> PMap key val
insert sx kx vx = runIdentity . (lens sx $ Identity . Map1 . Map.insert kx vx . getMap1)

fromList :: (Algebraic k, forall x. Ord (key x)) => [Σ k (Product key val)] -> PMap key val
fromList = foldr (\(Inj sx (Pair kx vx)) -> insert sx kx vx) empty

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

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

{-
Now creating a well typed trade map is easy:
-}

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

instance Eq (Trade c) where
  a == b = compare a b == EQ
instance Ord (Trade c) where
  compare = compare `on` uuid

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)
  ]