如何有效地添加存在类型的安全货币值？

Question

我编写了一个玩具库，它使用依赖类型来表示货币及其类型签名中的货币：

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness CHF
  EURWitness :: CurrencyWitness EUR
  PLNWitness :: CurrencyWitness PLN
  USDWitness :: CurrencyWitness USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)


data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

我现在如何编写

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)

，仅当它们是相同的货币时才可以安全地加钱？您可以想象，在用户提供货币参数的情况下可能需要这样做，因此我们无法在编译时检查他们的货币。

我最好的方法是：

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c' _)) = case (c, c') of
  (CHFWitness, CHFWitness) -> Just . SomeMoney $ add m m'
  (PLNWitness, PLNWitness) -> Just . SomeMoney $ add m m'
  -- ...
  (_, _) -> Nothing

这种方法的缺点是编写起来很麻烦、重复，并且当我添加新货币时会出现错误，因为编译器不会警告我这种情况未处理。

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c _)) = _

不起作用。 GHC 抱怨重复

c

：

Conlicting definitions of 'c'

。

Answer 1

一个选择是编写一个函数，将单例降级为正常值：

demoteCurrencyWitness :: CurrencyWitness c -> Currency
demoteCurrencyWitness CHFWitness = CHF
...

然后你可以使用沼泽标准的平等检查，以及货币无关的添加：

addSomeMoney (SomeMoney (Money c amount)) (SomeMoney (Money c' amount'))
 | demoteCurrencyWitness c == demoteCurrencyWitness c'
              = Just . SomeMoney . Money c $ amount+amount'
 | otherwise  = Nothing

在这种情况下，忘记 

demoteCurrencyWitness

子句将给出明显的错误，而不是错误的

Nothing

结果。写这个还是有点乏味，所以我会用

singletons-th

 来代替。

Answer 2

我们从OP的代码开始，大部分是逐字的。我们只添加一些扩展，启用警告（这应该在其他地方更正确地完成，但让我们保持简单）和

import Data.Typeable

。

（我还没有检查是否可以删除某些扩展）

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, 
    TypeApplications, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}
   
import Data.Typeable

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness 'CHF
  EURWitness :: CurrencyWitness 'EUR
  PLNWitness :: CurrencyWitness 'PLN
  USDWitness :: CurrencyWitness 'USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

现在是新部分。

我们首先“证明”任何货币类型都满足

Typeable

约束。这很简单，但需要一些样板文件。

重要的是，添加新货币将触发非详尽的模式匹配警告，因此保持同步相当容易。

withTypeableCurrency :: CurrencyWitness c -> (Typeable c => a) -> a
withTypeableCurrency CHFWitness x = x
withTypeableCurrency EURWitness x = x
withTypeableCurrency PLNWitness x = x
withTypeableCurrency USDWitness x = x

然后是加币功能。我们调用 

withTypeableCurrency

在范围内放置两个

Typeable

约束。然后我们利用

eqT

来检查两种货币类型是否相同。在肯定的情况下，我们不会得到一个无聊的

True

布尔值，而是一个方便的

Refl

，它允许编译器识别类型。剩下的就很简单了。

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney (m1@(Money (c1 :: CurrencyWitness tc1) _)))
             (SomeMoney (m2@(Money (c2 :: CurrencyWitness tc2) _))) =
  withTypeableCurrency c1 $
  withTypeableCurrency c2 $
  case eqT @tc1 @tc2 of
    Just Refl -> Just . SomeMoney $ add m1 m2
    Nothing -> Nothing