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

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

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

在这种情况下，被遗忘的子句 for 将给出明显的错误而不是错误的结果。demoteCurrencyWitnessNothing

写这个仍然有点乏味，所以我会用 singletons-th 代替。

完全“类型安全”的方法是可能的，但我们必须编写一些样板。

我们从 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

现在是新部分。

我们首先“证明”任何货币类型都满足约束。这是微不足道的，但需要一些样板。cTypeable

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

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

然后，货币添加功能。我们调用它来将两个约束放在范围内。然后我们利用杠杆来检查两种货币类型是否相同。在肯定的情况下，我们得到的不是无聊的布尔值，而是允许编译器识别类型的方便值。剩下的就很容易了。withTypeableCurrencyTypeableeqTTrueRefl

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  -- not the same type of currency

这种方法的优点是样板被限制在 中，并且不必在处理 、 等的每个函数中重复。withTypeableCurrencySomeMoneyaddSomeMoneysubtractSomeMoney

---

更新：一些样板可以利用包和一些模板 Haskell 删除。singletons

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, TypeApplications,
    ScopedTypeVariables, TemplateHaskell, EmptyCase, TypeFamilies,
    UndecidableInstances, TypeSynonymInstances, InstanceSigs #-}

import Data.Singletons.Decide
import Data.Singletons.TH

$(singletons [d|
  data Currency = CHF | EUR | PLN | USD
    deriving (Eq, Read, Show, Bounded)
  |])
-- This automatically creates the equivalent of
--    data SCurrency :: Currency -> Type where
--       SCHF :: SCurrency 'CHF
--       SEUR :: SCurrency 'EUR
--       SPLN :: SCurrency 'PLN
--       SUSD :: SCurrency 'USD
-- and some helper stuff.

-- singletons does not like deriving Enum, so we move it here.
deriving stock instance Enum Currency

-- singletons does not create this for some reason.
deriving stock instance Eq (SCurrency c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(SCurrency 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 m1@(Money c1 _))
             (SomeMoney m2@(Money c2 _)) =
  -- Check for singleton equality.
  case c1 %~ c2 of
    Proved    Refl -> Just . SomeMoney $ add m1 m2
    Disproved _    -> Nothing