如何高效实现存在类型安全货币值的同币种安全加法？

核心问题是要在运行时验证两个CurrencyWitness对应的类型相等，并让GHC认可这种相等性，从而安全调用add。以下是几种高效实现方式：

方法一：手动实现类型相等证明函数 #

先定义一个函数，当两个CurrencyWitness相等时返回类型相等的证明（(:~:) c c'），否则返回Nothing。GHC会因为CurrencyWitness是GADT，在新增币种时自动警告非穷举的模式匹配，避免遗漏分支：

import Data.Type.Equality ( (:~:)(Refl) )

sameCurrency :: CurrencyWitness c -> CurrencyWitness c' -> Maybe (c :~: c')
sameCurrency CHFWitness CHFWitness = Just Refl
sameCurrency EURWitness EURWitness = Just Refl
sameCurrency PLNWitness PLNWitness = Just Refl
sameCurrency USDWitness USDWitness = Just Refl
sameCurrency _ _ = Nothing

再利用这个证明函数实现addSomeMoney：

addSomeMoney :: Num r => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c' _)) =
  case sameCurrency c c' of
    Just Refl -> Just . SomeMoney $ add m m'
    Nothing -> Nothing

当sameCurrency返回Just Refl时，GHC会自动推导c和c'是同一类型，因此m和m'的类型统一为Money c r，可以合法调用add。

方法二：借助singletons库自动生成（可选） #

如果项目中使用singletons库，可以彻底避免手动维护相等证明。先通过模板Haskell自动生成单例类型和相等证明函数：

{-# LANGUAGE TemplateHaskell #-}
import Data.Singletons.TH

$(singletons [d|
  data Currency = CHF | EUR | PLN | USD
    deriving (Bounded, Enum, Eq, Read, Show)
  |])

此时库会自动生成对应CurrencyWitness的Sing Currency类型，以及singEq函数。直接用它实现addSomeMoney：

addSomeMoney :: Num r => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c' _)) =
  case singEq c c' of
    Just Refl -> Just . SomeMoney $ add m m'
    Nothing -> Nothing

新增币种时只需修改Currency的定义，所有相关代码会自动更新。

关于直接模式匹配报错的原因 #

你尝试的addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c _))会报错，因为两个c是独立的类型变量，GHC不会默认推断它们相等。必须通过显式的类型相等证明，才能让GHC认可两个Money实例的类型一致，从而允许调用add。

内容的提问来源于stack exchange，提问作者gregorias